【数学・論理学】演繹定理

公理系と仮定 $P$ から命題 $Q$ の証明ができる(これを$P\vdash Q$ で表す)とき、「 $Q$ は $P$ の演繹である」「 $Q$ は $P$ から演繹可能である」という。

これについてエルブランによる次の演繹定理が成り立つ:

$P\vdash Q$ ならば、 $\vdash P\rightarrow Q$

証明は演繹の長さの帰納法でできる。

$P\vdash\lnot\lnot P$を例としてみていく。まずは証明図を書く。

\begin{align*} \text{公理}&:P\rightarrow(\lnot P\rightarrow P)\\ \text{仮定}&:P\\ \text{推論}&:\lnot P\rightarrow P\\ \text{公理}&:\lnot P\rightarrow\lnot P\lor P\\ \text{公理}&:(\lnot P\rightarrow\lnot P\lor P)\rightarrow[(\lnot P\rightarrow(\lnot P\lor P\rightarrow\lnot P))\rightarrow(\lnot P\rightarrow\lnot P)]\\ \text{推論}&:(\lnot P\rightarrow(\lnot P\lor P\rightarrow\lnot P))\rightarrow(\lnot P\rightarrow\lnot P)\\ \text{公理}&:\lnot P\rightarrow(\lnot P\lor P\rightarrow\lnot P)\\ \text{推論}&:\lnot P\rightarrow\lnot P\\ \text{公理}&:(\lnot P\rightarrow P)\rightarrow[(\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P]\\ \text{推論}&:(\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P\\ \text{推論}&:\lnot\lnot P \end{align*}

$\lnot\lnot P$ は 証明図で前にある $$\lnot P\rightarrow\lnot P$$ と $$(\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P$$ から推論された。前にあるから、

$$P\vdash\lnot P\rightarrow\lnot P,\;P\vdash(\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P$$

である。

$$P\rightarrow\color{red}{(\lnot P\rightarrow\lnot P)},\;P\rightarrow(\color{red}{(\lnot P\rightarrow\lnot P)}\rightarrow\color{blue}{\lnot\lnot P})$$

が証明できるなら、三段論法

$$(A\rightarrow\color{red}{B})\rightarrow[(A\rightarrow(\color{red}{B}\rightarrow\color{blue}{C}))\rightarrow(A\rightarrow\color{blue}{C})]$$

が公理にあるから、 $$P\rightarrow\color{blue}{\lnot\lnot P}$$ も証明できる。

$$P\rightarrow\color{red}{(\lnot P\rightarrow\lnot P)}$$ については、 $$\color{green}{\lnot P\rightarrow\lnot P}$$ が証明できるから、公理

$$\color{green}{A}\rightarrow(B\rightarrow\color{green}{A})$$

を使えば、証明できる。

$$P\rightarrow(\color{red}{(\lnot P\rightarrow\lnot P)}\rightarrow\color{blue}{\lnot\lnot P})$$ については、証明図をみると、 $$\lnot P\rightarrow P$$ と公理 $$(\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)$$ から、 $$(\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P$$ が推論されている。 よって、同様に、 $$P\rightarrow(\lnot P\rightarrow P)$$ と $$P\rightarrow[(\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)]$$ が証明できればよい。 前者は公理だから証明できて、後者は $P\rightarrow(\text{公理})$ の形だから、 公理 $$\color{green}{[(\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)]}\rightarrow(P\rightarrow\color{green}{[(\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)]})$$ を使えば、証明できる。

以上の準備をまとめると、 $$P\rightarrow\lnot\lnot P$$ の証明図は次のようになる。

\begin{align*} \text{公理}&:\lnot P\rightarrow\lnot P\lor P\\ \text{公理}&:(\lnot P\rightarrow\lnot P\lor P)\rightarrow[(\lnot P\rightarrow(\lnot P\lor P\rightarrow\lnot P))\rightarrow(\lnot P\rightarrow\lnot P)]\\ \text{推論}&:(\lnot P\rightarrow(\lnot P\lor P\rightarrow\lnot P))\rightarrow(\lnot P\rightarrow\lnot P)\\ \text{公理}&:\lnot P\rightarrow(\lnot P\lor P\rightarrow\lnot P)\\ \text{推論}&:\lnot P\rightarrow\lnot P\\ \text{公理}&:\color{green}{\lnot P\rightarrow\lnot P}\rightarrow(P\rightarrow\color{green}{\lnot P\rightarrow\lnot P})\\ \text{推論}&:P\rightarrow(\lnot P\rightarrow\lnot P)\cdots(1)\\ \text{公理}&:P\rightarrow(\lnot P\rightarrow P)\cdots(2)\\ \text{公理}&:(\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)\cdots(3)\\ \text{公理}&:(P\rightarrow\color{red}{\lnot P\rightarrow P})\rightarrow[(P\rightarrow(\color{red}{(\lnot P\rightarrow P)}\rightarrow\color{blue}{((\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)}) )\rightarrow(P\rightarrow\color{blue}{( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)})]\cdots(4)\\ \text{推論(2)(4)}&:[(P\rightarrow(\color{red}{(\lnot P\rightarrow P)}\rightarrow\color{blue}{( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)}) )\rightarrow(P\rightarrow\color{blue}{( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)})]\cdots(5)\\ \text{公理}&:\color{green}{( (\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P) )}\rightarrow[P\rightarrow\color{green}{( (\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P) )}]\cdots(6)\\ \text{推論(3)(6)}&:P\rightarrow\color{green}{( (\lnot P\rightarrow P)\rightarrow( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P) )}\cdots(7)\\ \text{推論(5)(7)}&:P\rightarrow\color{blue}{( (\lnot P\rightarrow\lnot P)\rightarrow\lnot\lnot P)})\cdots(8)\\ \text{公理}&:(P\rightarrow\color{red}{(\lnot P\rightarrow\lnot P) })\rightarrow[(P\rightarrow(\color{red}{(\lnot P\rightarrow\lnot P)}\rightarrow\color{blue}{\lnot\lnot P}) )\rightarrow(P\rightarrow\color{blue}{\lnot\lnot P})]\cdots(9)\\ \text{推論(1)(9)}&:(P\rightarrow(\color{red}{(\lnot P\rightarrow\lnot P)}\rightarrow\color{blue}{\lnot\lnot P}) )\rightarrow(P\rightarrow\color{blue}{\lnot\lnot P})\cdots(10)\\ \text{推論(8)(10)}&:P\rightarrow\lnot\lnot P \end{align*}