ペアノ算術で十分である。なぜならペアノ算術は計算をエンコードできるから

• ペアノ算術(PA) は 機械的な計算過程 を表現できるため、個々の Goodstein 列の消滅はすべて PA で証明可能である
• Cantor 標準形と遺伝的基数表記 によって Goodstein 列とその下降性などを表現でき、その結果として 有限長の証明構成が可能になる
• 帰納法（強い帰納法／超限帰納法） により、特定の次数の基数まで証明をそれぞれ拡張できる
• PA は すべての自然数 n について「G(n) が 0 に到達する」 ことを証明できるが、Goodstein 定理全体（すべての n）についての総体的な証明はできない
• PA では 計算、データ構造（List、Pair など）、さらにはプログラミング言語（Lisp）自体のエンコード や、自身の証明過程のエンコードまでも十分に実装できる

---

序論と問題の背景

• この記事は ペアノ算術(PA) が Goodstein 列について「各 n ごとに 0 に到達する（G(n) terminates）」 ことを証明できることを述べる
• これは論理学者には自明に見えるかもしれないが、プログラマが理解できるように 計算のエンコード という観点から説明している
• Goodstein 列の各ケースについて、PA の内部で 具体的な証明ルーチンを構成 できる

Ordinals（順序数）と Goodstein 列

• Von Neumann の方式で 順序数（Sets as Ordinals） を生成する
  • 0 は空集合、1 は {0}、2 は {0,1}、ω は {0,1,2,…}、ω+1 は {0,1,2,…,ω} など、順序がよく定義される
• Goodstein 列 は Cantor 標準形を用いた 遺伝的基数表記 によって記述される
  • 例: ω^ω は ((1,ω))、すなわち ((1,(1,1)))
  • < の順序は各項の基数・係数に対する辞書式比較で判定する

帰納法と超限帰納法（Transfinite Induction）

• ペアノ算術の帰納法: 0 について成り立ち、n→n+1 について成り立てば、すべての自然数について成り立つ
• 強い帰納法 も PA で証明可能である
• 超限帰納法（Transfinite induction）: ZFC などでは無限基数に対して拡張可能であり、Cantor 標準形で書かれた数に適用できる
  • Theorem 1: Cantor 標準形内の下降列は常に有限である
  • Theorem 2: Cantor 標準形の数に対して超限帰納法を用いることができる

PA における超限帰納法と Goodstein 列の証明長

• PA は 任意の n に対する Goodstein 列の消滅証明 を生成できる
  • Cantor 標準形の塔の高さ m=O(log* n)（反復対数）に応じて証明を構成できる
  • 各段階ごとに m 回の証明を組み合わせることで、全体の証明長は O(m^2) となり、または特別な表記法（ω[m]）を導入すると O(m log m) に短縮できる
• ただし、Goodstein 定理全体（すべての n）についての証明は PA では不可能である（ε0 に対する超限帰納法は不可）
  • もし可能なら、PA の無矛盾性も証明できてしまい、Gödel の第2不完全性定理と衝突する

PA のプログラム、データ構造のエンコード

• PA は計算／プログラム／データ構造（数、対、リスト、その他あらゆる構造） を十分にエンコードできる
• 次のような方法で多様な機能を実装できる:
  • 基礎論理と演算（+, *, pow, //, %, min, max など）
  • パターンマッチングと条件分岐（if, cond など）
  • 数を 2 つの数（対）としてエンコードしたり、対から再びリストなど、より複雑な構造へ繰り返し拡張したりすること（再帰的リスト、木、テキストなど）
• このようなデータ構造のエンコードにより、任意の 仮想マシン／プログラミング言語（Lisp など）のインタプリタ まで構築できる

Lisp へのブートストラップとエンコード

• Lisp を例として、基礎的な数値演算・論理演算、データ構造、プログラミング言語の評価器／インタプリタ の実装法を説明する
• Lisp の構造（命令／引数マッピング、特殊形式、macro など）はすべて PA において適切な関数の組み合わせで実装できる
• さらに PA の内部で PA の証明過程そのもの、論理証明手続き、自己言及的構造 までもすべて記号的にエンコードして実装できる

