数学基礎論サマースクール2018
証明論 特に算術の無矛盾性証明
2018年9月3日から6日,神戸大学
《台風21号の影響によりプログラムおよび懇親会の日程に変更があります:9月1日更新》
不完全性定理によりペアノ算術 PA の無矛盾性は厳密には有限的に証明できないが,
ゲンツェンは順序数 ε_0 までの超限帰納法を用いて,
カット消去法によって PA の無矛盾性を,ある意味で有限的に証明した.
その後,アッカーマンはヒルベルトの ε 計算を用いた
PA の無矛盾性の証明を,
ゲーデルは直観主義算術を介した PA の無矛盾性の証明を与えている.
証明論の古典とでも呼ぶべきこの三つの無矛盾性証明は,
互いに深く関係しながらも全く異なる発想のもとで同じ目的を達成する興味深いもので,
技術的にも現在の証明論や理論計算機科学の基礎となる重要なものでもある.
今回の数学基礎論サマースクールではこの三つの無矛盾性の証明と,
この三つの無矛盾性証明から始まる証明論の発展を紹介する.
⊢ 概要
日時:2018年9月3日(月)から6日(木)
場所:神戸大学六甲台第2キャンパス内工学研究科LR棟5階LR501教室
http://www.kobe-u.ac.jp/guid/access/rokko/rokkodai-dai2.html
住所:神戸市灘区六甲台町1-1
情報:http://www2.kobe-u.ac.jp/~mkikuchi/ss2018.html
⊢ 講師および内容
(本論)
秋吉亮太:ゲンツェンとシュッテのカット消去法
高橋優太:ヒルベルトの ε 計算 [pdf1, pdf2,
pdf3]
藤原誠:ゲーデルのダイアレクティカ解釈と直観主義算術 [pdf, reference]
(入門・予備知識)
菊池誠:チュートリアル,趣旨説明,予備知識 [pdf1, pdf2]
黒川英徳:LK のカット消去定理
(発展)
新井敏康:ゲンツェンから始まる証明論50年 [pdf]
⊢ プログラム(9月1日更新)
9月3日(月)(変更があります:9月3日更新)
8:50-(受付開始:9月3日は休憩時間内に随時受付をします)
9:00-10:30:菊池1(三つの体系,完全性定理と不完全性定理:数理論理学の予備知識を持たない人に)
10:40-12:10:黒川1(LK のカット消去定理)
13:10-14:40:黒川2(カット消去定理の周辺)
14:50-16:20:菊池2(順序数のカントール標準形,ゲンツェンの証明の概要)
16:30-18:00:秋吉1(テイト計算と無限的証明図)
9月4日(火):警報が発令される可能性が高いため講義はなし
9月5日(水)
9:00-10:30:秋吉2(シュッテの無矛盾性証明)
10:40-12:10:秋吉3(シュッテの証明とゲンツェンの証明の対応)
13:10-14:40:藤原1(ダイアレクティカ解釈による算術の無矛盾性証明の概略)
14:50-16:20:高橋1(1階述語論理に対するε計算)
16:30-18:00:新井1(ゲンツェンから1960年代まで)
(18:30-:懇親会)
9月6日(木)
9:00-10:30:藤原2(ダイアレクティカ解釈の健全性定理)
10:40-12:10:高橋2(アッカーマンによる無矛盾性証明)
13:10-14:40:藤原3(BHK 解釈から見たダイアレクティカ解釈の意味)
14:50-16:20:高橋3(カット消去によるε代入法の停止性証明)
16:30-18:00:新井2(竹内外史からシュッテ学派へ)
⊢ 台風21号への対応(9月1日更新)
現在の予報では神戸市は4日(火)朝から警報が発令される可能性が高いです.
従って4日の講義は全て中止にして, 3日(月)の開始時刻を9時に変更します.
また,懇親会は4日から5日に変更します.
⊢ 懇親会(日程に変更があります)
日時:9月5日(水)18:30-20:30
場所:神戸大学六甲台第1キャンパス内アカデミア館3階レストランさくら
http://www.kucoop.jp/info/index.html
会費:3,500円(3日の受付時にお支払いください.4日から参加の場合は事前にご連絡ください.)
4日開催の予定に基づく出欠から変更のある場合は菊池誠(mkikuchi@kobe-u.ac.jp)までご連絡ください.
⊢ 参加申込
参加ご希望の方は以下の情報を8月24日(金)までに email で,
件名を「SS2018」として菊池誠(mkikuchi@kobe-u.ac.jp)までお送りください.
氏名:
所属:
身分:
連絡先 email アドレス:
懇親会:参加・不参加
締切を過ぎても対応可能な場合があります.お問い合わせください.
⊢ 世話人・連絡先:菊池誠,酒井拓史