Tait計算 - 国立公園

Tait計算

Tait calculus

#1階論理

言語$ L

$ x, y, z, ...は変項を意味する

$ t, u, v, ...は項を意味する

$ \mathrm{FV}(t), \mathrm{FV}(\Gamma)は$ t, \Gammaの自由変項の集合を意味する

有限集合$ \Gamma, \Delta, ..., その要素$ a, b, ...について以下の略記法を用いる

$ a, b, c, ... \coloneqq \{a,b,c,...\}

$ a, \Gamma \coloneqq \{a\} \cup \Gamma

$ \Gamma, \Delta \coloneqq \Gamma \cup \Delta

論理式

言語$ LのTait計算の論理式$ \mathrm{Formula}(L)を以下のように定義する

$ \top, \botは論理式

Proof Theory: The First Step into Impredicativityでは$ \top, \botは用いていない

$ Lの項$ t_1, ..., t_k, アリティ$ kの関係記号$ r \in Lについて

$ r(t_1, ..., t_k), $ \bar r(t_1, ..., t_k)は論理式

$ \varphi, \psiが論理式ならば

$ \varphi \land \psi, \varphi \lor \psiは論理式

変項$ xについて$ (\exists x)\varphi, (\forall x)\varphiは論理式

否定

論理式の否定$ (\lnot) \colon \mathrm{Formula}(L) \to \mathrm{Formula}(L)を以下のように帰納的に定義する

$ \lnot \top \coloneqq \bot

$ \lnot \bot \coloneqq \top

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

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

$ \lnot(\varphi \land \psi) \coloneqq \lnot \varphi \lor \lnot \psi

$ \lnot(\varphi \lor \psi) \coloneqq \lnot \varphi \land \lnot \psi

$ \lnot((\forall x)\varphi) \coloneqq (\exists x) \lnot\varphi

$ \lnot((\exists x)\varphi) \coloneqq (\forall x) \lnot\varphi

論理式$ \varphi の変項$ x の項$ t への書き換えを$ \varphi[x \mapsto t] と表記する

導出関係

論理式の有限集合$ \Gammaについて導出関係$ \vdash_\mathsf{T} \Gammaを定義する

$ (\textsf{AxL})\colon \vdash_\mathsf{T} r(t_1, ..., t_k), \bar r(t_1, ..., t_k), \Gamma

$ (\top)\colon \vdash_\mathsf{T} \top, \Gamma

$ (\land) \colon \vdash_\mathsf{T} \varphi, \Gamma \implies \vdash_\mathsf{T} \psi, \Gamma \implies \vdash_\mathsf{T} \varphi \land \psi, \Gamma

$ (\lor\textsf{-L})\colon \vdash_\mathsf{T} \varphi, \Gamma \implies \vdash_\mathsf{T} \varphi \lor \psi, \Gamma

$ (\lor\textsf{-R})\colon \vdash_\mathsf{T} \psi, \Gamma \implies \vdash_\mathsf{T} \varphi \lor \psi, \Gamma

$ (\lor\textsf{-L}), (\lor\textsf{-R})の代わりに以下を用いても（おそらく）よい

$ (\lor)\colon \vdash_\mathsf{T} \varphi, \psi, \Gamma \implies \vdash_\mathsf{T} \varphi \lor \psi, \Gamma

Tait計算の完全性定理の証明を考えるとこのほうが本質的だと思う

$ (\forall) \colon \vdash_\mathsf{T} \varphi, \Gamma \implies \vdash_\mathsf{T} (\forall x)\varphi, \Gamma

ただし$ x \notin \mathrm{FV}(\Gamma)

$ (\exists) \colon \vdash_\mathsf{T} \varphi[x \mapsto t], \Gamma \implies \vdash_\mathsf{T} (\exists x)\varphi, \Gamma

$ (\textsf{Cut})\colon \vdash_\mathsf{T} \varphi, \Gamma \implies \vdash_\mathsf{T} \lnot \varphi, \Delta \implies \vdash_\mathsf{T} \Gamma,\Delta

カット除去定理で除去可能

素朴な解釈：

$ \vdash_\mathsf{T} \varphi_1, ..., \varphi_kは$ \varphi_1, ..., \varphi_kのいずれかが成り立つことを意味する

実際$ \vdash_\mathsf{T} \varphi_1,...,\varphi_k \iff \vdash_\mathsf{T} \bigvee_i \varphi_i

定義

理論$ T, 論理式の有限集合$ \Gammaについて以下を満たすとき$ T \vdash_\mathsf{T} \Gammaとかく

有限集合$ \psi_1, ..., \psi_k \in T が存在して$ \vdash_\mathsf{T} \lnot\psi_1, ..., \lnot \psi_k, \Gamma

特に$ \Gamma = \{\varphi\}のとき$ T \vdash \varphiと書く

定理：弱化

$ \Gamma \subseteq \Deltaならば$ \vdash_\mathsf{T} \Gamma \implies \vdash_\mathsf{T} \Delta

Proof.

$ \vdash_\mathsf{T} \Gammaの構成に関する帰納法

❏

定理

任意の論理式$ \varphiについて

$ \vdash_\mathsf{T} \varphi, \lnot \varphi,\Gamma

Proof.

$ \varphiの構成に関する帰納法

❏

参考文献

Proof Theory: The First Step into Impredicativity