Gödel-McKinsey-Tarskiの定理
命題論理の論理式から命題様相論理の論理式に写す写像$ \cdot^G \colon \mathrm{Form}_\mathsf{P\Lambda} \to \mathrm{Form}_\mathsf{M\Lambda}を以下のように定める．
$ p^G \mapsto \Box p
$ (\lnot \varphi)^G \mapsto \Box \lnot \varphi^G
$ (\varphi \land \psi)^G \mapsto \varphi^G \land \psi^G
$ (\varphi \lor \psi)^G \mapsto \varphi^G \lor \psi^G
$ (\varphi \to \psi)^G \mapsto \Box(\varphi^G \to \psi^G)
$ \vdash_\mathbf{iPL} \iff \vdash_\mathbf{S4} \varphi^G
ただし$ \vdash_{\mathbf{iPL}}は直観主義命題論理で証明可能，$ \vdash_{\mathbf{\mathbf{S4}}}は様相論理S4で証明可能 proof
下記のLem 2, Lem 3より
Memo
多分，以下の文献に由来する．
McKenseyとTarskiの方はよくわかっていない．1944年でヒットするのはこれだが，これに書いてあるのか？
以下の証明は非常に概略だけ示している．
Prop
Gödel翻訳した論理式は必ず$ \Boxの中に閉じた（Boxedな）なんらかの論理式と証明体系上で同値である．すなわち，
任意の$ Aに対して次の$ A'が存在する．$ \vdash A^G \leftrightarrow \Box A'
proof
次のことに注意すれば明らか．
$ \vdash \Box A \land \Box B \leftrightarrow \Box(A \land B)
$ \vdash \Box A \lor \Box B \leftrightarrow \Box(A \lor B)
Lem.1
$ Aは$ \bf iPLの論理式とする．$ \vdash_\mathbf{K4} A^G \to \Box A^G
proof
直観主義論理の論理式の帰納法．
Lem.2: $ \implies
$ Aは$ \bf iPLの論理式とする．$ \vdash_\mathbf{iPL} A \implies \vdash_\mathbf{S4} A^G
proof
公理の場合
構文論上で（すなわちHilbert演繹体系上で）やると非常に煩雑だが，簡易的にはおそらく次の事実を確かめれば良い．
例えば公理$ \vdash_\mathbf{iPL} A \to (B \to A)であるが，これをGödel翻訳した$ \vdash_\mathbf{S4} \lbrack A \to (B \to A) \rbrack^Gを確かめるとする．
$ \lbrack A \to (B \to A) \rbrack^G \equiv \Box(A^G \to \Box(B^G \to A^G))である．
ここでPropより任意のGödel変換後の論理式がBoxedであることに注意して$ A^G \equiv \Box A', B^G \equiv \Box B'で置き換える．
$ \Box(\Box A' \to \Box(\Box B' \to \Box A'))
この論理式が$ \bf S4上の定理であることを確かめれば良い．
例えばこれはwo/tpgを使って確かめると確かに定理となる． memo
論理式を置き換えずに$ \Box(A^G \to \Box(B^G \to A^G))が$ \bf S4上の定理か確かめようとすると失敗する．
事実この例は$ \bf S4の定理ではない．
モーダスポネンスの場合
$ \vdash_\mathbf{iPL} A \to Bかつ$ \vdash_\mathbf{iPL} Aによって$ \vdash_\mathbf{iPL} Bが得られたとする．
帰納法の仮定より
$ \vdash_\mathbf{S4} \Box (A^G \to B^G)
公理Kより$ \vdash_\mathbf{S4} \Box A^G \to \Box B^G
$ \vdash_\mathbf{S4} A^G
必然化より$ \vdash_\mathbf{S4} \Box A^G
モーダスポネンスより$ \vdash_\mathbf{S4} \Box B^G
公理Tより$ \vdash_\mathbf{S4} B^G
memo
Lem 3: $ \impliedby
$ Aは$ \bf iPLの論理式とする．$ \vdash_\mathbf{S4} A^G \implies \vdash_\mathbf{iPL} A
proof
対偶：$ \nvdash_\mathbf{iPL} A \implies \nvdash_\mathbf{S4} A^Gを示す
完全性定理より$ Aを妥当としない$ \mathcal{M}^I := \lang W, \mathbin{\leq}, V \rangと世界$ w \in Wが存在する．
すなわち$ w \nVdash^{\mathcal{M}^I} A
$ \mathcal{M}^I := \lang W, \mathbin{\leq}, V \rangをそのまま$ \bf S4のモデル$ \mathcal{M} := \lang W, \mathbin{\leq},V \rangとする．
$ \mathbin{\leq}は直観主義論理のモデル由来の，すなわち推移的かつ反射的なので，$ \bf S4のモデルとしても良い．
正確にはフレームが$ \lang M,\mathbin{\leq} \rang \in \mathbb{F}(\mathbf{S4})である
今，（直観主義論理の）論理式の帰納法を回すことで次のことが成り立つことが確認される．
任意の$ B,v \in Wで$ v \Vdash^{\mathcal{M}^I} B \iff v \Vdash^{\mathcal{M}} B^G
よって$ \nVdash^{\mathcal{M}} A^Gが成り立つ．よって健全性定理より$ \nvdash_\mathbf{S4} A^Gが得られる．よってOK
memo