非専門的シンギュラリティー研究所

無限に動き続けるシステムを表す方法を AI なども使って考えていきます。

不完全性定理(11)

不完全性定理

プログラミング言語版不完全性定理(6)

「不完全性定理(8) - エレファント・ビジュアライザー調査記録」では第2不完全性定理の式の計算を抽出して、そこから ChatGPT を使って第2不完全性定理の証明を書いてもらおうとしました。第1不完全性定理の式の計算は少し間違っていたので、第2不完全性定理の方も間違っているかもしれません。これを確かめていきます。

その前に第2不完全性定理について ChatGPT で書いてもらいました。

第二不完全性定理を証明支援システムで証明できるように書き直してください

と入力すると以下の結果となりました。

ゲーデルの第二不完全性定理は、形式体系 $T$ が以下の条件を満たすときに成り立ちます：
1. $T$ はペアノ算術（PA）を含むだけの表現力を持つ。
2. $T$ が無矛盾であれば、 $T$ 自身の無矛盾性を証明できない。
証明支援システム（たとえば Coq や Lean）でこの定理を形式化するためには、次のように進めます。

1. 形式体系のモデル化

$T$ を証明支援システム内で形式化します。具体的には、ペアノ算術 (PA) の公理系と推論規則を定義します。

$T$ の定理とは、公理と推論規則を用いて導ける式であることを示します。

2. ゲーデル数の構成

数式や証明を自然数にエンコードするゲーデル数を定義します。

ゲーデル数の操作（例：数式の合成、推論規則の適用など）を形式化します。

3. 自己言及文の構築

「 $T$ が無矛盾である」という文を $Con(T)$ として形式化します。

$\displaystyle Con(T) := \neg \exists n. Prf(n, \ulcorner \bot \urcorner)$
ここで、 $Prf(n, x)$ は「 $n$ 番目のゲーデル数が $x$ の証明である」という意味です。

4. 無矛盾性の証明不能性の証明

$T$ が無矛盾であると仮定しても、 $T$ 内では $Con(T)$ を証明できないことを示します。

これには、ゲーデルの第一不完全性定理の応用が必要です。すなわち、自己言及する「証明できない文」を構築し、それが無矛盾性を示唆することを利用します。

5. 証明支援システムへの実装

Coq や Lean で次の要素を形式化します：

ペアノ算術の公理

ゲーデル数のエンコード

証明の形式化とその操作

$Con(T)$ の定義と、それが $T$ 内で証明不能であることの証明

6. 注意点

証明支援システム自体の無矛盾性を仮定する必要があります（メタレベルでの無矛盾性）。

形式体系 $T$ は、Coq や Lean の算術部分に限定して形式化します。

具体的な Coq や Lean のコードはやや長くなるため、段階的に進めるのがおすすめです。まずはペアノ算術の形式化から始め、その上でゲーデル数と自己言及文の構築を行うとよいでしょう。

ゲーデル数への変換はライブラリ等でできると仮定して、それ以外の部分を書いてください

と入力すると以下の結果となりました。

それでは、ゲーデル数への変換をライブラリで行えると仮定し、Coq での形式化を進めます。今回は以下のステップで実装します：
1. ペアノ算術 (PA) の公理の定義
2. 証明可能性の形式化
3. 無矛盾性の定義
4. 第二不完全性定理の主張

前提

ゲーデル数への変換および操作は `GodelLib` という仮想ライブラリに任せる。

公理と推論規則を構造体として定義する。
1. ペアノ算術 (PA) の公理の定義

Coq では、PA の公理は命題の集合として表現できます。
Require Import Coq.Lists.List.
Import ListNotations.

(* 項と式の定義 *)
Inductive term : Type :=
  | Var : nat -> term
  | Zero : term
  | Succ : term -> term
  | Plus : term -> term -> term
  | Mult : term -> term -> term.

