Formalized Formal Logic
- Shogo Saito
- Mashu Noguchi
数理論理学の様々な事実をLeanで形式化するプロジェクト．自分は主に様相論理を中心とした証明可能性論理，解釈可能性論理や命題論理について形式化している．全体としてはGödelの不完全性定理やSolovayの算術的完全性定理などが形式化されている．
https://github.com/FormalizedFormalLogic/Foundation
野口 真柊
Mashu Noguchi
主に定理証明支援系を用いて形式化した成果物を置いておきます．
数理論理学の様々な事実をLeanで形式化するプロジェクト．自分は主に様相論理を中心とした証明可能性論理，解釈可能性論理や命題論理について形式化している．全体としてはGödelの不完全性定理やSolovayの算術的完全性定理などが形式化されている．
https://github.com/FormalizedFormalLogic/Foundation
T. Kurahashi and K. Tominaga. “Smullyan’s truth and provability” で導入されたSmullyanの初等的な形式体系をLeanで形式化し，不動点定理やTarskiの定義不可能性定理，Gödelの不完全性定理のような現象が起こることを確認した．
https://github.com/SnO2WMaN/SmullyanTP