On a Theorem by Bezboruah & Shepherdson

本論文は、ベズボロアとシェパードソンによる弱理論 PA⁻ の無矛盾性証明不可能性に関する定理の意義を巡るクレイゼルの批判を退け、プドラークの定理との比較を行うとともに、ニールセンとマルコフの洞察に基づく符号化を用いて同定理を再証明するものである。

要約

この論文は、数学の「不完全性定理」という非常に難解なテーマについて書かれていますが、著者のアルベルト・ヴィッサーさんは、それを**「偉大な定理の影に隠れた、忘れられた小さな英雄の物語」**として描いています。

わかりやすくするために、いくつかの比喩を使って説明しましょう。

1. 物語の舞台：「不完全性定理」という巨大な城

まず、背景にあるゲーデルの第二不完全性定理を想像してください。これは数学界の「巨大な城」のようなものです。

• 定理の意味： 「ある数学のルール（理論）が、自分自身に矛盾がないことを証明することは、そのルールが矛盾を含んでいるか、あるいは証明能力が不足しているかのどちらかしかない」という、とても強力なルールです。

2. 登場人物と対立：「クレイゼル」と「ベズボルア＆シェパードソン」

この城の入り口で、2 つのグループが出会います。

• クレイゼル（批判者）：
  彼は「この巨大な城の門は、『Q』という小さな村（非常に単純な数学のルール）には適用できない」と言います。

  • 彼の主張： 「Q という村はあまりに貧弱で、足し算の交換法則さえ証明できない。だから、Q が『自分自身は矛盾していない』と言ったとしても、それは単なる代数の式に過ぎず、本当の『矛盾のなさ』を表現しているとは考えられない。だから、Q に対してこの定理を適用しても意味がない」と主張しました。
  • 比喩： 「子供が『私は嘘をつかない』と言っても、その子供がまだ言葉を十分に理解していないなら、その言葉の重みは本物ではない」と言っているようなものです。

• ベズボルア＆シェパードソン（挑戦者）：
  彼らは 1976 年、「いや、Q という小さな村でも、自分自身の矛盾を証明できないことは技術的に証明できる！」と反論しました。

  • 彼らの成果： クレイゼルの言う「貧弱さ」を逆手に取り、Q 内で矛盾を導き出す「偽の証明」が作れるような奇妙な世界（モデル）を構築しました。つまり、「Q には矛盾がない」という言葉を Q 自身で証明することはできない、という事実を突きつけました。
  • 結果： しかし、クレイゼルの権威が強かったため、彼らの論文は「 apologetic（謝罪調）」なトーンで書かれ、その後は長い間、忘れ去られてしまいました。

3. 著者の主張：「忘れられた宝石の再評価」

この論文の著者ヴィッサーさんは、**「クレイゼルの批判は正しくない。ベズボルア＆シェパードソンの発見は、実はとても重要で美しい」**と言っています。

• なぜ重要なのか？
  クレイゼルは「意味が通じないから無意味だ」と言いましたが、ヴィッサーさんは「意味は強い理論（Peano 算術など）から与えられたものでよく、弱い理論でも同じ意味を持つ」と考えます。
  • 比喩： 「ZFC（強力な数学のルール）で証明された『3 で割る』という計算が、ZF（選択公理なし）では意味が変わるなんてありえないでしょう？弱い理論でも、強い理論と同じ『意味』で考えられるはずだ」という主張です。

4. 新しい発見：「マークov 暗号」という新しい鍵

著者は、ベズボルア＆シェパードソンの証明を、**「マルコフ暗号（Markov Coding）」**という新しい技術を使って、よりシンプルに再証明しました。

• どんな仕組み？
  彼らは、整数を「行列（数字の箱）」に変換する特別な方法を使います。
  • 比喩： 普通の証明は「長い文章」ですが、彼らの方法は「レゴブロック」を組み立てるようなものです。
  • 証明の核心：
    1. 非標準的な「巨大な世界（モデル）」を用意します。
    2. その世界には、**「矛盾（⊥）」と「矛盾の前提（⊥→⊥）」**という 2 つの特別なブロックがあります。
    3. 通常、これらを並べると「矛盾」にはなりません。しかし、著者が作った特殊な世界（K というモデル）では、「前提のブロック」が見えなくなってしまうのです。
    4. その結果、その世界に住む人々にとっては、**「前提もなしに、いきなり『矛盾』が証明されてしまった」**ように見えてしまいます。
    5. つまり、その世界（理論 PA-）の中では、「矛盾がない」という主張が証明できない、という事実が浮き彫りになります。

