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

授業スライド こちらから 授業要約・宿題 こちらから

前回の復習 宿題の答え合わせ 形式化された算術

今回は、台風で中止になった前回の内容で行います。前々回までで、最小述語論理の話は終了です。これである程度数学を展開するための道具は揃いました。それでは、授業第十回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょ…

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

授業スライド こちらから 授業要約・宿題 こちらから

前回の復習 宿題の答え合わせ 形式化された算術

緊急:本日は台風のため休講とします。 前回までで、最小述語論理の話は終了です。これである程度数学を展開するための道具は揃いました。それでは、授業第十回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう！ その枠組み…

授業スライド こちらから 授業要約・宿題 こちらから

前回の復習 宿題の答え合わせ eigenvariable条件（復習） 双対性 (duality) 宿題

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

授業スライド こちらから 授業要旨・宿題 こちらから

前回の復習 宿題の答え合わせ 述語論理:∃の導入と除去 双対性 (duality) 宿題

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