Inductive formula : Type :=
  | Eq : term -> term -> formula
  | Not : formula -> formula
  | And : formula -> formula -> formula
  | Or : formula -> formula -> formula
  | Implies : formula -> formula -> formula
  | Forall : nat -> formula -> formula
  | Exists : nat -> formula -> formula.

(* ペアノ算術の公理を型として定義 *)
Inductive PA_axioms : formula -> Prop :=
  | PA_ZeroNotSucc : PA_axioms (Not (Eq (Succ Zero) Zero))
  | PA_SuccInjective : forall x y,
      PA_axioms (Implies (Eq (Succ x) (Succ y)) (Eq x y))
  | PA_ZeroPlus : forall x,
      PA_axioms (Eq (Plus Zero x) x)
  | PA_SuccPlus : forall x y,
      PA_axioms (Eq (Plus (Succ x) y) (Succ (Plus x y)))
  | PA_ZeroMult : forall x,
      PA_axioms (Eq (Mult Zero x) Zero)
  | PA_SuccMult : forall x y,
      PA_axioms (Eq (Mult (Succ x) y) (Plus (Mult x y) y))
  | PA_Induction : forall P,
      (* ∀P. P(0) ∧ ∀n. P(n) → P(n+1) → ∀m. P(m) *)
      PA_axioms (Implies 
                   (And (P Zero)
                        (Forall 0 (Implies (P (Var 0)) (P (Succ (Var 0))))))
                   (Forall 0 (P (Var 0)))).
2. 証明可能性の形式化

証明可能性を形式化します。
ゲーデル数へのエンコードはライブラリに任せるため、`Prf` 関数を定義します。
Parameter GodelLib : Type.
Parameter Encode : formula -> GodelLib.
Parameter Prf : GodelLib -> GodelLib -> Prop.

(* 証明可能性: T が φ を証明できる *)
Definition Provable (T : list formula) (φ : formula) : Prop :=
  exists n, Prf (Encode (AndAll T)) (Encode φ).

(* 省略形: PA が φ を証明できる *)
Definition PA_Provable (φ : formula) : Prop :=
  Provable (map Encode (filter PA_axioms (all_formulas))) φ.
3. 無矛盾性の定義

「無矛盾性」を形式化します。
$Con(T) := \neg \exists n. Prf(n, \ulcorner \bot \urcorner)$
(* ⊥ を表す式 *)
Definition FalseFormula := (Eq Zero (Succ Zero)).

(* 無矛盾性の定義 *)
Definition Con (T : list formula) : Prop :=
  ~ Provable T FalseFormula.

(* PA の無矛盾性 *)
Definition Con_PA : Prop := Con (map Encode (filter PA_axioms (all_formulas))).
4. 第二不完全性定理の主張

形式体系 $T$ が無矛盾ならば、 $T$ 内で $Con(T)$ を証明できないことを主張します。
Theorem Godel_Second_Incompleteness :
  Con_PA -> ~ PA_Provable (Encode (Not (Exists 0 (Prf (Var 0) (Encode FalseFormula))))).
Proof.
  (* 証明の詳細はゲーデルの自己言及構成と第一不完全性定理を使用 *)
Admitted.
説明

`PA_axioms` でペアノ算術の公理を形式化しました。

`Provable` で証明可能性を定義し、`Con` で無矛盾性を定義しました。

`Godel_Second_Incompleteness` で第二不完全性定理を Coq 上で主張しています。

証明には、ゲーデルの第一不完全性定理を用いた自己言及構成が必要なため、`Admitted` としています。

次のステップ

ゲーデルの自己言及構成を形式化し、証明を完成させること。

Coq のタクティクスを駆使して、矛盾が導かれないことを示す。

この設計により、ゲーデル数へのエンコード部分を除いた不完全性定理の形式化が可能です。

証明の手順を説明してください

と入力すると以下の結果となりました。

ゲーデルの第二不完全性定理の証明は、以下の手順で進めます。
今回は、ゲーデル数への変換をライブラリに任せ、自己言及文の構成に重点を置きます。

