Tait計算の完全性定理：意味論的主補題

semantic main lemma

#Tait計算

#補題

探索木$ (\prec^{T,\Gamma})が整礎関係でないと仮定する

整礎でないので無限降下列$ \Gamma_1, \Gamma_2, ...が存在する

$ ... \prec^T_2 \Gamma_2 \prec^T_1 \Gamma_1 \prec^T_0 \Gamma_0 \coloneqq \Gamma

弱Kőnigの補題

無限降下列の和を$ \Gamma_\omegaと書く

$ \Gamma_\omega \coloneqq \bigcup_i \Gamma_i

補題1

$ \Gamma_sは単調

$ \Gamma_s \subseteq \Gamma_{s+1}より

$ \top \notin \Gamma_\omega

Proof.

$ \top \in \Gamma_sならば$ s \le \braket{\ulcorner \mathsf{Top} \urcorner, i}を満たす$ iが存在して

$ \Gamma_{\braket{\ulcorner \mathsf{Top} \urcorner, i}+1} \prec^T_{\braket{\ulcorner \mathsf{Top} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{Top} \urcorner, i}}

$ \top \in \Gamma_s \subseteq \Gamma_{\braket{\ulcorner \mathsf{Top} \urcorner, i}}だからこれは$ \prec^T_{\braket{\ulcorner \mathsf{Top} \urcorner, i}}の定義に反する

❏

$ r(t_1, ..., t_k) \notin \Gamma_\omegaまたは$ \bar r(t_1, ..., t_k) \notin \Gamma_\omega

Proof.

$ r(t_1, ..., t_k) \in \Gamma_s, $ \bar r(t_1, ..., t_k) \in \Gamma_{s'}と仮定する

$ \max(s,s') \le \braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}を満たす$ iが存在して

$ \Gamma_{\braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}+1} \prec^T_{\braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}}

$ r(t_1, ..., t_k), \bar r(t_1, ..., t_k) \in \Gamma_{\max(s, s')} \subseteq \Gamma_{\braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}}よりこれは$ \prec^T_{\braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}}の定義に反する

❏

$ \varphi \land \psi \in \Gamma_\omegaならば$ \varphi \in \Gamma_\omegaまたは$ \psi \in \Gamma_\omega

$ \varphi \land \psi \in \Gamma_sならば$ s \le \braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}を満たす$ iが存在して

$ \Gamma_{\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}+1} \prec^T_{\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}}

$ \Gamma_{\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}+1} = \varphi,\Gamma_{\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}}または$ \psi,\Gamma_{\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}}

よって$ \varphi \in \Gamma_\omegaまたは$ \psi \in \Gamma_\omega

❏

$ \varphi \lor \psi \in \Gamma_\omegaならば$ \varphi, \psi \in \Gamma_\omega

$ \varphi \lor \psi \in \Gamma_sならば$ s \le \braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}を満たす$ iが存在して

$ \Gamma_{\braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}+1} = \varphi, \psi, \Gamma_{\braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}} \prec^T_{\braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}}

よって$ \varphi, \psi \in \Gamma_\omega

❏

$ (\forall x)\varphi \in \Gamma_\omegaならばある変項$ vについて$ \varphi(v) \in \Gamma_\omega

$ (\forall x)\varphi \in \Gamma_sならば$ s \le \braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}を満たす$ iが存在して

$ \Gamma_{\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}+1} = \varphi(v_{\Gamma_{\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}}}),\Gamma_{\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}} \prec^T_{\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}}

よって$ \varphi(v_{\Gamma_{\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}}}) \in \Gamma_\omega

❏

$ (\exists x)\varphi \in \Gamma_\omegaならば任意の項$ tについて$ \varphi(t) \in \Gamma_\omega

$ (\exists x)\varphi \in \Gamma_sならば$ s \le \braket{\ulcorner \mathsf{Exists}_{\varphi, t} \urcorner, i}を満たす$ iが存在して

$ \Gamma_{\braket{\ulcorner \mathsf{Exists}_{\varphi,t} \urcorner, i}+1} = \varphi(t), \Gamma_{\braket{\ulcorner \mathsf{Exists}_{\varphi,t} \urcorner, i}} \prec^T_{\braket{\ulcorner \mathsf{Exists}_{\varphi,t} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{Exists}_{\varphi,t} \urcorner, i}}