5. 結論：なぜこの話が必要なのか？

著者は、この論文を通じて 3 つのメッセージを伝えています。

1. 歴史的な正義： クレイゼルの批判は正しくなく、ベズボルア＆シェパードソンの功績は正当に評価されるべきだ。
2. 教育的な価値： この証明は、数学のモデルがどうやって「矛盾」を隠したり、見せかけたりするかを視覚的に理解するのに役立つ。
3. 技術的な美しさ： 古い証明を、新しい「行列（レゴブロック）」のアイデアを使って、より美しく再構築した。

まとめ

この論文は、**「数学の偉大な定理（不完全性定理）が、最も単純なルール（Q や PA-）の小さな村でも、どんなに貧弱でも、自分自身を完全には証明できないという事実」**を、新しい視点と技術で再発見し、その美しさを再評価しようとする物語です。

クレイゼルという「厳格な審査員」に否定された小さな発見が、実は「数学の深淵」を覗くための重要な鍵だった、というワクワクする話なのです。

技術概要

アルベルト・ヴィッサー（Albert Visser）による論文『ON A THEOREM BY BEZBORUAH & SHEPHERDSON』の技術的な要約を以下に示します。

1. 研究の背景と問題設定

• 主題: ベズボルア（Bezboruah）とシェパードソン（Shepherdson）が 1976 年に証明した定理（以下、BS 定理）の再検討と、その意義の再評価。
• 核心となる問題: 第二不完全性定理は、通常、ペアノ算術（PA）のような強い理論において「理論は自身の無矛盾性を証明できない」と述べる。しかし、非常に弱い理論であるロビンソン算術（Q）や、離散順序可換環の非負部分を表す PA$^-$ においても、同様の結果が成り立つかどうかは長年議論されてきた。
• クレイゼルの批判: ジョージ・クレイゼル（Georg Kreisel）は、Q や PA$^-$ のような弱い理論では、証明可能性述語がヒルベルト・バーンヤス条件（Hilbert-Bernays conditions）を満たさず、したがって「無矛盾性」を意味的に表現していないと主張し、BS 定理の哲学的・数学的意義を否定していた。
• 本論文の目的:
  1. クレイゼルの批判が誤りであることを論理的に示す。
  2. BS 定理とパヴェル・プドラーク（Pavel Pudlák）による第二不完全性定理の現代的拡張（Q における結果）を比較し、両者の違いと関係を明確にする。
  3. ニールセン（Nielsen）とマルコフ（Markov）の洞察に基づいた新しい列符号化（マルコフ符号化）を用いて、BS 定理の新たな証明を提供する。

2. 主要な論点と批判的検討（第 2 章）

• クレイゼルの批判への反論:
  • クレイゼルは、弱い理論内で証明可能性述語の性質が証明できない場合、その述語は「無矛盾性」を表現しないと主張した。
  • 著者は、意味は理論の強さに依存して変化するものではなく、真の算術（True Arithmetic）の文脈において適切な公式が「無矛盾性」を表現すると仮定すれば、弱い理論内での証明可能性の欠如は意味の欠如を意味しないと反論する。
  • 推論主義的立場であっても、弱い部分理論が何を示せるかという問い自体に技術的・教育的価値がある。
• 技術的意義: BS 定理は、Q や PA$^-$ において無矛盾性が証明不可能であることを示す「技術的な挑戦」であり、そのモデル構成（離散順序環のモデル）は、矛盾証明が具体的に可視化できる点で教育的価値が高い。

3. 第二不完全性定理との比較（第 3 章）

