ペアノ算術だけで十分な理由: PAは計算をエンコードできる

 (math.stackexchange.com)
1 ポイント 投稿者 GN⁺ 2025-06-15 | 1件のコメント | WhatsAppで共有
  • PAは Goodstein 定理全体 ∀n G(n) は証明できないが、各標準自然数 n について G(n) の PA 証明の存在 は PA 内部で示せる
  • 要点は、n に必要な有限高さの ω 冪塔までだけを扱い、その範囲の 超限帰納法の証明 を機械的に生成する構成にある
  • 必要な高さ m は n の hereditary base notation の高さに対応し、O(log*(n)) であり、略記 ω^[m] を使うと証明長は O(m log m) 程度まで縮む
  • この結果が意味するのは「各個別事例の証明は作れる」ということであって、PAが Goodstein 定理全体 を証明するという意味ではない
  • PAは自然数1つの中に数、対、リスト、プログラム状態、形式論理の証明をすべてエンコードできるため、生成された証明が実際に PA の証明かどうかも PA の中で検証できる

問題の数学的な形

  • 関心の対象は、Goodstein 列が最終的に 0 に到達するという命題 G(n) である

  • よく知られた区別は次のとおり

    • PAは、標準自然数の各具体例 G(15)、G(268) のような命題は証明できる
    • PAは、全称命題 ∀n ∈ N: G(n) は証明できない

  • 問いは、PAが次の形の命題を証明できるかどうかである

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) は、p が PA における φ の 証明コード であることを意味する

  • 結論は、このレベルでは PAだけで十分 だということである

PAが証明すべきこと

  • 各 n について、PAが示せばよい内容は次の3点である
    • G(n) を証明するのに必要な 証明長 を計算できる
    • その証明を構成する手続きが停止する
    • 構成された証明の最後の文が G(n) の停止を述べている
  • 各 G(n) に対して、長さ O(log*(n) log(log*(n))) の PA 証明を構成できる
  • log* は 反復対数 (iterated logarithm) であり、きわめてゆっくり増加する関数である
  • n が大きくなるほど必要な証明も長くなるため、これだけで PA が Goodstein 定理全体を証明できるわけではない

Goodstein 列と順序数表記

  • Goodstein 列は hereditary base notation を用い、これは Cantor normal form で書かれた順序数表現と結びついている

  • John von Neumann 流の構成では、順序数は集合として構成される

    • 0 は空集合
    • ある順序数 ord があれば、ord ∪ {ord} も順序数
    • 順序数たちの集合 X があれば、X の合併も順序数

  • Cantor normal form は順序数を次の形で表す

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • 各 ni は正の自然数
    • 各 ordi は順序数
    • ord1 > ord2 > ... > ordk

  • この表記は次の順序数を表す

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • 比較は ord1、n1、ord2、n2 の順の 辞書式比較 で処理し、一方が先に終わる場合は短い方が小さい

帰納法から超限帰納法へ

  • PAの第5公理は自然数に対する 帰納法 を与える
    • S(0) が真である
    • S(n) なら S(s n) も真である
    • すると、すべての自然数について S が真である
  • PAはここから < を再帰的に定義でき、さらに 強い帰納法 も証明できる
    • すべての n について、n より小さいすべての数で S が真なら S(n) も真であることを示せば、すべての自然数で S が真になる
  • ZFCでは、順序数全体に対する強い帰納法である 超限帰納法 を証明できる
  • Cantor normal form で書かれた対象については、次の2性質が使われる
    • Cantor normal form で書かれた下降列は必ず有限である
    • Cantor normal form の対象に対して超限帰納法を適用できる

PAの中で可能な超限帰納法の範囲

  • PAは、すべての順序数に対する超限帰納法を証明することはできない
  • その代わり、有限の高さをもつ特定の順序数範囲なら PA の中で扱える
    • PAは強い帰納法を証明できるので、ω までの超限帰納法を扱える
    • 同じ論法で、ω^ω に対する超限帰納法も証明可能である
    • さらに同じ方法を繰り返して、ω^(ω^ω)、ω^(ω^(ω^ω)) など有限高さの塔について扱える
  • 各段階の証明は塔の高さだけが変わり、機械的に生成 される
  • m 番目の塔をそのまま書くと、全体の証明長は O(m^2) である
  • ω^[m] のような略記を使うと、m の記述に必要なのは O(log m) の長さだけで済むため、全体の証明は O(m log m) になる
  • ε₀ 未満の各順序数それぞれについて、PA 内の超限帰納法の証明は存在するが、これを1つにまとめるには無限長の証明が必要になる
  • もし PA が ε₀ に対する超限帰納法を証明できれば、PA の無矛盾性を証明できてしまい、Gödel の第2不完全性定理と衝突する

