ウカシェヴィチの公理系における二重否定除去律の具体的な証明

　『ゲーデルと20世紀の論理学2』を読んでいる者です。今回は、ヤン・ウカシェヴィチによる命題論理の3つの公理図式からなる公理系において、二重否定除去律「 $\neg\neg A\rightarrow A$ 」が定理であることを完全性定理を使わずに示します。

背景

　「 $\neg\neg A\rightarrow A$ 」の具体的な証明が想像できなかったので、取り組んでみたらとても感動したので書きます。もちろん、証明の存在自体は、命題論理の一般化された完全性定理によって示されています。

定義

　定義2.20、定義2.21は『ゲーデルと20世紀の論理学2』から引用した。

　ウカシェヴィチによる公理系は以下の3つからなる。
\begin{align}
P1.&\quad A \rightarrow (B \rightarrow A)。\\
P2.&\quad (A \rightarrow (B \rightarrow C) ) \rightarrow ( (A \rightarrow B) \rightarrow (A \rightarrow C) )。\\
P3.&\quad (\neg B \rightarrow \neg A ) \rightarrow (A \rightarrow B )。
\end{align} $A,B,C$ は任意の命題であるから、この3つは公理図式（公理の集合）である。

定義2.20　命題論理の定理はつぎのように定義される。

　（1）公理 $P1,P2,P3$ は定理である。
　（2） $A$ と $A\rightarrow B$ が定理なら、 $B$ も定理である（三段論法）。

定義2.21　命題の列 $A_0,A_1,\dots,A_n$ が以下の条件を満たしているとき、その列を $A_n$ の証明という。各 $k\leq n$ について、

　（1） $A_k$ は公理（ $P1,P2,P3$ ）であるか、
　（2） $i,j\lt k$ が存在して $A_j$ は $A_i\rightarrow A_k$ である。

......（省略）......

補足

　「 $A$ が定理である」ことと「 $A$ の証明が存在する」ことは同値である。 $A$ が定理であることを $\vdash A$ と書く。理論（追加の公理） $\Sigma$ の上で $A$ が定理であることを $\Sigma\vdash A$ と書く。その他は、本書を参照してほしい。

例

　例として、「 $A\rightarrow A$ 」の証明を具体的に示す。
　2020/8/22追記： $X$ の部分は何でもよい。
\begin{align}
A_0:&\quad A\rightarrow ( (X\rightarrow A)\rightarrow A)。&(P1)\\
A_1:&\quad (A\rightarrow ( (X\rightarrow A)\rightarrow A) ) \rightarrow ( (A \rightarrow (X \rightarrow A) )\rightarrow (A \rightarrow A) )。&(P2)\\
A_2:&\quad (A\rightarrow(X\rightarrow A) ) \rightarrow (A \rightarrow A)。&(A_0,A_1)\\
A_3:&\quad A \rightarrow ( X \rightarrow A )。&(P1)\\
A_4:&\quad A \rightarrow A。&(A_3,A_2)
\end{align}

本題

　「 $\neg\neg A\rightarrow A$ 」が定理であることを具体的に示す。

導出

　例の「 $A\rightarrow A$ 」が定理であることは $P1,P2,P3$ に適当に当てはめれば示せたが、「 $\neg\neg A \rightarrow A$ 」はそうもいかない。
　そこで、演繹定理「 $\Sigma\cup\{ A\}\vdash B \Rightarrow \Sigma\vdash A\rightarrow B$ 」とその証明を利用する。
　演繹定理の証明をやってみると気付くのが、 $\vdash A\rightarrow B$ 、 $\vdash A\rightarrow (B\rightarrow C)$ から $\vdash A\rightarrow C$ が導けることである（ $P2$ を使う）。また、上の例で $A\rightarrow A$ の証明を見ている。この2つより、理論 $\{A\}$ における $B$ の具体的な証明から理論なしの $A\rightarrow B$ の具体的な証明が機械的に構成できることが示せる。

証明

