SnO2WMaN/lean4-propositional-logic
まだ殆ど何も示していない．意味論すら与えていない． Tait計算のほうもやったが，全然進まなかったので今回は断念… 個人的には今後この計画がうまく行った場合に様相論理の形式化を行いたいと思っており， 様相論理についてTait計算でやっている論文や教科書を見たことがないため一旦こっちで…という腹積もりもある 大いに参考にしている
対象は命題論理なので量化子に関する公理/推論規則は省略した． 以下を導入した．
本の中では$ \sf SK
この公理の名前$ \sf Sと$ \sf Kが何から来ているのかは書いてないが，多分SKIコンビネータ計算のSとKなのではないかと思う S := λxyz.xz(yz)
$ \mathsf {S} \equiv (\Phi \to \Psi \to \Chi) \to (\Phi \to \Chi) \to (\Psi \to \Chi)
K := λxy.x
$ \mathsf{K} \equiv \Phi \to (\Psi \to \Phi)
書いているときに気づいたがこのままでは様相論理の公理K$ \sf Kと名前が被って大変なことになってしまう 構文的同値$ \lnot \varphi \equiv \varphi \to \botとする．
無くてもいいがあったほうが式の見通しが良くなる．
$ \botに意味を与えるという意味でも合ったほうが良い
この時点で証明できるもの
二重否定導入$ \mathsf{DNI} \equiv \Phi \to \lnot\lnot\Phi 驚くべき帰結1$ \mathsf{CM_1} \equiv (\Phi \to \lnot\Phi) \to \lnot\Phi $ \land,\lorに関する公理を$ \sf HPM_0に追加したもの．
これにいろんな公理を更に追加すると$ \sf HPJや$ \sf HPKが得られる
基本的には$ \sf HPMに爆発律$ \mathsf{EFQ} \equiv \bot \to \Phiを追加することで得られる． 基本的には$ \sf HPMに二重否定除去$ \mathsf{DNE} \equiv \lnot\lnot\Phi \to \Phiを追加することで得られる． その他
驚くべき帰結2$ \mathsf{CM_2} \equiv (\lnot\Phi \to \Phi) \to \Phi 排中律$ \mathsf{LEM} \equiv \Phi \lor \lnot\Phi Peirceの法則$ \mathsf{Per} \equiv ((\Phi \to \Psi) \to \Phi) \to \Phi Tarskiの法則$ \mathsf{Tar} \equiv \Phi \lor (\Phi\to\Psi) 実際$ \Psi \equiv \botとすれば$ \lnotの構文的同値に依って排中律と同じものが得られる．
inductive Formulaで帰納的に論理式を与えないという方法はかなり参考にした
https://gyazo.com/46cd209b75296ee22144d0579d2ce5ec
その代わり大変なことにはなっている
HasLogicalSymbolsとかで纏めるべきだが…