各 G(n) に対する証明生成手続き

  • 特定の n について必要なのは、hereditary base notation の塔の高さまでだけである
  • この高さは O(log*(n)) であり、PAが容易に計算できる関数として扱える
  • プログラムは入力 n に対して次を出力できる
    • PAに関する共通事実の証明
    • G(n) が、ある m について ω^[m] 内の 下降列 を追跡しているという証明
    • その m を計算した過程と、m の値に関する証明
    • ω^[0] に対する超限帰納法の証明
    • ω^[i] の超限帰納法が ω^[i+1] の超限帰納法を含意するという証明
    • i = 0 から m-2 までの各段階の超限帰納法の証明
    • ω^[m-1] の超限帰納法が、ω^[m] 内のすべての下降列が有限であることを含意するという証明
    • G(n) が停止するという結論
  • PAは、この手続きについて次を証明できる
    • 手続きが停止する
    • 手続きが文のリストを生成する
    • リストがペアノ公理から始まる
    • 各文がそれ以前の文から論理的に導かれる
    • 帰納法により、すべての文が証明される
    • 最後の文が「G(n) は停止する」である
  • したがって PA は、任意の自然数 n について、PA が G(n) の停止を証明するという事実を証明する

PAが計算をエンコードする方法

  • 「エンコード」とは、ある自然数が特定の構造を意味するように定める方法である
  • PAの基本材料は次のとおり
    • 0
    • 後者関数 (s n)
    • 等号
    • 0 でない数に対する前者 (p n)
    • 帰納法によって正当化される再帰定義
    • 0 または 1 に応じて分岐する条件文
  • PAの中では、次のような基本的算術関数を再帰的に定義できる
    • <
    • min, max
    • +
    • *
    • 冪乗
    • 余り %
    • 整数除算 //
  • これらの関数の基本性質は、PAの中で帰納法により証明可能である

1つの自然数でデータ構造を作る

  • 2つの自然数を1つの自然数にエンコードするために、2進表現のビットを交互に配置する方法を使える
    • 奇数位置のビットは head
    • 偶数位置のビットは tail
  • このように作った対から、再び head と tail を取り出せる
  • 対を作れるなら 連結リスト も表現できる
    • 0 を nil として使う
    • 空リスト
    • 先頭への要素追加
    • 先頭と末尾の読み出し
    • 長さの計算
    • 任意位置へのアクセス
    • 挿入と削除
  • 数、対、リストがあれば、スタック、キュー、木、テキスト文書、仮想マシンのような構造もすべて1つの自然数で表せる

Lispと計算手続きのエンコード

  • Lispは括弧構造と command and arguments という形を持つため、パースと解釈の説明がしやすい言語として使われる
  • PA内の自然数は (type, value) の対として解釈できる
    • 数値
    • 真偽値
    • 対
    • リスト
    • テキストなど
  • 自然数の中には特定の型の有効な値でないものもあるが、有効な値は一意に何らかの構造を表せる
  • このエンコードの上に、Lisp のデータ構造、Lisp 仮想マシン、Lisp インタプリタを構成できる
  • Lisp は Turing complete なので、この経路を通じて任意の計算可能手続きとその手続きの状態を PA の中にエンコードできる
  • 特定のステップ数の後の計算状態も、PA の中で表現し追跡できる

PAはPAの証明もエンコードする

  • 一階述語論理の証明は、文のリストとして見られる
    • 各文は1つの推論ステップ
    • 誤った文や誤った推論を書くこともできるが、検証手続きによって排除できる
  • PAの中で type-proof のような型を作り、証明を文リストとしてエンコードできる
  • 次の検証手続きも PA の中にエンコード可能である
    • 証明が整形式か確認する
    • 各証明ステップが有効か確認する
    • どの公理を仮定しているか確認する
    • 最後の結論が目的の文か確認する
  • ある公理系からある文の証明が存在するなら、その証明を表す特定の PA 自然数も存在する
  • PAは、その数が実際に証明コードかどうかを確認する計算を表現できるため、「PA内の証明」それ自体を PA の中で扱える
  • Gödel は計算全体をエンコードしなくても PA の中に論理をエンコードしたが、プログラマの観点では、計算のエンコードを経由して理解するやり方が自然な道筋になる

関連記事

