基礎演習 I 論理学

京都大学文学部の「基礎演習 I 論理学」(毎週火曜日16:30〜18:00)の授業Blogです。

CAPE論理学上級Ⅱ「構成的型理論」

CAPE論理学上級Ⅱ「構成的型理論

開催予定日(中継urlは本ポスト下部を参照してください)

  • ① 3月26日(土)1030-1230「ラッセルのパラドックスと3つの対策」
  • ② 3月26日(土)1430-1630「カリー・ハワード対応と『証明のデータ型としての命題』観」
  • ③ 3月27日(日)1030-1230「証明論的意味論としてのマーティン・レーフの構成的型理論
  • ④ 3月27日(日)1430-1630「認識論の機械化:証明の正規化と証明支援系」
③3月27日(日)1030-1230「証明論的意味論としてのマーティン・レーフの構成的型理論


④3月27日(日)1430-1630「認識論の機械化:証明の正規化と証明支援系」



開催要旨

ラッセルのパラドックスが発見されてから120年がたち、一般向けの概説書では「数学の基礎の危機に、三つの立場『論理主義』『直観主義』『形式主義』が現れて危機を克服しようとしたが、集合論が生き残った」との一言で済まされることが多いようです。実際、ラッセルの論理主義に基づいた型理論は、ゲーデルによって「無意味に複雑である」と評されたように、歴史的な遺物と思われかねない書きっぷりのようにも思えます。

ところがその後、1972年にマーティンレーフが構成的型理論を発表し、論理主義と直観主義構成主義)の両派を束ねる形で、新たな流れが始まりました。構成的型理論は数学の基礎としてだけではなく、計算機科学の基礎理論(有限ステップで計算が終わるプログラムのための基礎理論)として大きな役割を果たすようになります。

この進展は、論理学における証明論的意味論の進展と手を携えて進んでいます。証明論的意味論における命題の意味はその証明であると見なす立場から、『証明のデータ型としての命題』という考え方が生まれ、構成的型理論はその表現の一つであると見なすことができるからです。
技術的な観点からは、マーティンレーフらの構成的型理論の最大の特徴は、データ型の帰納的な構成法を許す点にあり、このアイディアこそ、帰納的な構成と解体という構成主義の基本的なアイディアを表現し、再帰関数の定義を自然に行うことを可能にするのです。

このような構成的型理論は、コンピュータ上に実装することができ、現在、コンピュータのソフトウェアの正しさを証明する「ソフトウェア検証」に活用されています。このことは、哲学的には、人間の認識論(知識を獲得するための人間の心の認知的活動)の機械化の一例として、興味あるものです。

この講義では、歴史的な流れを追いながら、構成的型理論の基本的な枠組みを紹介し、余裕があれば証明支援系などの計算機上の実装についても少しお話ししたく思います。

参考文献:

受講対象者:

哲学・論理学・言語学・計算機科学などを専門とする大学院生以上を想定していますが、どなたでもご参加いただけます。前提知識としては、
(1)自然演繹を使って証明を書いたことがある、
(2)古典論理直観主義論理のちがいについて聞いたことがある(排中律等)、
(3)ラッセルのパラドックスについて聞いたことがある
の3点とします。

第177回CAPEレクチャー(2021/09/12)

日時: 2021年09月12日(日) 16:00-18:00
開催方法:Youtubeにて中継

タイトル:

構成と解体:原始再帰関数の計算と推論の共通点

アブストラクト:

推論と計算はよく似ていると言われ、多くの共通点が指摘されています。その中で、本レクチャーでは、「必ず有限ステップで答を出さなければならない」という性質に着目し、計算と推論(証明)がともに、有限ステップの「構成」と「解体」という操作に分解でき、本質として同じで表現の仕方が異なるのだということを紹介します。

参考資料

www.academia.edu

中継

前回、最小算術 Q の断片(大小関係に関する公理を除去したもの)の公理系を紹介し、これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう!
その枠組みとして、計算が有限回で終わることが確実に見て取れるようなメタレベルの「原始再帰関数」について、それを対象レベルでシミュレートするような関数を考え、対象レベルにおいてもその値がメタレベルにおける計算と等しくなる(数値的表現可能性)を紹介し、その例として「2+2=4」となることをQにおいて形式的に証明してみましょう。

授業内容

  1. 前回の復習
  2. 1≠2
  3. 計算(原始再帰的関数)
  4. 証明(数値的表現可能性)
  5. 成績および今後の予定



注意
  1. 本来は、0だけでなく、形式化された算術の全ての記号(=,+,×など)も、本来の算数の記号と分けて書く必要があるのですが、スライド作成の都合上、同じ記号を使っています。ご注意下さい。

前回までで、最小述語論理の話は終了です。これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう!
その枠組みとして、形式化された算術(自然数と足し算・かけ算の世界)の一つである、最小算術 Q の断片(大小関係に関する公理を除去したもの)を選びます。そして、例として、等式に関する命題(1≠2)を、Qにおいて形式的に証明してみましょう!!

授業内容

  1. 前回の復習
  2. 宿題の答え合わせ
  3. 形式化された算術
  4. 1≠2
  5. 成績および今後の予定

注意
  1. 本来は、0だけでなく、形式化された算術の全ての記号(=,+,×など)も、本来の算数の記号と分けて書く必要があるのですが、スライド作成の都合上、同じ記号を使っています。ご注意下さい。

本日の授業内容

授業第十回目、最小述語論理の問題演習です。また、量化子 ∀の導入規則と∃の除去規則に付加されているeigenvariable条件についての復習を行います。この二つの制限が組み合わさって、∃x(x=0)⇒∀(x=0)のような望まれない命題の導出をどう防ぐのかを解説します。また、前回時間がなかったため、二つの量化子の双対性について復習します。

授業内容
  1. 前回の復習
  2. 宿題の答え合わせ
  3. eigenvariable条件(復習)
  4. 双対性 (duality)

本日の授業

授業第九回目、存在量化子 ∃の導入・除去規則についてです。∀の場合は導入規則にeigenvariable条件がありましたが、∃では除去規則に似たようなeigenvariable条件があり、∃xA の除去規則で Aを満たす自然数 x を選ぶ際の制約条件はAのみであることを表現しています。この規則は x がA[x]を満たす「未知数」であることを表現しています。

授業内容

  1. 前回の復習
  2. 述語論理:∃の導入と除去


本日の授業

授業第八回目の今回は、全称量化子 ∀ の導入・除去規則についてです。∀xP(x) は「前提なしで任意の x を選んできたとき P(x)が成立する」という意味ですが、その「前提なしで選ぶ」という要求を実現するため、∀ の導入規則には 「eigenvariable 条件」という非常にややこしい制限がついているので、注意が必要です。

授業内容

  1. 前回の復習
  2. 宿題の答え合わせ
  3. 述語論理:∀の導入と除去
  4. 補講日について