PA 内での論理自体のエンコード

• 数理論理学における一階述語論理の証明過程 を PA の数データとしてエンコードできる
• 各証明段階／命題／推論規則／正しい証明の検査を、一連の数値関数やリスト処理として認識・処理する
• このようなメタ的で自己言及的なエンコードは、Gödel の不完全性や停止問題の証明にもつながる

結論

• 計算、データ構造、プログラム、論理証明過程に至るまで、PA では十分にエンコード・証明・解釈が可能である
• したがって 任意の Goodstein 列（n に対する G(n) の消滅） は PA の内部で具体的に証明可能である
• ただし、Goodstein 定理全体（すべての n）について「PA が PA の内部で Goodstein 定理を証明する」という証明は、論理の限界上不可能である
• プログラマの観点から見ると、PA は計算そのものをエンコードできる完全な論理基盤である

[GN⁺]

Hacker Newsのコメント

• これは、私がStack Overflowで質問した内容をブログ記事にしたものです。Peano公理系で証明できることの限界と、Peano公理系の内部でどのようにLispをブートストラップするかの説明が含まれています。冗談の大半は第2節にあります。修正や追加の質問も歓迎です。
  • この記事を読みながら、"Why Lisp?" セクションで括弧が対応していない箇所を見つけました（(defun not (x) (if x false true) の例を参照）。いったん誰かが括弧を使い始めると、本能的に正しく閉じられているか確認してしまいます。そのあとで「括弧が釣り合っているかはコンピュータで簡単に判定できる」と書かれているのを見て大笑いしました。こういう冗談は本当に面白かったですし、"Basic Number Theory" セクションの ; After a while, you stop noticing that stack of closing parens. というコメントも印象的でした。久しぶりにLispに触れましたが、とても楽しく読める記事でした。
  • この記事は本当に興味深いです。まだ導入部しか読んでいませんが、Peano公理系（PA）の中ではGoodstein列のあらゆる個別のケースが 0 に到達することは証明できる一方で、「すべて」のケースが 0 に到達することは証明できないという点が面白いです（実際には当然の帰結だとしても、なおわくわくします）。そして、Peano公理系だけで計算をエンコードできるという事実は本当に奇妙です（原理的には当然ですが、以前はもう一段の自己参照を考えたことがありませんでした）。ちょうど最近、集合論をもう少し学ぼうと思って Intro to Set Theory の教科書でGoodstein列のところまで進めた経験があります。おすすめの上級集合論の教科書や、Peano算術を深く掘り下げた教科書があれば教えていただけるとありがたいです。Goodsteinの定理の証明にPAがなぜ不十分なのかを理解するのが当面の小さな目標ですが、代わりに勧められる別の道筋でも歓迎です。
  • 記事中のオメガ（omega）で、2か所ほど \omega と表記し忘れている箇所があります。
• Boyer-Moore理論と非常によく似ています。この理論はPeano公理系のレベルで数学を積み上げていくものです。BoyerとMooreはこの理論を実装した自動定理証明器を開発しており、GNU Common LISPで動作するコピーもあります。"A Computational Logic" 論文 と nqthm実装 も参照する価値があります。論文の例では、Peano公理から出発すると素数の乗算のような複雑な定理は難しい一方で、加法の交換法則、乗法の分配法則、GCD関数に関する定理などは十分に証明可能だという点が印象的でした。
• 私は数学にもプログラミングにも背景がありますが、個人的にはGoodsteinの定理の独立性の部分を自己言及的に迂回できそうだという点のほうが興味深いです。PA+「PAはオメガ無矛盾（omega-consistent）である」という前提を追加すればGoodsteinの定理を証明できるのではないかと思いますし、それによって epsilon_0 までの超限帰納法（transfinite induction）も可能になるのではないかと推測しています。EDIT: もしかすると「PAは無矛盾である」だけでも十分ではないでしょうか？
  • 残念ながらそうではありません。そして Con(PA) だけでなく、任意の普遍量化された論理式だけでも十分ではないことが知られています。関連するMath StackExchangeの回答 を参照してください。最初の質問に関連して、オメガ無矛盾性をPAの論理式としてどのようにエンコードするのか気になります。すぐには思いつかず、興味をそそられます。
  • Stack Overflowでの質問者は私です。質問には追加でいくつか回答へのリンクも書いておきました。本質的には「PAは無矛盾である」だけでは不十分ですが、「PAで証明されるなら真である」という種の「一様反映原理（uniform reflection principle）」があれば十分です。この原理がオメガ無矛盾性と完全に同じだと断言はできませんが、Wikipediaの説明 を読む限りそう読めます。T がオメガ無矛盾であるとは「T + RFN_T + すべての真な論理式の集合 が無矛盾である」という意味であり、これは「T + RFN_T が真である」ことと同値だと解釈できます。
  • 私はこうした帰納的（再帰的）な構造も気に入っています。結局のところ、PAが何を証明するかについてのメタ証明を作り、PAを信頼するならそのメタ証明も信頼できると考えています。単に「PAは無矛盾である」だけで十分だという部分は、まだはっきり理解できていません。私の考えでは、PA+「PAの無矛盾性」だと、標準自然数の範囲ではGoodsteinの定理が真であるモデルが存在する一方で、ある非標準整数 N に対してGoodsteinの定理が偽であるモデルも許してしまうように思えます。オメガ無矛盾性というより強い主張なら、こうしたケースを排除できるはずです。
  • Math StackExchangeの投稿では、PA+超限帰納法（epsilon_0）の証明がPA自身を証明すると述べられています。私としては、PA+「PAの無矛盾性」があれば epsilon_0 までの超限帰納法を証明できるように思えます。
  • このあたりになると、もう私が気軽に発言できる細部を超えている気がします。ChatGPTによれば、「PA+PAの無矛盾性」だけでは十分ではないとのことです。ChatGPTは論理学の本を相当読み込んでいるでしょうから、そういう主張なら信じられそうです。
• Stack OverflowでJoJoModdingに書いた私のコメントは正しくありませんでした。「非標準PAモデルには無限の自然数があるため、PAが自分である証明を作ったと証明しても、それが有限長であることを証明できない」と書きましたが、実際にはPAが「PAが X を証明した」と証明すれば、PA は X 自体も証明します。重要なのは非標準モデルの存在ではなく、標準自然数のモデルがPAのモデルであるという点です。したがって、「PAが X を証明することを証明した」なら、実質的には標準的な有限自然数に対応する証明が1つ生成され、その数を使ってPA内部で X の実際の証明を構成できます。
  • 論理をより詳しく検討する時間はありませんが、自然言語で見ると、「PAが forall n, G(n) を証明する」のではなく、「PAが forall n, Provable(G(n)) を証明する」という違いが核心なのだと思います。私は論理にあまり強くないので、なぜ forall n, Provable(P(n)) を証明したからといって Provable(forall n, P(n)) を証明できるわけではないのか、誰か具体的に説明してくれるとありがたいです。
  • 「PAが『PAが X を証明する』ことを証明すれば、PA は X を証明する」という命題は正しくありません。PAで可能なすべての証明を探索する関数を作ることができ、実際に回答の最後の部分でその方法を概説しました。ここから will-return や opposite-return のような関数も作れますが、これは停止性問題の標準的な証明と一致します。opposite-return(opposite-return, opposite-return) のケースを考えると、PAが opposite-return が返ることを証明すれば、実際には返らないことも証明してしまいますし、逆に返らないことを証明すれば返ることを証明してしまいます。もしPAが「証明可能なものはすべて実際に証明可能である」といった、さらに強い命題を採用してしまうなら、それはすぐにGödelの第二不完全性定理により、PAが矛盾していることを意味します。したがって、単に「PAが証明する」と「PAが自分で証明すると証明する」は必ず区別しなければなりません。
• 純粋ラムダ計算だけでも十分です。ラムダ計算自体が計算をエンコードできるからです。
• 誰かと帰納的データ型について話していて、zero/succ で作る Nat の定義（Lean や Rocq で見られるもの）を見せました。相手は「これだけで十分なのか？」「Peano公理系が必要なのか？ 帰納的データ型よりさらに原始的な何かがあるのか？」などと疑問を持っていました。Peano公理系を本質的に自明なものと思い込まず、あくまで一つの設計にすぎないと折に触れて振り返るのは大事だと思うようになりました。
  • 「帰納データ型よりもっと根本的なものがあるのか？」への答えとして、自然数そのものが帰納データ型よりもさらに原始的だと思います。すべての帰納データ型は、自然数と、少数の他の原始的な型コンストラクタ（Π, Σ, =, Ω）だけで構成できます。
• Kirby-Parisの定理に関するQ&A も参照してください。
• PAの無矛盾性について、PA内部で証明可能であることを説明する動画資料を共有します。YouTubeリンク
  • これは非論理学者にとってぜひ説明が必要な点です。Gödelの第二不完全性定理によれば、もしPAが自分自身の無矛盾性を証明できるなら、PAは矛盾していることになります（偽を含めて何でも証明できるようになります）。この動画は、PAが矛盾していることを証明しているのではなく、PAがより弱い意味で「自分の無矛盾性」を証明できることを示しています。論理学の基礎を知らなければ正確に理解するのは難しい内容ですが、それでも十分に興味深いです。
• この話題は123ポイントも取っているのに、肝心のSOに投稿された元の本文は11アップボートしかありません。
  • Stack Overflowではアップボートするのに15ポイント必要です。評判システムのせいで人々が投稿したがらないこともありますし、15ポイントという制限がアップボートを妨げているのだと思います。
• 計算だけで十分なのでしょうか？ 計算可能実数は実数全体の部分集合です。
  • 「実数」という名前自体が誤解を招く呼び方だと思います。実数は現実の物理的な比を意味すると解釈することもできます。たとえば 180.255ポンドと言えば、ジョーンズの実際の体重と標準ポンドとのあいだの現実の物理的な比を意味します。こうした比も物理的に存在している、つまり実数は物理的な比として解釈できるわけです。一方で現在では、数を現実から切り離された抽象概念として見る立場が優勢で、これは典型的にはプラトン主義的な見解です。しかし現実には、無限の精度で何かを測定したり表現したりすることは不可能です。たとえば50桁を超える精度の測定は量子力学的な制約により不可能です。もし太陽系天体の軌道を誤差なく測ろうとして50桁以上に進めば隣接する恒星の質量効果を、100桁以上では銀河全体をモデル化する必要があり、最終的には実測不能な物理的影響まで考慮しなければなりません。したがって現実には有限精度の数学しか可能ではありません。つまり原理上はすべてが計算可能だとしても、無限に向かうにつれて数学的モデル自体が無意味になっていきます。
  • 本当にそうでしょうか？ 実は、非可算（uncountable）のほうが多いという発想は誤解から出発しています。私の説明投稿 を参照してください。非可算のもののほうが多いと受け入れるなら、「存在」について論争的な立場を取らざるを得ません。関連する議論 も参照してください。最後に、どこまでも論理を展開したとしても、最終的にはコンピュータで表現できます。巨大基数をZFCに加えたとしても、PAから出発して任意の結論まで推論できますから、実質的にはPAだけで十分だと私は考えます。さらに説得が必要なら、Gödel, Escher, Bach をおすすめします。
  • 私の考え方は少し違います。一般の実数そのものは、計算・記号化・記録などいかなる形でも扱えませんが、実数に関する「命題」自体は有用な形で表現したり計算したりできる場合がよくあります。Harvey Friedmanや今回の記事の著者のように、単純な体系から想像以上に複雑な値を生み出そうとする試みは本当に興味深いです（参考までに、audiomulchのWebサイトにはアクセスできませんでした）。
  • 「十分だ」という言葉に何の目的も付いていない限り、この問いは定義が曖昧です。何のために十分なのかが重要です。
  • 「計算だけで十分なのか？」という問い自体が間違っていると思います。もちろん十分ではありません。もし十分なら、現実を信じやすい時計じかけのようなものだとみなす一部の考え方がすべて正しいことになってしまいます。現実はそれよりもずっと面白く、複雑です。