それ自身もその否定も証明できない、というゲーデル論理式は正しい。

 同一構造

           原始帰納的関数


 自然数(系S1)⇔論理式(系S2)の対応を示す関数

 ゲーデル数:n1⇔一変数(k)論理式:G(n1,k)
 ゲーデル数:n2⇔一変数(k)論理式:G(n2,k)

           …
 ゲーデル数:no⇔一変数(ni)論理式:¬Prov(ni,ni)

 ゲーデル論理式:¬Prov(no,no)は、
 それ自身もその否定も証明できない。
  (ゲーデルの第一不完全性定理)
A「G(ni,ni)が証明できる。」
 ≡Prov(ni,ni) 
@「¬G(ni,ni)が証明できる。」
 ≡¬Prov(ni,ni) …*

  〜自然数論を含む形式的体系S1(無矛盾)〜

 <自然数>
 n1,n2,

 
 <一変数(k)論理式>
 G(n1,k),G(n2,k),… →k=ni(i=1,2,…)を代入→ G(n1,n1),G(n2,n2),…


                                  




                                        しかし、系S2からの考察(下記)により


  〜自然数論を含む形式的体系S2(無矛盾)〜
























 ※
 系S1を系S2から考察すると、

 「¬Prov(ni,ni)…*が証明できる。」≡一変数(ni)論理式:Prov(no,ni)
 ∴¬Prov(ni,ni)⇔Prov(no,ni)
 ni=noのとき、
 ¬Prov(no,no)⇔Prov(no,no)
 完全性を仮定すると矛盾! ∴ゲーデル第一不完全性定理が成立。



「ゲーデルの不完全性定理」を学ぶ(その2)

「数学の中の無限」への扉へもどる

 今回、ゲーデルの不完全性定理を構造的に捉えることにより、その1では拭い切れなかった
“狐につままれたような感”をかなり払拭できたような気がします。
 以下に、その内容を示しましたので、どうぞご覧下さい。

1.ゲーデルの第一不完全性定理・模式図(完全性を仮定)
                                    注)その1で用いた記号に一部変更を加えています。








































[ポイント]
(1)系S1と系S2は同一構造
@形式的体系においては、論理式や証明は公理および推論規則に基づく記号の有限列として表せる。
Aよって、記号に自然数(ゲーデル数)を対応させれば、論理式や証明は自然数の有限列として表せる。
Bゆえに、系S2における超数学的な命題は自然数列についての命題となる。
 即ち、系S2は系S1と同一構造となる。
(2)証明可能を意味する論理式の存在
 「論理式○○が証明できる。」という命題は記号の配列に関する命題であり、
 実際に論理式(Prov)として表すことができる。
(3)その他
@G(ni,k)などは系S1内の一変数(k)論理式の上に、その外部の系S2から貼った、ゲーデル数niを識別番号とする
 ラベルと見る。
A第一不完全性定理は
 「リシャ-ルのパラドックス」や「うそつきのパラドックス」といった自己言及によるパラドックスと
 論理的共通性・類似性を持つが、
 同定理が「無矛盾な系S1に対して完全性を仮定すると、この系S1を、その外部にあってこれと同一構造の系S2
 から見たときに矛盾が生じる。」という重構造の上の背理法であることに留意すれば、
 論理破綻のパラドックスとの差異がわかる。

2.ゲーデルの第二不完全性定理
 系S1内でこの系が無矛盾であることが証明できたと仮定。
⇒第一不完全性定理により「¬Prov(no,no)が証明できないこと」が証明できた。
⇒「¬Prov(no,no)が証明できない。」⇔「ゲーデル数noの論理式の変数にnoを代入した式は証明できない。」
                        ⇔¬Prov(no,no)
⇒¬Prov(no,no)が証明できたことになる。
⇒第一不完全性定理に反し、矛盾!
⇒系S1内ではその無矛盾を証明することが出来ない。(ゲーデルの第二不完全性定理

3.考察
@「自分自身を証明することができない。」というゲーデル論理式が証明できないことがそんなに衝撃的なこと
 なのか、そんな命題が証明できないから系が不完全だというのはおおげさではないか。
 「うそつきのパラドックス」でうそつきか正直者かが判定できないことに大騒ぎするのと何が違うのか。
 初めてゲーデルの第一不完全性定理の説明を読んだとき、そう感じました。
Aしかし、ゲーデル論理式=「自分自身を証明することができない。」というのは系S2から見たときの解釈で
 あって、系S1内部からはそのようには見えない、ということではないかと思います。
 系S1内部では¬Prov(ni,ni)のniはあくまで前が論理式、後が自然数であって、両者は全く別物なのであり、
 これを1つの変数として捉えることは、系S1の外部の系S2でしか行えないはずです。
Bですから、¬Prov(no,no)は系S1から見れば、有限個の記号を並べた、変数をnoとする論理式P(no)
 すぎないのですが、これを系S2から見れば¬Prov(¬Prov(¬Prov(…) ) )となって、
 それ自身もその否定も証明できないことがわかるということなのだろうと思います。
 ましてや、この第一定理が無矛盾性の証明可能性すらも否定する次の第二定理に繋がるのですから、
 事は重大と言うわけです。
C第一定理を比喩的に表現すれば、次のようになります。
 すなわち、無矛盾である系S1を別の同構造の系S2の“ルーペ”を介して見ると、
 そこには、「それ自身の証明⇔その否定の証明」という矛盾を有する論理式が必ず見出されます。
 これが、系S1においてそれ自身もその否定も証明することのできないゲーデル論理式にほかなりません。
 第一定理をこのように捉えたとき、第二定理は次のようになります。
 もし、系S1からその系自身の無矛盾性を証明できたと仮定すると、
 第一定理より系S1内にはゲーデル論理式が存在することになります。
 そして、このゲーデル論理式を同じ系S1の“ルーペ”を介して見ると、それは矛盾を有する論理式と映ります。
 これは取りも直さず、“ルーペ”を介して見られている系S1内に矛盾が存在することを意味し、
 系S1の無矛盾性が証明できたとする仮定に反します。
 よって、背理法より、系S1からその系自身の無矛盾性を証明することはできないことになります。
 
 この定理の証明を理解するポイントはこのようなところにあると思います。