概要

ゲーデルの第二不完全性定理は次のように述べられます：

定理： 形式体系 $T$ が無矛盾であり、ペアノ算術（PA）を含むだけの表現力を持つならば、 $T$ 内では $T$ 自身の無矛盾性を証明できない。

$\displaystyle Con(T) := \neg \exists n. Prf(n, \ulcorner \bot \urcorner)$
ここで、 $Prf(n, x)$ は「 $n$ 番目のゲーデル数が $x$ の証明である」ことを意味します。

証明の流れ

1. 証明可能性の形式化
2. 無矛盾性の定義
3. 自己言及文の構築（ゲーデル文）
4. 矛盾の導出
5. 結論の導出
1. 証明可能性の形式化

まず、 $T$ における証明可能性を次のように形式化します：

$Provable_T(φ)$ : $T$ が $φ$ を証明可能である。

$\displaystyle Provable_T(φ) := \exists n. Prf(n, \ulcorner φ \urcorner)$
証明支援システムでは、この定義は次のように書きます：
Definition Provable (T : list formula) (φ : formula) : Prop :=
  exists n, Prf (Encode (AndAll T)) (Encode φ).
2. 無矛盾性の定義

無矛盾性を次のように定義します：

$Con(T)$ : $T$ が無矛盾である。

$\displaystyle Con(T) := \neg Provable_T(\bot)$
ここで、 $\bot$ は矛盾（例えば $0 = 1$ ）を表します。
Coq では次のように定義します：
Definition FalseFormula := (Eq Zero (Succ Zero)).
Definition Con (T : list formula) : Prop :=
  ~ Provable T FalseFormula.
3. 自己言及文の構築（ゲーデル文）

ここが証明の核心です。ゲーデル文 $G$ を次のように構成します：

$G$ : 「 $G$ 自身は $T$ 内で証明できない」という文。

$\displaystyle G := \neg Provable_T(\ulcorner G \urcorner)$

1. ゲーデル数の利用： $G$ のゲーデル数を $g$ とする。
2. 自己言及の構築： $G$ を次のように表現します：
$\displaystyle G := \neg \exists n. Prf(n, g)$
3. 数式への変換： $G$ を算術の範囲で表現可能な文にします。
Coq の場合、次のように定義できます：
Definition G := Not (Exists 0 (Prf (Var 0) (Encode G))).
4. 矛盾の導出

次に、 $T$ が無矛盾であるという仮定の下で、 $T$ 内で $G$ の証明ができないことを示します。

仮定

$Con(T)$ を仮定します。つまり、 $T$ では $\bot$ が証明できない。

$\displaystyle Con(T) := \neg Provable_T(\bot)$

矛盾の導出

1. $G$ の場合分け：

$T \vdash G$ と仮定 → $T \vdash \neg Provable_T(\ulcorner G \urcorner)$ となるが、これは $G$ の定義に矛盾。

$T \vdash \neg G$ と仮定 → $T \vdash Provable_T(\ulcorner G \urcorner)$ となるが、これは $G$ の定義に矛盾。

2. 結論：
よって、 $T$ 内で $G$ を証明することも、その否定を証明することもできない。
5. 結論の導出

以上の手順から、 $T$ 内で $G$ を証明できないため、 $T$ は自身の無矛盾性を証明できないことが示されます。
つまり、
$\displaystyle Con(T) \rightarrow \neg Provable_T(\ulcorner Con(T) \urcorner)$
Coq では次のように主張します：
Theorem Godel_Second_Incompleteness :
  Con_PA -> ~ PA_Provable (Encode (Not (Exists 0 (Prf (Var 0) (Encode FalseFormula))))).
Proof.
  (* 詳細はゲーデル文の自己言及構成に依存するため省略 *)
Admitted.
補足

ゲーデルの第一不完全性定理の利用：自己言及文を構築する際に、第一不完全性定理を応用しています。

