めもめも

このブログに記載の内容は個人の見解であり、必ずしも所属組織の立場、戦略、意見を代表するものではありません。

形式化された証明に関する形式化されない証明

こちらの書籍に登場する、

 定理7.1 関係 x=y は論理式 x=y で表現される

の「証明」について考えます。

まず、表現可能性の定義より、次の2つの「事実」が「検証」できればよいことになります。

 1. m=n\ \Rightarrow\ \vdash \mathbf m = \mathbf n

 2. m\ne n\ \Rightarrow\ \vdash \mathbf m \ne \mathbf n

ここで、「事実」「検証」とカッコ付きにしたのは、上記の事実 1., 2. は、論理式ではなく、形式体系における形式証明が適用できるものではない、ということを強調しています。ここでは、形式体系における「証明」とは異なる作業が求められており、その意味で、「証明」ではなく「検証」と言う言葉を使っています。

また、左辺の m,\,n はあくまでも直感的な意味での自然数を表す記号なので、ここでは、

m=3,\,n=3 の時は、\mathbf 3=\mathbf 3 は証明可能な論理式であろうか?」

m=3,\,n=5 の時は、\mathbf 3\ne \mathbf 5 は証明可能な論理式であろうか?」

と言ったように、具体的な自然数を個別に当てはめた時に、(すべての場合において)右辺の論理式が証明可能であるかを検証することが求められています。この検証作業は、形式体系に頼らずにあくまでも、「自然数に対する素朴な直感」の範囲で検証する必要があります。

まず、1. について考えると、公式4.1「x=x」より、「任意の1階の対象式 \mathbf m について \vdash \mathbf m = \mathbf m である」という事実が成り立っており、まぁまぁ、直感的にも正しいことがわかります。

一方、2. についてはどうでしょうか?

書籍の中では、次の3つの事実から「明らか」と簡単な説明で終わっています。

 \vdash{\mathbf m'}\ne\mathbf 0 (公理 I.1)---- (1)

 \vdash{\mathbf m'}={\mathbf n'} \rightarrow \mathbf m=\mathbf n (公理 I.2)

 \vdash\mathbf m=\mathbf n\rightarrow\mathbf n=\mathbf m (公式 4.3)

これ、ちょっと言葉足らずですよね・・・。もう少し詳しく説明すると、公理 II.3「(\neg B\rightarrow\neg A)\rightarrow(A\rightarrow B)」を用いると、(公理 I.2)、(公式 4.3)から、それぞれ、次の事実が成り立ちます。

 \vdash\mathbf m\ne\mathbf n \rightarrow {\mathbf m'}\ne{\mathbf n'} ---- (2)

 \vdash\mathbf n\ne\mathbf m\rightarrow\mathbf m\ne\mathbf n ---- (3)

ここで、一例として、\mathbf 3\ne \mathbf 5 という論理式について考えます。(1) で \mathbf m=\mathbf 1 の場合から、

 \vdash{\mathbf 2} \ne \mathbf 0

であり、(2) で \mathbf m = {\mathbf 2}\mathbf n =\mathbf 0 の場合と組み合わせて、

 \vdash{\mathbf 3} \ne \mathbf 1

が言えます。同様の作業を繰り返すと、

 \vdash{\mathbf 5} \ne \mathbf 3

が得られて、最後に、(3) で \mathbf n=\mathbf 5\mathbf m=\mathbf 3 の場合とあわせて、

 \vdash{\mathbf 3} \ne \mathbf 5

が確かに成り立ちます。これは、あくまで、\mathbf 3\ne \mathbf 5 という一例にすぎませんが、任意の自然数の組について同様の議論が成り立つことは、「直感的」にも明らかです。これで、冒頭の定理7.1が「証明」されたことになります。

・・・なんだか周りくどいですよね。

もう少し、一般的な意味での「数学」っぽい「証明」の体裁で書くなら、次のようになるかもしれません。

任意の自然数の組 a > b が与えられた時、(1) で \mathbf m = a-b の場合を考えて、(2) を繰り返し適用すると \vdash \mathbf a\ne\mathbf b が成り立つ。a < b の場合は、同様の議論で \vdash \mathbf b\ne\mathbf a が成り立つので、(3) を用いて \vdash \mathbf a\ne\mathbf b が言える。

まぁまぁ、先ほどの \mathbf 3\ne \mathbf 5 という具体例が頭の中にあれば、これを一般化して議論しているだな、というのはすんなり納得できるのですが、具体例を抜きにしていきなり上記の「抽象的(?)」な証明を見たとしたらどうでしょうか? 「この議論に何か想定外の抜けはないだろうか?」「本当にこの議論はすべての自然数について正当化されるのだろうか?」という素朴な疑問はどうしても残ります。

で、「これを正当化するためには、直感を排した形式体系を構築して、証明を形式化して・・・」と考え始めるのですが、ここでは形式体系に関する議論をしているので、これをやりはじめると「形式体系の形式体系の形式体系の・・・」という無限の循環に陥ってしまいます。

「形式体系が素朴な自然数に対する直感を正しく反映しているか」という形式体系そのものに関する議論は、あくまでも、一般的な意味での「数学的直感」に頼った議論で正当化するしかないのです。

むかーし、はじめて冒頭の書籍を読んだ際に、このあたりが腹落ちせずに、読み進めるのに苦労したことをふと思い出して、メモってみました。

追記

上述の内容は、「表現可能性」に関わる議論において、論理式によって表現されるべき「内容」が直感的な命題であることに起因するものであり、形式体系そのものに関するすべての議論が形式体系内部ではできない、と言っているわけではありません。特に形式体系の無矛盾性に関する議論では、「無矛盾である」という直感的な内容の命題を(表現可能性の議論に基づいて)論理式の形で表すことができれば、その論理式自体が証明できるかどうかは、該当の形式体系内で議論することができます。

・参考:無矛盾性証明について