1件のコメント

 
GN⁺ 2025-06-15
Hacker News のコメント

  • Stack Overflow の質問をブログ記事に発展させたもの
    ペアノの公理で証明できる限界と、その中で Lisp をブートストラップし始める方法を扱っている
    ひどい冗談は全部第2セクションにあり、訂正や追加の質問は歓迎

    • 記事を全部読んでみたところ、「Why Lisp?」セクションの (defun not (x) ...) の例に、括弧の対応が合っていない箇所が1つ見えた
      後の「コンピュータにバランスの取れた括弧を見つけさせるのは本当に簡単だ」と書いている部分と重なってかなり笑えたし、「Basic Number Theory」セクションの「閉じ括弧の山が見えなくなる」というコメントも面白かった
      Lisp は長いこと触っていなかったが、また追いながら要点をつかめたので良い記事だった
    • まだ導入部以降はあまり読んでいないが、Goodstein 数列の各具体例が 0 で終わることは PA の中で証明できるのに、すべての数列が終わるという命題は証明できない、という前提が興味深い
      ペアノの公理だけで計算を符号化できるという点も妙に不思議で、自己参照の層がもう1つ増えた感じがする
      最近、集合論をさらに勉強し始めて Goodstein 数列まで見たのだが、次の段階の高度な集合論の教科書や、ペアノ算術を深く扱う教科書のおすすめが知りたい
    • ブートセクタ Lispも自力でブートストラップする: https://justine.lol/sectorlisp2/
      https://t3x.org のさまざまな Lisp も、cons セルと apply/eval で数やその他を実装している
      John McCarthy のメタ循環評価器は、Alan Kay が「ソフトウェアの Maxwell 方程式」と呼んだコードで、SectorLISP では ASSOC EVAL EVCON APPLY EVLIS PAIRLIS のような形で実装されている
      一部の Forth も似ており、T3X の Zenlisp は eval/apply が相互に再帰呼び出しされる仕組みを中心に説明している: http://t3x.org/zsp/index.html
    • 「omega」と書いている箇所が2つあるが、\omega と書くべきだと思う

  • 数学とプログラミングの両方をやった立場からすると、計算の符号化そのものより、Goodstein の定理の独立性をこのような自己参照の方法で迂回できるという点のほうが興味深い
    PA +「PA は ω-無矛盾である」が Goodstein の定理を証明できる、という意味のように見えるし、もしかすると ε₀ までの超限帰納法も一般に可能なのかもしれない
    追記: PA +「PA は無矛盾である」だけでも十分なのかもしれない

    • 元の SO 質問を書いた立場から、質問に関連する回答リンクをいくつか追加した
      要するに「PA は無矛盾である」だけでは足りず、「PA が何かを証明するならそれは真である」という一様反映原理があれば十分
      この原理が ω-無矛盾性と同値かどうかは 100% 確信していないが、次を見るとそう読める: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia は T が ω-無矛盾であることを「T + RFN_T + すべての真な文の集合が無矛盾」と説明しているが、これは「T + RFN_T が真である」と同じ意味に見える
    • この再帰構造が気に入っている
      本質的には、PA が何を証明するかについてのメタ証明を作り、PA を信頼するならそのメタ証明も信頼することになる
      ただし、PA +「PA は無矛盾である」がどう十分なのかはよく分からない
      その体系は、標準自然数では Goodstein の定理が真だが、ある非標準整数 N では Goodstein の定理が偽であるようなモデルを許すように思え、まさにその場合をより強い ω-無矛盾性 が排除するように見える
    • 残念ながらそうではなく、純粋な全称式だけでは他のこともうまくいかないようだ
      つまり Con(PA) に特有の問題ではなく、より一般的な現象である: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      最初の質問に関連して、ω-無矛盾性を PA の式としてどのように符号化するのかが気になる
    • Math Exchange の投稿では、PA + ε₀ に関する超限帰納法が PA の無矛盾性を証明すると言っている
      だから PA +「PA は無矛盾である」が ε₀ に関する超限帰納法を証明できそうに見える
    • いまでは自信を持って言うには細部が少し専門外になっている
      ChatGPT は PA +「PA は無矛盾である」だけでは十分ではないと言っていたし、論理学の教科書を十分に消化しているはずなので、その主張は信じてもよさそうだ

  • 初めて ペアノ算術を使ったとき、その表現力にはかなり驚いた
    最初は基本的な体系に見えるが、計算そのものを PA の中に符号化でき、いろいろな種類の計算をまねられると気づくと、複雑に見えていたものが噛み合い始める
    こうした符号化技法を初心者に分かりやすく説明している資料のおすすめが知りたい

  • これは Boyer-Moore 理論と非常によく似ている。この理論も Peano 公理のレベルから数学を積み上げるもの
    Boyer と Moore はこの理論向けの自動定理証明器も作っており、GNU Common Lisp で動作するコピーを https://github.com/John-Nagle/nqthm/tree/master に置いている
    彼らの説明によると、プログラムをかなり優秀な数学の学生のように考えると分かりやすい。Peano 公理だけを与えても素因数分解定理を証明したり発見したりすることは期待しにくいが、Peano 公理とともに「加法の交換法則を証明せよ」「乗法が加法に対して分配的であることを証明せよ」「GCD 関数の結果が 2 つの引数を割り切ることを証明せよ」といった定理のリストを与えれば、うまく処理できるということ
    論文: https://www.cs.utexas.edu/~boyer/acl.pdf

  • Math StackExchange で JoJoModding に付けたコメントは間違っている
    「PA は自分が証明を作ると証明できるが、その証明が有限長であることは証明できないかもしれない」という説明は要点を取り違えている
    PA が「PA は X を証明する」を証明するなら、PA は X を証明できる
    重要なのは非標準モデルがあることではなく、標準自然数モデルが PA のモデルであるという点
    したがって PA が「PA は X を証明する」を証明するなら、実際に「PA は X を証明する」の符号化された証明に対応する標準的な有限自然数があり、その自然数から PA の中での X の証明を構成できる

    • 提示された自然言語版は曖昧なので、区別が重要
      示されたのは「PA が Provable(forall n, G(n)) を証明する」ではなく、「PA が forall n, Provable(G(n)) を証明する」という方
      前者なら実際に「PA が forall n, G(n) を証明する」が従うが、後者は違う
      Goodstein 数列に言及せず、一般の命題 P について forall n, Provable(P(n)) を証明するからといって Provable(forall n, P(n)) を証明できるわけではない、という論証を見たい
    • 「PA が『PA は X を証明する』を証明すれば、PA は X を証明する」という主張は真ではない
      PA の中で、PA が作れるすべての証明を検索する関数を構成でき、それをもとに、ある関数と入力が返るかどうかを分析する will-return 関数を作れる
      これは停止問題を解こうとする試みに似ていて、常に動くわけではないが、多くの場合には動作する
      ここで opposite-return を作ると、与えられた関数と入力が返らないときには返ろうとし、返るときには返らないように構成できる
      標準的な停止問題の証明と同じ方法で (opposite-return opposite-return opposite-return) を考えると、PA は「PA が opposite-return が返ると証明できるなら実際には返らない」「PA が返らないと証明できるなら実際には返る」「PA が自分が証明すると証明したものすべてを実際に証明できるなら、前の 2 つの命題のどちらかの証明を持つはずである」「したがってその場合 PA は不整合である」を証明できる
      これは Gödel の第2不完全性定理の一形態であり、だからこそ「PA が証明する」と「PA が自分が証明すると証明する」は区別されなければならない
    • 標準モデルが PA のモデルであるということは、PA が無矛盾である場合にのみ成り立ち、PA は自分が無矛盾であることを証明できない。不整合でない限り、Gödel の定理により不可能
      そのため、提案された証明は PA 内部では機能せず、そのコメントの要点もまさにその部分だと思われる

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • ある人と 帰納的データ型について話していて、Lean や Rocq の Nat のような zero/succ 定義を見せた
    相手は「これが全部なのか？ Peano 公理は？ 帰納的データ型よりさらに原始的なものはあるのか？」と尋ねてきて、興味深かった
    Peano 公理を当然内在するものと見るのではなく、複数の設計のうちの一つとして見るべきだと思い出させられた

    • 自然数は帰納的データ型よりも原始的だと見ている
      すべての 帰納的データ型は、自然数と少数の原始的な型形成子、例えば Π、Σ、=、Ω などを組み合わせて構成できるから

  • 純粋な ラムダ計算だけでも十分。ラムダ計算は計算を符号化するから

  • PA の無矛盾性に関して、PA の中で証明できる: https://youtu.be/6pjLmmkZnIA

    • 論理学者でない人には文脈が不可欠
      Gödel の第2不完全性定理は、PA が自分自身の無矛盾性を証明できるなら PA は不整合であり、したがって偽を含め何でも証明できることを示す
      リンク先の仕事は PA の不整合を示したものではなく、PA が「自己の無矛盾性を証明する」という言葉の、より弱い新しい意味を定義したうえで、PA がその弱いことをできると示したもの
      興味深い仕事だが、意味を理解するにはすでに論理学をかなり知っている必要がある

  • この記事は 123 ポイントを得ているが、リンク先の SO の投稿は賛成票が 11 個しかない

    • Stack Overflow では 15 ポイントの評判がないと賛成票を投じられない
      そこで投稿すると削除されやすいという評判の問題に 15 ポイント制限まで加わり、多くの人が賛成票を投じられないようだ