自己言及の巧妙さ： $G$ が自身について語るように設計されているため、形式体系内部では矛盾なく証明が不可能です。

形式体系の仮定： $T$ がペアノ算術を含む表現力を持ち、無矛盾であるという仮定が必要です。

次のステップ

ゲーデル文の構築をさらに厳密に形式化する。

Coq での証明を完了させるために、第一不完全性定理の形式化を行う。

`Admitted` を埋めるために、自己言及文の不証明性を直接示す。

この手順を基に、証明支援システム上でゲーデルの第二不完全性定理を厳密に形式化・証明できます。

ゲーデル数をプログラミング言語のコードに変えるとどうなりますか？

と入力すると以下の結果となりました。これは知りたいことではなかったのですが、役に立ちそうなので引用しておきます。

ゲーデル数は、数式やプログラムを自然数にエンコードする手法です。プログラミング言語でこれを実装する場合、以下のようなステップを踏みます：
1. シンボルのエンコード：変数、関数、演算子などを自然数に対応させます。
2. 構造のエンコード：項や式の構造を保持しつつ、自然数に変換します。
3. プライムのべき乗の利用：ゲーデル数の生成には、異なる素数のべき乗を掛け合わせる方法を使います。

1. シンボルのエンコード

シンボルに番号を割り当てます。たとえば：

$x_i$ → $i$

$0$ → $1$

$Succ$ → $2$

$Plus$ → $3$

$Mult$ → $4$

$Eq$ → $5$

$Not$ → $6$

$And$ → $7$

$Or$ → $8$

$Implies$ → $9$

$Forall$ → $10$

$Exists$ → $11$

2. 構造のエンコード

構造を保持するために、項や式をリストとしてエンコードします。
例えば、 $Plus(x, 0)$ は以下のようにリストで表せます：
$\displaystyle Plus(x, 0) \Rightarrow [3, x, 1]$

3. プライムのべき乗の利用

ゲーデル数は、各要素に素数のべき乗を割り当てて計算します。
具体的には：
$\displaystyle g = p_1^{a_1} \cdot p_2^{a_2} \cdot \ldots \cdot p_n^{a_n}$
ここで、 $p_i$ は $i$ 番目の素数、 $a_i$ はリストの $i$ 番目の要素です。
Python による実装例

Python を使って、式をゲーデル数に変換するコードを書いてみます。
from sympy import prime

* シンボルに対応する番号
SYMBOL_TABLE = {
    'Var': lambda x: x,
    'Zero': 1,
    'Succ': 2,
    'Plus': 3,
    'Mult': 4,
    'Eq': 5,
    'Not': 6,
    'And': 7,
    'Or': 8,
    'Implies': 9,
    'Forall': 10,
    'Exists': 11
}

* 項のエンコード
def encode_term(term):
    if isinstance(term, int):  # 変数 (Var)
        return [[SYMBOL_TABLE['Var':term]]]
    if term == 'Zero':
        return [SYMBOL_TABLE['Zero']]
    if isinstance(term, tuple) and len(term) == 2:
        func, arg = term
        if func == 'Succ':
            return [SYMBOL_TABLE['Succ']] + encode_term(arg)
    if isinstance(term, tuple) and len(term) == 3:
        func, arg1, arg2 = term
        return [SYMBOL_TABLE[func]] + encode_term(arg1) + encode_term(arg2)
    raise ValueError("Unknown term structure")

* 式のエンコード
def encode_formula(formula):
    if isinstance(formula, tuple):
        if formula[0] in ['Eq', 'Not', 'And', 'Or', 'Implies']:
            func, left, right = formula
            return [SYMBOL_TABLE[func]] + encode_term(left) + encode_term(right)
        if formula[0] in ['Forall', 'Exists']:
            func, var, body = formula
            return [SYMBOL_TABLE[func], var] + encode_formula(body)
    raise ValueError("Unknown formula structure")

