Tait計算の完全性定理

おおまかな証明方針はProof Theory: The First Step into Impredicativityに沿っているが探索木の定義など一部異なる

主補題

$ Lの理論$ T

次が成り立つ

探索木$ (\prec^{T,\Gamma})が整礎関係ならば$ T \vdash_\mathsf{T} \Gamma

探索木$ (\prec^{T,\Gamma})が整礎関係でないならば次を満たす構造$ \mathfrak{M}が存在する

$ \mathfrak{M} \models T

任意の$ \varphi \in \Gamma について$ \lnot \mathfrak{M} \models \varphi

Proof.

完全性定理

$ T \vDash \varphiならば$ T \vdash \varphi

Proof.

$ \Gamma \coloneqq \{\varphi\}とする

主補題より$ T \vdash \varphiまたは$ \mathfrak{M}が存在して$ \mathfrak{M} \models T, $ \lnot \mathfrak{M} \models \varphi

後者は仮定に反する