よって$ \varphi(t) \in \Gamma_\omega

❏

$ \psi \in Tならば$ \lnot\psi \in \Gamma_\omega

$ \Gamma_{\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, 0} + 1} \prec^T_{\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, i}} \Gamma_{\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, 0}}

より$ \Gamma_{\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, 0} + 1} = \lnot\psi, \Gamma_{\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, 0}}

よって$ \lnot \psi \in \Gamma_\omega

❏

定義

$ L構造$ \mathfrak{M}^{\Gamma_\omega}を定義する

$ Lは等号を含まない点に注意

$ |\mathfrak{M}^{\Gamma_\omega}| \coloneqq \mathrm{Term}(L)

$ f^{\mathfrak{M}^{\Gamma_\omega}}(t_1, ..., t_k) \coloneqq f(t_1,...,t_k)

$ r^{\mathfrak{M}^{\Gamma_\omega}}(t_1,...,t_k) \iff \bar r(t_1,...,t_k) \in \Gamma_\omega

$ \mathfrak{M}^{\Gamma_\omega}は$ Lの$ \lnot\Gamma_\omegaの真理値を持つ項モデル

変項の割当$ \Phiを以下のように定義する

$ \Phi(x) \coloneqq x

補題2

$ \varphi \in \Gamma_\omega \implies \mathfrak{M}^{\Gamma_\omega} \models \lnot \varphi[\Phi]

Proof.

$ \varphiの複雑性に関する帰納法

$ \top

補題1より$ \top \notin \Gamma_\omega

$ \bot

$ \mathfrak{M}^{\Gamma_\omega} \models \top

$ r(t_1,...,t_k)

$ r(t_1,...,t_k) \in \Gamma_\omegaなので補題1より$ \bar r(t_1,...,t_k) \notin \Gamma_\omega

また$ \mathfrak{M}^{\Gamma_\omega} \models \lnot r(t_1,...,t_k) \iff \bar r(t_1,...,t_k) \notin \Gamma_\omega

$ \bar r(t_1,...,t_k)

$ \mathfrak{M}^{\Gamma_\omega} \models \lnot \bar r(t_1,...,t_k) \iff \bar r(t_1,...,t_k) \in \Gamma_\omegaより

$ \varphi \land \psi

補題1より$ \varphi \in \Gamma_\omegaまたは$ \psi \in \Gamma_\omega, $ \varphi \in \Gamma_\omegaとして一般性を失わない

帰納法の仮定より$ \mathfrak{M}^{\Gamma_\omega} \models \lnot \varphi

よって$ \mathfrak{M}^{\Gamma_\omega} \models \lnot(\varphi \land \psi) \iff \mathfrak{M}^{\Gamma_\omega} \models \lnot \varphi \lor \lnot \psi

$ \varphi \lor \psi

補題1より$ \varphi, \psi \in \Gamma_\omega

帰納法の仮定より$ \mathfrak{M}^{\Gamma_\omega} \models \lnot \varphi \land \lnot \psi

$ (\forall x)\varphi

補題1より$ \varphi(v) \in \Gamma_\omega

帰納法の仮定より$ \mathfrak{M}^{\Gamma_\omega} \models \lnot \varphi(v), よって$ \mathfrak{M}^{\Gamma_\omega} \models \lnot(\forall x)\varphi(x)

$ (\exists x)\varphi

補題1より任意の$ t \in \mathfrak{M}^{\Gamma_\omega}について$ \varphi(t) \in \Gamma_\omega

帰納法の仮定より$ \mathfrak{M}^{\Gamma_\omega} \models \lnot\varphi(t)

よって$ \mathfrak{M}^{\Gamma_\omega} \models (\forall x)\lnot \varphi(x) \iff \mathfrak{M}^{\Gamma_\omega} \models \lnot(\exists x)\varphi(x)

❏

定理：意味論的主補題

以下が成り立つ

1. $ \mathfrak{M}^{\Gamma_\omega} \models T

2. $ \varphi \in \Gamma \implies \mathfrak{M}^{\Gamma_\omega} \models \lnot \varphi[\Phi]

Proof.

補題1と補題2より

$ \Gamma \subseteq \Gamma_\omegaと補題2より

❏