• プドラークの定理（Gödel-Pudlák 版）:
  • 理論 $U$ が $S^1_2$（多項式時間計算可能性の理論）を解釈し、かつ $U$ が自身の無矛盾性を証明できるなら、$U$ は矛盾する。
  • プドラークは、$Q$ が定義可能なカット上で $S^1_2$ を解釈することを示し、これにより $Q$ における第二不完全性定理が導かれる。
  • このアプローチは、証明系やゲーデル数化の具体的な形式に依存せず、解釈可能性（interpretability）に焦点を当てている。
• BS 定理との違い:
  • 手法: BS 定理は、$\beta$-関数による列符号化と、ヒルベルト様式の証明系に依存した具体的なモデル構成（矛盾証明の存在するモデルの構築）を用いる。
  • 一般性: プドラークの結果は解釈可能性の観点から一般化されるが、BS 定理は特定の符号化と証明系に依存しており、解釈可能性のバージョンには直接拡張できない。
  • 結論: 両者は $Q$ の無矛盾性の非証明という点で一致するが、アプローチと到達する範囲は「全く異なる結果」として捉えるべきである。

4. 新たな証明：マルコフ符号化を用いた BS 定理の再証明（第 4 章）

著者は、従来の $\beta$-関数に代わる、マルコフ符号化（Markov Coding） を用いて BS 定理を再証明する。

• マルコフ符号化の基礎:
  • 整数行列の群 $SL_2(\mathbb{Z})$ の非負部分 $SL_2(\mathbb{N})$ が、2 つの生成元 $A = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}$ と $B = \begin{pmatrix} 1 & 0 \\ 1 & 1 \end{pmatrix}$ による自由モノイドと同型であるという事実（ニールセンの洞察）を利用する。
  • 列 $n_0, \dots, n_{k-1}$ を $B A^{n_0} \dots B A^{n_{k-1}}$ として符号化する。これを「ur-strings」と呼ぶ。
• 証明の概要:
  1. モデルの構成: 真の算術の非標準モデル $M$ と、その要素的末端拡張（elementary end-extension）$N$ を考える。
  2. 行列の定義: $N$ 内で、非標準数 $a \in M$ と $b \in N \setminus M$ を用いて行列 $\beta = [n]^a [m]^b$ を構成する（ここで $[n] = B A^n$）。
  3. 部分モデル $K$ の抽出: $K_0$ を $N$ の部分環として構成し、その非負部分 $K$ を PA$^-$ のモデルとする。
  4. 矛盾証明の存在:
     • $K$ 内では、$\beta$ は「ur-string」として存在し、かつその構成要素として $n$（公理 $\bot \to \bot$ のゲーデル数）と $m$（結論 $\bot$ のゲーデル数）を含む。
     • しかし、$K$ 内では $a$（$n$ の繰り返し回数）が存在しない（$x_1$ が $K_0$ に属さないことを示す）。
     • 結果として、$K$ 内ではこの列 $\beta$ が「公理から $\bot$ への証明」として機能してしまう（公理部分と結論部分の境界が欠落するため）。
  5. 結論: $PA^-$（および真の普遍文を含む拡張）は、BeSh（極めて弱い理論）の無矛盾性を証明できない。

5. 主要な貢献と結果

• 理論的貢献: クレイゼルの批判を退け、BS 定理の正当性と重要性を再確認した。
• 技術的貢献:
  • プドラークの結果（解釈可能性ベース）と BS 定理（モデル構成ベース）の明確な対比。
  • マトリックス理論（$SL_2(\mathbb{N})$ の自由モノイド同型性）と非標準モデル論を組み合わせた、BS 定理の新しい証明法の提示。
  • 証明の過程で、ChatGPT を活用して行列の固有値と漸化式の関係を整理し、証明の効率化を図った点（付録的貢献）。
• 教育的価値: 弱い理論における矛盾証明が具体的にどのように「見えて」しまうかをモデル構成を通じて可視化しており、$\Pi^0_1$ 文と普遍文の違いを理解する上で有益である。

6. 意義

本論文は、第二不完全性定理の適用範囲に関する長年の議論に決着をつけ、弱い理論における無矛盾性の非証明が単なる技術的トリックではなく、深い意味を持つ結果であることを示した。また、マルコフ符号化を用いた新しい証明法は、算術的符号化とモデル理論の新たな接点を示唆しており、計算量理論や証明論の今後の研究に寄与する可能性がある。