ac.sno2wman.net

メモ

勉強したことやちょっとしたメモなどを置いておきます．

1. 論理学を（Leanで）つくる

   論理学をLeanで作ってみて，数理論理学と論理学に同時に修練してもらうことを意図した教材． 現在のところ，古典命題論理の強完全性定理の証明のみが置かれていて，解説などは一切無い．

   note

2. Kripke不完全な様相論理

   様相論理 $\mathbf{K}$ の公理 $\Box (\Box p \leftrightarrow p) \to \Box p$ による拡張論理 $\mathbf{KH}$ はKripke意味論に対して完全ではないという事実のノート．

   note

3. 算術の超準モデルなどに関して

   note

4. Yabloのパラドックスについて

   note

5. Henkin構成による1階述語論理の完全性証明

   note

6. Smullyanのシステムの形式化について

   SmullyanTP の形式化に関するちょっとしたメモ． 証明支援系 Advent Calendar 2024の3日目の記事として書いた．

   note