2025.02.10
https://gyazo.com/4685281f50f88c4737584267fa327d21
発狂
これを図示するLeanの何か作りたい．出来るのだろうか？
$ A \in \mathbf{FPL} \iff A^g \in \mathbf{GL}
解釈を次のように定める．
$ f(A \to B) \mapsto \mathrm{Pr}_T(\ulcorner f(A) \to f(B) \urcorner)
$ \mathbf{FPL} \vdash Aと任意の$ fで$ \mathbf{PA} \vdash f(A)が同値となる．
$ A \to B \in \mathbf{FPL} \iff \mathbf{GL} \vdash \Box(A \to B)なのでまあ明らかではある．
帰結関係上のモーダスポネンスは成立しない．
$ p, p\to q \nvdash_\mathbf{VPL} q
特に，$ \top \to p \nvdash p
$ A \to Bの証明とは，$ Aという仮定を使って$ Bの証明を作る方法である．
$ A \to Bの証明は$ Aの証明を$ Bの証明に変換する方法である．
メモ
思った
Harropの補題で$ \vdashの方ってどうやってやるんだっけ？と思ってちょっと考えた $ \lang \varphi_1,...\varphi_n \rang（ただし$ \varphi_nは証明したい論理式で固定する）が実際にHilbert流演繹体系で証明になっているかどうかは有限時間で検査可能 可算無限なのでこれは適当なエンコーディングによって$ \lang \varphi_1,...\varphi_n \rangが列挙可能
これらの事実から従う．
で良いのだっけ？