Tait計算の完全性定理：統語論的主補題

syntactic main lemma

#補題

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

補題

$ \Deltaが$ \prec^{T, \Gamma}の値域ならば$ T \vdash_\mathsf{T} \Delta

Proof.

$ (\prec^{T,\Gamma})上の帰納法によって証明する

$ \Delta' \prec^{T, \Gamma} \Deltaとなる任意の$ \Delta'について$ T \vdash_\mathsf{T} \Delta'と仮定する

$ r(t_1,...,t_k), \bar r(t_1,...,t_k) \in \Delta, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{AxL}_{r,t_1,...,t_k} \urcorner, i}のとき

$ \Deltaは$ (\mathsf{AxL})で証明可能

$ \top \in \Delta, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{Top} \urcorner, i}のとき

$ \Deltaは$ (\mathsf{Top})で証明可能

$ \varphi \land \psi \in \Delta, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}のとき

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

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

仮定より$ T \vdash_\mathsf{T} \varphi, \Delta, $ T \vdash_\mathsf{T} \psi, \Deltaより$ T \vdash_\mathsf{T} \varphi \land \psi, \Delta, よって$ T \vdash_\mathsf{T} \Delta

$ \varphi \lor \psi \in \Delta, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}のとき

$ \varphi,\psi,\Delta \prec^T_{\braket{\ulcorner \mathsf{Or}_{\varphi,\psi} \urcorner, i}} \Delta

仮定より$ T \vdash_\mathsf{T} \varphi, \psi,\Deltaより$ T \vdash_\mathsf{T} \varphi \lor \psi, \Delta. よって$ T \vdash_\mathsf{T} \Delta

$ (\forall x)\varphi \in \Delta, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}のとき

$ \varphi[x \mapsto v_\Delta],\Delta \prec^T_{\braket{\ulcorner \mathsf{Forall}_{\varphi,t} \urcorner, i}} \Delta

仮定より$ T \vdash_\mathsf{T} \varphi[x \mapsto v_\Delta],\Delta より$ T \vdash_\mathsf{T} (\forall x)\varphi, \Delta . よって$ T \vdash_\mathsf{T} \Delta

$ (\exists x)\varphi \in \Delta, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{Exists}_{\varphi,t} \urcorner, i}のとき

$ \varphi[x \mapsto t],\Delta \prec^T_{\braket{\ulcorner \mathsf{Exists}_{\varphi,t} \urcorner, i}} \Delta

仮定より$ T \vdash_\mathsf{T} \varphi[x \mapsto t],\Delta より$ T \vdash_\mathsf{T} (\exists x)\varphi, \Delta . よって$ T \vdash_\mathsf{T} \Delta

$ \psi \in T, $ \mathrm{rank}(\Delta) = \braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, i}のとき

$ \lnot\psi,\Delta \prec^T_{\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, i}} \Delta

仮定より$ T \vdash_\mathsf{T} \lnot\psi,\Delta より$ T \vdash_\mathsf{T} \Delta

上記のいずれの条件にも該当しないとき

$ \Delta \prec^T_{\mathrm{rank}(\Delta)} \Delta

仮定より$ T \vdash_\mathsf{T} \Delta

❏

系：統語論的主補題

$ T \vdash_\mathsf{T} \Gamma

定理：非構成的カット除去定理

上の補題は$ (\mathsf{Cut})を用いずに証明している

従ってTait計算の完全性定理と健全性定理を踏まえると$ T \vdash^{\mathsf{(Cut)}}_\mathsf{T} \varphiならば$ T \models \varphiだから$ T \vdash _\mathsf{T} \varphi

よって$ (\mathsf{Cut})は除去できる