CAPE論理学上級Ⅱ「構成的型理論」 開催予定日（中継urlは本ポスト下部を参照してください） ① 3月26日（土）1030-1230「ラッセルのパラドックスと3つの対策」 ② 3月26日（土）1430-1630「カリー・ハワード対応と『証明のデータ型としての命題』観」 ③ 3月27…
第177回CAPEレクチャー(2021/09/12) 日時: 2021年09月12日(日) 16:00-18:00 開催方法:Youtubeにて中継 タイトル: 構成と解体：原始再帰関数の計算と推論の共通点 アブストラクト: 推論と計算はよく似ていると言われ、多くの共通点が指摘されています。その中…
前回、最小算術 Q の断片（大小関係に関する公理を除去したもの）の公理系を紹介し、これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう！ その…
前回までで、最小述語論理の話は終了です。これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう！ その枠組みとして、形式化された算術（自然数と…
本日の授業内容 授業第十回目、最小述語論理の問題演習です。また、量化子 ∀の導入規則と∃の除去規則に付加されているeigenvariable条件についての復習を行います。この二つの制限が組み合わさって、∃x(x=0)⇒∀(x=0)のような望まれない命題の導出をどう防ぐの…
本日の授業 授業第九回目、存在量化子 ∃の導入・除去規則についてです。∀の場合は導入規則にeigenvariable条件がありましたが、∃では除去規則に似たようなeigenvariable条件があり、∃xA の除去規則で Aを満たす自然数 x を選ぶ際の制約条件はAのみであること…
本日の授業 授業第八回目の今回は、全称量化子 ∀ の導入・除去規則についてです。∀xP(x) は「前提なしで任意の x を選んできたとき P(x)が成立する」という意味ですが、その「前提なしで選ぶ」という要求を実現するため、∀ の導入規則には 「eigenvariable …
今週の授業予定 授業第七回目、命題論理はいっぺんおいて、今回から述語論理に入ります。量化子の初回は何故量化子が必要なのか、量化子∀との∃の導入の意図を説明します。 数学では無限を本質的に扱いますが、無限は命題論理の枠組みでは分析しきれません。…
授業内容 授業第六回目の今回は、最小命題論理の自然演繹、⇒, ∧と∨の導入規則・除去規則についての演習です。また、これまで論理結合子⇒, ∧, ∨ を学んできましたが、それらの間の相互関係について考えてみたいと思います。 前回の復習 宿題の答え合わせ 演習…
授業内容 授業第五回目の今回は、メタの世界の「かつ」と「または」をシミュレートする、自然演繹の∧と∨の、導入規則・除去規則について紹介します。また、論理結合子⇒,∧と∨の導入規則と除去規則を持つ記号体系として、最小命題論理を定義します。 前回の復…
授業第四回目は、⇒の導入規則／除去規則に関する問題演習です。前回出題の宿題の回答も説明します。また「きれいな証明」や「部分論理式原理」という概念を紹介します。「きれいな証明」は、名前こそショボいですが、後期で「正規な証明」として再登場する、…
授業第三回目は論理的帰結関係を表す論理結合子⇒の自然演繹における導入規則・除去規則です。論理学の最も重要な概念の一つが論理的帰結関係ですから、それを表す論理結合子⇒ こそ「the 論理結合子 of 論理結合子」という感じです。導入規則と除去規則は、論…
授業第二回目の今回は、帰納的定義を紹介します。また、その例として、形式言語における「自然数もどき」（自然数を表現する計算機内のコード）、項、命題などの帰納的定義を紹介します。 帰納的定義は、計算機上でメタの数学をシミュレートする際の基本的な…
授業第一回目の今回は、本授業の事務上の説明（オンライン授業の進め方、成績評価）および、人間の推論のコンピュータによるシミュレーションとしての形式的な論理学とはどういうものであるかを説明します。同時に、その際に重要になってくる「メタ／対象」…
哲学(演習) ／科学哲学（演習）シラバス 論理学1（講義）（前期 火5）（矢田部俊介） 哲学(演習) （哲学専修 5141001） 科学哲学科学史（演習） （科学史科学哲学 8241005） 授業開始：4月13日（火） 本授業は教務掛での分類でいうところの「対面授業が実施…
論理学上級I 「ウソツキのパラドックス2020（傾向と対策）ー真理理論入門」（矢田部俊介） 京都大学大学院文学研究科 応用哲学・倫理学センター（CAPE）公開セミナー（公式案内はこちら） 日時：2021年3月13日（土）、14日（日） YouTube中継 スケジュール 3…
授業内容 後期授業第十二回目、本日は古典述語論理のタルスキモデルと、完全性定理および健全性定理の話をします。 前期の授業でやったように、そもそも述語論理は無限個の対象に関する推論を行うために導入されたものであり、述語論理のモデルは、命題論理…
後期授業第十一回目、本日は古典命題論理の完全性定理と健全性定理の話をします。 今回は、古典命題論理の完全性定理を、反例を作るときに昔から使用される「分析的推論」を一般化した証明探索樹を使った真理関数の構成法を解説します。また、古典命題論理の…
後期授業第十回目の今回は、古典論理のモデルの紹介を行います。前回演習で紹介したように、古典論理での証明は、排中律をアクロバチックに使う事が可能なため、大変複雑なものになります。では人はなぜ古典論理を使うかというと、そのモデルが非常に簡単で…
古典論理での証明に関する問題演習とします。問題は当日配布します。注：先週、宿題として、古典論理（直観主義論理＋排中律）で二重否定除去則などを証明しようという問題がでており、その答合わせにあたります。お時間がある方はどうぞ。
今回の内容 後期授業第八回目は、直観主義論理上で新たな推論規則として排中律を導入し、古典論理を定義します。 世間一般の数学では、直観主義論理では証明できない「排中律」という規則をよく使います。直観主義論理に新たに推論規則として排中律を付け加…
後期授業第六回目は、直観主義論理のモデルの話です。排中律など直観主義論理で証明できない命題が、直観主義論理で本当に証明できないことを証明するのは大変です。そこで今回は、証明できない命題の「反例モデル」を構成することによって証明不可能性を証…
（11月10日よりハイブリッド授業となります！！） 後期授業第五回は、新しい論理規則を受け入れるとはどういうことかという話をします。 つまり、最小論理に、新しい論理規則「矛盾律」を付加し、論理体系「直観主義論理」へと拡大します。この拡大は保存拡…
後期授業第4回目は、「論理結合子の意味とは何か」という哲学的論理学話のまとめとして、「証明の正規化」の話をします。また、その後、正規化の話を軸に、記号の書き換え体系が論理と呼ばれるための条件について考えたいと思います。具体的には、最小命題論…
後期第三回授業は、「論理結合子の意味とは何か」の続きで、「反転原理」（inversion principle）を取り上げます。 前回紹介したように、トンクは体系を自明化するという本質的な欠陥を持っていましたが、言語全体というグロ−バルなレベルでは、「保存拡大性…
後期授業第二回目の今回は、「論理結合子の条件」について、証明論的意味論の立場から考えてみたいと思います。 具体的には、意味の理論IIの素朴な解釈である素朴な推論主義「論理結合子の意味は導入規則と除去規則によって完全に定められる」が正しいかどう…
後期授業開講＠火曜日5限５講 本日の授業内容 前期は、最小述語論理という体系について、論理結合子の導入規則と除去規則を意味を考えずに紹介してきました。 後期授業の初回である今回は、「論理結合子の意味とは何か」について考えてみたいと思います。 こ…
前回、最小算術 Q の断片（大小関係に関する公理を除去したもの）の公理系を紹介し、これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう！ その…
補講第一回は8月1日（土）16時〜17時半の予定です。前回までで、最小述語論理の話は終了です。これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょ…
本日の授業 授業第九回目、存在量化子 ∃の導入・除去規則についてです。∀の場合は導入規則にeigenvariable条件がありましたが、∃では除去規則に似たようなeigenvariable条件があり、∃xA の除去規則で Aを満たす自然数 x を選ぶ際の制約条件はAのみであること…
