直観主義論理: 可能世界意味論に関する完全性定理

まず言語$\L$が可算である場合を考える。このとき$\Fml(\L\cup C)$が可算無限集合となることに注意し、これに属する論理式を$\qty{\zeta_n\mid n\in\N}$と添字づける。

最初に、以下の主張を$n$に関する帰納法で示す。

$\Gamma_0\defeq\Gamma~(\sube\Fml(\L))$とすると、仮定よりこれは2つの性質を満たす。

次に、条件(a),(b)を満たすような$\Gamma_n$の存在を仮定する。まず、以下の条件を考える。

排中律を用いて、$(\ast')$が成り立つか否かで場合分けする。

(case 1) $(\ast')$が成り立たない場合: $\Gamma_{n+1}\defeq\Gamma_n$とする(確かに(a),(b)を満たす)。

(case 2) $(\ast')$が成り立つ場合

$(\ast')$の2条件を満たす$\zeta_m$の中で、添字が最小であるようなものを$\zeta_\overline{m}$とする。$\zeta_\overline{m}$に対して(c)と(d)のどちらが成り立つかで場合分けする。

(case 2-1) (c)が成り立つ場合

このとき、$\Gamma_n,\psi\vdash\vphi$と$\Gamma_n,\theta\vdash\vphi$のどちらか一方は成り立たない。実際、両方が成り立つと仮定すると、$\Gamma_n\vdash\psi\lor\theta$より以下の導出が構成でき、帰納法の仮定($\Gamma_n\nvdash\vphi$)に矛盾する。

$\Gamma_n,\psi\nvdash\vphi$である場合、$\Gamma_{n+1}\defeq\Gamma_n\cup\qty{\psi}$と定義すれば、$\Gamma_{n+1}$は条件(a),(b)を満たす。もう一方の場合も同様。

(case 2-2) (d)が成り立つ場合

このとき、$\Gamma_n\cup\qty{\vphi}$に含まれない定数$c\in C$を1つとる(条件(b)よりそのような定数は存在する)。すると、$\Gamma_n,\psi[x:=c]\nvdash\vphi$である。これを示すために、$\Gamma_n,\psi[x:=c]\vdash\psi$を仮定しよう。いま$c$は$\Gamma\cup\qty{\vphi}$に登場しない定数なので、これを$\Gamma\cup\qty{\vphi}$に登場しない変数$y$に置換しても同様に導出は構成可能である。これと$\Gamma\vdash\exists x.\psi~(\equiv\exists y.\psi[x:=y])$より以下の導出が構成でき、帰納法の仮定($\Gamma_n\nvdash\vphi$)に矛盾する。

よって、$\Gamma_{n+1}\defeq\Gamma_n\cup\qty{\psi[x:=c]}$と定義すれば、$\Gamma_{n+1}$は条件(a),(b)を満たす。

以上で$(\ast)$が示された。ここで、$\Gamma'\defeq\bigcup_{n\in\N}\Gamma_n$と定義する。この$\Gamma'$が所期の条件を満たすことを確認しよう。

• $\Gamma_0=\Gamma$より、$\Gamma\sube\Gamma'$。
• $\Gamma'\vdash\vphi$を仮定すると、ある$n\in\N$に対して$\Gamma_n\vdash\vphi$となり、(a)に矛盾する。よって$\Gamma'\nvdash\vphi$。
• $\Gamma'$が$\L\cup C$に対してプライムであることは、以下のように示せる。
  • $\Gamma'\vdash\psi\lor\theta$を仮定する。
    • このとき、ある$n\in\N$に対して$\Gamma_n\vdash\psi\lor\theta$である。
    • $\psi\lor\theta$の添字を$m$とする(i.e., $\zeta_m\equiv\psi\lor\theta$)。増大列$(\Gamma_n)_{n\in\N}$の構成方法から、最初から高々$m+1$ステップ目以内に$\psi\lor\theta$が(case 1)の対象になる。すなわち、ある$1\leq i\leq m+1$に対して$\Gamma_{n+i}\vdash\psi$または$\Gamma_{n+i}\vdash\theta$。
    • よって、$\Gamma'\vdash\psi$または$\Gamma'\vdash\theta$が成り立つ。
  • $\Gamma'\vdash\exists x.\psi$を仮定した場合も同様。

最後に、言語$\L$が不可算濃度を持つ場合について、証明の概略のみ述べる。整列可能性定理を用いて、論理式の集合$\Fml(\L\cup C)$を整列順序により順序付ける。これに基づいて、$(\ast)$と同様の主張を超限帰納法により示せばよい。

$n$を任意にとり、$\psi$の構成に関する帰納法で示す。状態$\tuple{\Delta,C_k}$($k\geq n$)を任意にとる。

• $\psi\equiv Pt_1\ldots t_n$(原子論理式)の場合: 構造・割り当ての定義より明らか。
• $\vphi\equiv\top$の場合: $(\top I)$より$\Delta\vdash\top$なので成立。
• $\psi\equiv\bot$の場合: $\M_\L$の定義より$\Delta$は無矛盾なので成立。
• $\psi\equiv\theta\land\zeta$の場合
  $$ \begin{align*} \tuple{\Delta,k}\vDash_\id \theta\land\zeta \iff& \tuple{\Delta,k}\vDash_\id \theta\And\tuple{\Delta,k}\vDash_\id \zeta\\[5pt] \iff& \Delta\vdash\theta\And\Delta\vdash\zeta\quad(\because~\text{帰納法の仮定})\\[5pt] \iff& \Delta\vdash\theta\land\zeta\quad(\because~(\land I),(\land E)) \end{align*} $$
• $\psi\equiv\theta\lor\zeta$の場合
  $$ \begin{align*} \tuple{\Delta,k}\vDash_\id \theta\lor\zeta \iff& \tuple{\Delta,k}\vDash_\id \theta\Or\tuple{\Delta,k}\vDash_\id \zeta\\[5pt] \iff& \Delta\vdash\theta\Or\Delta\vdash\zeta\quad(\because~\text{帰納法の仮定})\\[5pt] \iff& \Delta\vdash\theta\lor\zeta\quad(\because~(\lor I),\text{プライム性}) \end{align*} $$
• $\psi\equiv\exists x.\theta$の場合
  $$ \begin{align*} \tuple{\Delta,k}\vDash_\id \exists x.\theta \iff& \Exists t\in\Term(\L_k).\tuple{\Delta,k}\vDash_{\id[x\mapsto t]}\theta \\[5pt] \iff& \Exists t\in\Term(\L_k).\tuple{\Delta,k}\vDash_\id\theta[x:=t]\quad(\because~\text{割り当てに関する補題})\\[5pt] \iff& \Exists t\in\Term(\L_k).\Delta\vdash\theta[x:=t]\quad(\because~\text{帰納法の仮定})\\[5pt] \iff& \Delta\vdash\exists x.\theta\quad(\because~(\exists I),\text{プライム性}) \end{align*} $$
• $\psi\equiv\theta\to\zeta$の場合
  • $(\Rarr)$: 対偶を示すために、$\Delta\nvdash\theta\to\zeta$を仮定する。
    • $({\to}I)$(の対偶)より$\Delta,\theta\nvdash\zeta$であるから、ヘンキン拡張により、$\Delta'\supe\Delta\cup\qty{\theta}$と$\Delta'\nvdash\zeta$を満たすプライムな$\Delta'\sube\Fml(\L_{k+1})$が得られる。このとき、$\theta\in\Delta'$より$\Delta'\vdash\theta$である。
    • よって帰納法の仮定から、$\tuple{\Delta',k+1}\vDash_\id\theta$かつ$\tuple{\Delta',k+1}\nvDash_\id\zeta$が言える⁴。
    • 以上と$\tuple{\Delta',k+1}\geq\tuple{\Delta,k}$より、充足関係の定義から$\tuple{\Delta,k}\nvDash_\id\theta\to\zeta$。
  • $(\Larr)$: $\Delta\vdash\theta\to\zeta$を仮定する。
    • 状態$\tuple{\Delta',\ell}(\geq\tuple{\Delta,k})$を任意に取り、$\tuple{\Delta',\ell}\vDash_\id\theta$を仮定する。
    • このとき帰納法の仮定より$\Delta'\vdash\theta$。さらに$\Delta'\supe\Delta$より$\Delta'\vdash\theta\to\zeta$なので、$({\to}E)$より$\Delta'\vdash\zeta$となり、再び帰納法の仮定より$\tuple{\Delta',\ell}\vDash_\id\zeta$となる。
    • 以上より、充足関係の定義から$\tuple{\Delta,k}\vDash_\id\theta\to\zeta$。
• $\psi\equiv\forall x.\theta$の場合
  • $(\Rarr)$: 対偶を示すために、$\Delta\nvdash\forall x.\theta$を仮定する。
    • $c\in C_{k+1}$を1つとる(任意でよい)。定義より$c\notin\Term(\L_{k})$である。
    • まず$\Delta\nvdash\theta[x:=c]$である。実際、$\Delta\vdash\theta[x:=c]$と仮定すると、$c$は$\Delta$に出現しないので$\Delta$に出現しない変数$y$に置換でき$\Delta\vdash\theta[x:=y]$となるが、これは$(\forall I)$から$\Delta\vdash\forall x.\theta$を導き矛盾する。
    • このときヘンキン拡張により、$\Delta'\supe\Delta$と$\Delta'\nvdash\theta[x:=c]$を満たすプライムな$\Delta'\sube\Fml(\L_{k+2})$が得られる。帰納法の仮定より、$\tuple{\Delta',k+2}\nvDash_\id\theta[x:=c]$が言えて、さらに割り当てに関する補題から$\tuple{\Delta',C_{k+2}}\nvDash_{\id[x\mapsto c]}\theta$。
    • 以上と$\tuple{\Delta',C_{k+2}}\geq\tuple{\Delta,C_k},~c\in\Term(\L_{k+2})$より、充足関係の定義から$\tuple{\Delta,C_k}\nvDash_\id\forall x.\theta$。
  • $(\Larr)$: $\Delta\vdash\forall x.\theta$を仮定する
    • 状態$\tuple{\Delta',\ell}(\geq\tuple{\Delta,k})$および$t\in\Term(\L_\ell)$を任意にとる。
    • $\Delta'\supe\Delta$より$\Delta'\vdash\forall x.\theta$なので、$(\forall E)$より$\Delta'\vdash\theta[x:=t]$となる。帰納法の仮定より$\tuple{\Delta',\ell}\vDash_\id\theta[x:=t]$である。これと割り当てに関する補題より$\tuple{\Delta',\ell}\vDash_{\id[x\mapsto t]}\theta$。
    • 以上より、充足関係の定義から$\tuple{\Delta,k}\vDash_\id\forall x.\theta$。

対偶を示す。$\Gamma\nvdash\vphi$を仮定すると、ヘンキン拡張により、$\Gamma'\supe\Gamma$と$\Gamma'\nvdash\vphi$を満たすプライムな$\Gamma'\sube\Fml(\L_0)$が得られる。このとき真理補題より、

• $\tuple{\Gamma',0}\vDash_\id\Gamma\quad(\because\Gamma'\supe\Gamma)$
• $\tuple{\Gamma',0}\nvDash_\id\vphi\quad(\because\Gamma'\nvdash\vphi)$

このようなモデル・状態・付値の存在により、$\Gamma\nvDash\vphi$が示された。