探索木 - 国立公園

探索木

search tree

#Tait計算

注意

おそらく一般的な定義ではない

$ Lは可算言語であると仮定する

可算個の集合$ A の要素の自然数へのコード化を$ a \mapsto {\ulcorner a \urcorner}と書く

対関数を$ \braket{\_, \_}\colon \N^2 \to \Nと書く

Tait計算の略記法を用いる

論理式の有限集合$ \Gamma

理論$ T

定義：ラベル

ラベルの集合$ \Lambda^Tを以下のように定義する

$ \Lambda^T \coloneqq \{\textsf{AxL}_{r, t_1, ..., t_k}\ |\ r \in L, t_1, ..., t_k \in \mathrm{Term}(L)\}

$ {} \cup \{\mathsf{Top}\}

$ {} \cup \{\mathsf{And}_{\varphi, \psi}\ |\ \varphi, \psi \in \mathrm{Formula}(L)\}

$ {} \cup \{\mathsf{Or}_{\varphi, \psi}\ |\ \varphi, \psi \in \mathrm{Formula}(L)\}

$ {} \cup \{\mathsf{Forall}_{\varphi}\ |\ \varphi \in \mathrm{Formula}(L)\}

$ {} \cup \{\mathsf{Exists}_{\varphi, t}\ |\ \varphi \in \mathrm{Formula}(L), t \in \mathrm{Term}(L)\}

$ {} \cup \{\mathsf{Id}_{\psi}\ |\ \psi \in T\}

定義よりこれは可算集合なので自然数にコードできる

$ \Lambda^Tは公理$ TのTait計算の演繹規則のラベルを意味する：

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

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

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

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

$ (\mathsf{Forall}_{\varphi}) \colon T \vdash_\mathsf{T} \varphi[x \mapsto v_\Gamma], \Gamma \implies T \vdash_\mathsf{T} (\forall x)\varphi, \Gamma

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

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

$ (\mathsf{Id_\psi})\colon T \vdash_\mathsf{T} \lnot \psi, \Gamma \implies T \vdash_\mathsf{T} \Gamma

ただし$ \psi \in T

定義：$ (\prec^T_s)

$ s \in \Nについて$ (\prec^T_s) \subseteq \mathcal{P}_{<\omega}(\mathrm{Formula}(L)) \times \mathcal{P}_{<\omega}(\mathrm{Formula}(L))を定義する

$ r(t_1, ... t_k), \bar r(t_1, ... t_k) \in \Delta, $ s = {\braket{\ulcorner \mathsf{AxL}_{r, t_1, ..., t_k} \urcorner, i}}ならば

任意の$ \Delta'について$ \Delta' \nprec^T_s \Delta

$ \top \in \Delta, $ s = \braket{\ulcorner \mathsf{Top} \urcorner, i}ならば

任意の$ \Delta'について$ \Delta' \nprec^T_s \Delta

$ \varphi \land \psi \in \Delta, $ s = {\braket{\ulcorner \mathsf{And}_{\varphi,\psi} \urcorner, i}}ならば

$ \varphi,\Delta \prec^T_s \Delta

$ \psi,\Delta \prec^T_s \Delta

$ \varphi \lor \psi \in \Delta, $ s = {\braket{\ulcorner \mathsf{Or}_{\varphi, \psi} \urcorner, i}}ならば

$ \varphi, \psi, \Delta \prec^T_s \Delta

$ (\forall x) \varphi \in \Delta , $ s = {\braket{\ulcorner \mathsf{Forall}_{\varphi} \urcorner, i}}ならば

$ \varphi[x \mapsto v_\Delta], \Delta \prec^T_s \Delta

$ v_\Deltaは$ v_\Delta \notin \mathrm{FV}(\Delta)を満たす変項

$ (\exists x) \varphi \in \Delta , $ s = {\braket{\ulcorner \mathsf{Exists}_{\varphi, t} \urcorner, i}}ならば

$ \varphi[x \mapsto t], \Delta \prec^T_s \Delta

$ \psi \in T, $ s = {\braket{\ulcorner \mathsf{Id}_{\psi} \urcorner, i}}ならば

$ \lnot \psi, \Delta \prec^T_s \Delta

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

$ \Delta \prec^T_s \Delta

定義

$ \Gammaについて論理式の有限集合上の関係$ (\prec^{T, \Gamma}) \subseteq \mathcal{P}_{<\omega}(\mathrm{Formula}(L)) \times \mathcal{P}_{<\omega}(\mathrm{Formula}(L))を定義する

$ \Delta_{s+1} \prec^T_s \Delta_s \prec^T_{s-1} ... \prec^T_1\Delta_1 \prec^T_0 \Delta_0 = \Gammaを満たす$ s, $ \Delta_1, ..., \Delta_{s+1}が存在するとき$ \Delta_{s+1} \prec^{T, \Gamma} \Delta_s

$ (\prec^{T,\Gamma})の値域の元について$ sをその$ \mathrm{rank}(\Delta)と書く

定理

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

定理

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