Tait計算の完全性定理
主補題
次が成り立つ
探索木$ (\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
後者は仮定に反する