* ゲーデル数の計算
def godel_number(sequence):
    result = 1
    for i, num in enumerate(sequence):
        result *= prime(i+1) ** num
    return result

* 使用例: Plus(x, Zero) を表現
term = ('Plus', 0, 'Zero')
encoded_term = encode_term(term)
godel_num = godel_number(encoded_term)

print(f"Term: {term}")
print(f"Encoded: {encoded_term}")
print(f"Godel Number: {godel_num}")
例： $Plus(x, 0)$ のエンコード

`term = ('Plus', 0, 'Zero')` の場合：
1. `encode_term` で `[3, 0, 1]` にエンコードされる。
2. `godel_number` で次の計算を行う：
$\displaystyle g = 2^3 \cdot 3^0 \cdot 5^1 = 8 \cdot 1 \cdot 5 = 40$
3. ゲーデル数は `40` となる。

解説

エンコードの工夫：シンボルを整数に変換し、リストで構造を表しています。

素数のべき乗の利用：異なる素数のべき乗を使うことで、情報の順序と内容を一意にエンコードできます。

拡張の可能性：変数の扱い、より複雑な式、論理結合子を含む場合にも対応可能。

応用と次のステップ

Coq や Lean への応用：形式体系内でのエンコード関数を定義できます。

自己言及文の構築：ゲーデル数を利用して、自己言及する文（ゲーデル文）を構築できます。

証明可能性の形式化：エンコードした数値を使って、証明可能性 $Prf(n, x)$ を定義できます。

この実装を元に、ゲーデルの第一・第二不完全性定理の形式化に応用できます。

不完全性定理とはなにか完全版ゲーデルとチューリング天才はなにを証明したのか (ブルーバックス B 2277)

不完全性定理とはなにか完全版ゲーデルとチューリング天才はなにを証明したのか (ブルーバックス B 2277)

作者:竹内薫
講談社

チューリングの計算理論入門　チューリング・マシンからコンピュータへ (ブルーバックス)

チューリングの計算理論入門　チューリング・マシンからコンピュータへ (ブルーバックス)

作者:高岡詠子
講談社

不完全性定理: 数学的体系のあゆみ (ちくま学芸文庫ノ 4-1 Math&Science)

不完全性定理: 数学的体系のあゆみ (ちくま学芸文庫ノ 4-1 Math&Science)

作者:野崎昭弘
筑摩書房

今度こそわかるゲーデル不完全性定理 (今度こそわかるシリーズ)

今度こそわかるゲーデル不完全性定理 (今度こそわかるシリーズ)

作者:本橋信義
講談社

数学基礎論 (ちくま学芸文庫)

数学基礎論 (ちくま学芸文庫)

作者:前原昭二,竹内外史
筑摩書房

数学基礎論　増補版

数学基礎論　増補版

作者:新井敏康
東京大学出版会

論理学

作者:野矢茂樹
東京大学出版会

証明と論理に強くなる～論理式の読み方から，ゲーデルの門前まで～

証明と論理に強くなる～論理式の読み方から，ゲーデルの門前まで～

作者:小島寛之
技術評論社

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化

作者:萩原学,アフェルト・レナルド
森北出版

数理論理学

数理論理学

作者:戸次大介
東京大学出版会

数理論理学: 合理的エ-ジェントへの応用に向けて

数理論理学: 合理的エ-ジェントへの応用に向けて

作者:加藤暢
コロナ社

計算理論の基礎 [原著第3版] 1.オートマトンと言語

計算理論の基礎 [原著第3版] 1.オートマトンと言語

作者:Michael Sipser
共立出版

計算理論の基礎 [原著第3版] 2.計算可能性の理論

計算理論の基礎 [原著第3版] 2.計算可能性の理論

作者:Michael Sipser
共立出版

計算理論の基礎 [原著第3版] 3.複雑さの理論

計算理論の基礎 [原著第3版] 3.複雑さの理論

作者:Michael Sipser
共立出版