\begin{align}
\{\neg\neg A\}&\vdash \neg\neg A、&\\
\{\neg\neg A\}&\vdash \neg\neg\neg\neg A \rightarrow \neg\neg A、&（P1と三段論法）\\
\{\neg\neg A\}&\vdash \neg A \rightarrow \neg\neg\neg A、&（P3と三段論法）\\
\{\neg\neg A\}&\vdash \neg\neg A \rightarrow A、&（P3と三段論法）\\
\{\neg\neg A\}&\vdash A&（三段論法）
\end{align}であるから、
\begin{align}
&\vdash \neg\neg A \rightarrow \neg\neg A、\\
&\vdash \neg\neg A \rightarrow (\neg\neg\neg\neg A \rightarrow \neg\neg A)、\\
&\vdash \neg\neg A \rightarrow (\neg A\rightarrow \neg\neg\neg A)、\\
&\vdash \neg\neg A \rightarrow (\neg\neg A \rightarrow A)、\\
&\vdash \neg\neg A \rightarrow A
\end{align}が証明の通過地点となる。これから具体的な証明を得ることは容易である。その証明列は長くなるが、書いてみることにする。これは要するに、機械語でFizzBuzzをするようなものである。 $P3$ をくるくる回すように使う。 $A_{15}$ から $A_{19}$ は、 $A\rightarrow A$ の証明に二重否定がついただけである。上に示した証明の通過点に該当する命題の番号には、 $*$ を付けた。
　
\begin{align}
A_0:&\quad (\neg\neg\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg A \rightarrow \neg\neg\neg A)、&(P3)\\
A_1:&\quad ( (\neg\neg\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg A \rightarrow \neg\neg\neg A))\\
&\rightarrow (\neg\neg A \rightarrow ( (\neg\neg\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg A \rightarrow \neg\neg\neg A)))、&(P1)\\
A_2:&\quad \neg\neg A \rightarrow ( (\neg\neg\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg A \rightarrow \neg\neg\neg A))、&(A_0,A_1)\\
A_3:&\quad (\neg\neg A \rightarrow ( (\neg\neg\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg A \rightarrow \neg\neg\neg A)))\\
& \rightarrow ( (\neg\neg A \rightarrow (\neg\neg\neg\neg A \rightarrow \neg\neg A))\rightarrow (\neg\neg A \rightarrow (\neg A \rightarrow \neg\neg\neg A)))、&(P2)\\
A_4:&\quad (\neg\neg A \rightarrow (\neg\neg\neg\neg A \rightarrow \neg\neg A))\rightarrow (\neg\neg A \rightarrow (\neg A \rightarrow \neg\neg\neg A))、&(A_2,A_3)\\
A_5*:&\quad \neg\neg A \rightarrow (\neg\neg\neg\neg A \rightarrow \neg\neg A)、&(P1)\\
A_6*:&\quad \neg\neg A \rightarrow (\neg A \rightarrow \neg\neg\neg A)、&(A_5,A_4)\\
A_7:&\quad (\neg A \rightarrow \neg\neg\neg A)\rightarrow(\neg\neg A \rightarrow A)、&(P3)\\
A_8:&\quad ( (\neg A \rightarrow \neg\neg\neg A)\rightarrow(\neg\neg A \rightarrow A))\rightarrow \\
&(\neg\neg A \rightarrow ( (\neg A \rightarrow \neg\neg\neg A)\rightarrow(\neg\neg A \rightarrow A)))、&(P1)\\
A_9:&\quad \neg\neg A \rightarrow ( (\neg A \rightarrow \neg\neg\neg A)\rightarrow(\neg\neg A \rightarrow A))、&(A_7,A_8)\\
A_{10}:&\quad (\neg\neg A \rightarrow ( (\neg A \rightarrow \neg\neg\neg A)\rightarrow(\neg\neg A \rightarrow A))) \\
&\rightarrow ( (\neg\neg A \rightarrow (\neg A \rightarrow \neg\neg\neg A)) \rightarrow (\neg\neg A \rightarrow (\neg\neg A \rightarrow A)) )、&(P2)\\
A_{11}:&\quad(\neg\neg A \rightarrow (\neg A \rightarrow \neg\neg\neg A)) \rightarrow (\neg\neg A \rightarrow (\neg\neg A \rightarrow A))、&(A_9,A_{10})\\
A_{12}*:&\quad \neg\neg A \rightarrow (\neg\neg A \rightarrow A)、&(A_6,A_{11})\\
A_{13}:&\quad (\neg\neg A \rightarrow (\neg\neg A \rightarrow A)) \\
&\rightarrow ( (\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg\neg A \rightarrow A) )、&(P2)\\
A_{14}:&\quad (\neg\neg A \rightarrow \neg\neg A) \rightarrow (\neg\neg A \rightarrow A)、&(A_{12},A_{13})\\
A_{15}:&\quad \neg\neg A\rightarrow ( (X\rightarrow \neg\neg A)\rightarrow \neg\neg A)、&(P1)\\
A_{16}:&\quad (\neg\neg A\rightarrow ( (X\rightarrow \neg\neg A)\rightarrow \neg\neg A) ) \rightarrow ( (\neg\neg A \rightarrow (X \rightarrow \neg\neg A) )\rightarrow (\neg\neg A \rightarrow \neg\neg A) )、&(P2)\\
A_{17}:&\quad (\neg\neg A\rightarrow(X\rightarrow \neg\neg A) ) \rightarrow (\neg\neg A \rightarrow \neg\neg A)、&(A_{15},A_{16})\\
A_{18}:&\quad \neg\neg A \rightarrow ( X \rightarrow \neg\neg A )、&(P1)\\
A_{19}*:&\quad \neg\neg A \rightarrow \neg\neg A、&(A_{18},A_{17})\\
A_{20}*:&\quad \neg\neg A \rightarrow A。&(A_{19},A_{14})\\
\end{align}

終わり

リンク

ゲーデルと20世紀の論理学2 - 東京大学出版会