On a Question of Hamkins'

ハムキンスの問いに対し、拡張性の要件を緩めた「条件付き拡張性」の下では$\Pi^0_1$-柔軟なロサ式が存在することを示す一方、完全な拡張性を持つロサ式は存在しないことを証明し、さらに「整合的拡張性」の場合の解決を未解決問題として残した。

要約

1. 物語の舞台：「PA」という巨大な図書館

まず、PA（ペアーノ算術）というものを想像してください。これは、足し算や掛け算のルールが完璧に記された、巨大な「数学の図書館」です。
この図書館には、すべての正しい数学の定理が収められているはずですが、実は「完全な百科事典」を作ることはできないという悲しい事実（不完全性定理）があります。つまり、この図書館には「正解かどうか、図書館のルールだけでは判断できない問題」が必ず存在します。

2. ハムキンス博士の問い：「魔法の鏡」は作れるか？

この論文のきっかけは、ジョエル・ハムキンスという学者が投げかけた質問です。

「もし、ある数学の問題（$\phi$）が『正解かどうか分からない状態』にあるとき、**『その問題に対する答え』を自動的に決める魔法の鏡（$\rho$）**を作れるだろうか？」

この「魔法の鏡」には、2 つの条件が求められました。

1. 独立していること（Independence）：
   鏡が「YES」と言っても「NO」と言っても、図書館（PA）は矛盾せずに生き残れること。つまり、鏡の答えが正解でも不正解でも、図書館のルールは壊れない。
2. 拡張性（Extensionality）：
   これが重要なんです。鏡は**「中身が同じなら、同じ答えを出さなければならない」**というルールです。
   例えば、「2+2=4」と「4=2+2」は中身が同じなので、鏡はどちらに対しても同じ答え（YES か NO）を出さなければなりません。

ハムキンス博士は、「そんな魔法の鏡は作れるか？」と聞きました。

3. 著者の結論：「完全な魔法の鏡」は存在しない

著者のアルベルト・ヴィッサーは、**「いいえ、そんな完全な魔法の鏡は作れません」**と答えました。

【なぜ作れないのか？】
これは**「鏡のジレンマ」のようなものです。
もし、鏡が「中身が同じなら同じ答えを出す（拡張性）」というルールを厳格に守ろうとすると、ある瞬間に鏡が「自分自身を否定する」ような矛盾した状況に陥ってしまいます。
まるで、「この文章は嘘です」と言っているようなパラドックス（矛盾）が起き、図書館のルールが崩壊してしまうのです。
つまり、「中身が同じなら同じ答えを出す」という「公平さ（拡張性）」を完璧に保とうとすると、「独立して自由な答えを出す」という「柔軟性」**が失われてしまうのです。

4. 解決策：「条件付きの魔法の鏡」

しかし、著者はここで諦めませんでした。条件を少しだけ緩めれば、魔法の鏡は作れることを発見したのです。

「完全な公平さ（拡張性）」を「条件付きの公平さ（Conditional Extensionality）」に変えるのです。

• 元のルール（完全な公平さ）： 「中身が同じなら、どんな状況でも同じ答えを出す」
• 新しいルール（条件付き公平さ）： 「中身が同じなら、**『その問題が正しいと仮定した状況』**では同じ答えを出す」

これならどうなるか？
著者は、**「ゆっくり進む証明（Slow Provability）」という新しい技術を使って、「条件付きの魔法の鏡」**を作りました。

• この鏡の能力：
  • 問題が「正解かどうか分からない状態」なら、鏡は**「どんな Π01（複雑な数式）の答えにも合わせられる」**という驚異的な柔軟性（$\Pi^0_1$-Flexibility）を持っています。
  • つまり、鏡は「あなたが『A』と言いたいなら『A』、『B』と言いたいなら『B』と、あなたの希望に合わせて答えを変えられる」のです。
  • ただし、そのためには「その問題が正しいと仮定していること」が前提条件になります。

5. 残った謎：「一貫した公平さ」はどうなる？

論文の最後には、まだ解決していない**「最後の難問」**が残されています。

• 完全な公平さ： 矛盾している問題に対しても同じ答えを出す（これは不可能と判明）。
• 条件付き公平さ： 正しいと仮定した時に同じ答えを出す（これは可能）。
• 中間の公平さ（一貫した公平さ）： **「矛盾していない問題（一貫した問題）に対してだけ、同じ答えを出す」**ルールはどうなる？

これは、「完全な公平さ」と「条件付き公平さ」の中間に位置するルールです。
「矛盾している問題」は除外して、「矛盾していない（一貫した）問題」に対してだけ公平であれば、魔法の鏡は作れるのでしょうか？

著者は**「これはまだ分かりません」**と答え、この問題を次の研究者に託しています。

---

まとめ：この論文が教えてくれること

1. 完璧な「自動判定機」は作れない：
   「中身が同じなら、どんな状況でも同じ答えを出す」という**「完全な公平さ」と、「正解かどうか分からない自由な答えを出す」という「柔軟性」**を両立させることは、数学的に不可能です。
2. 条件を緩めれば可能：
   「その問題が正しいと仮定した時のみ、公平に振る舞う」という**「条件付きの公平さ」**なら、非常に強力な「柔軟な魔法の鏡」を作ることができます。
3. まだ謎は残っている：
   「矛盾していない問題に対してだけ公平にする」という**「一貫した公平さ」**ではどうなるかは、まだ誰も答えを持っていません。

一言で言うと：
「完璧な公平さで自由な答えを出す機械は作れないけど、少しルールを緩めれば、驚くほど柔軟な機械は作れるよ。でも、その中間のルールについては、まだ謎なんだよ」という、数学的な探検の記録です。

技術概要

1. 問題の背景と定義

ハムキンスの問い（Question 28）
Joel Hamkins は、以下の 2 つの性質を満たす $\Pi^0_1$ 形式式 $\rho(x)$ の存在を問いました。

1. 独立性（Independence）: 理論 $PA + \varphi$ が無矛盾であれば、$PA + \varphi + \rho(\ulcorner\varphi\urcorner)$ と $PA + \varphi + \neg\rho(\ulcorner\varphi\urcorner)$ の両方が無矛盾である。
2. 拡張性（Extensionality）: $PA \vdash \varphi \leftrightarrow \psi$ ならば、$PA \vdash \rho(\ulcorner\varphi\urcorner) \leftrightarrow \rho(\ulcorner\psi\urcorner)$ である。

このような形式式を「拡張的ロサー形式式（extensional Rosser formula）」と呼びます。Hamkins は、この形式式が任意の複雑さ（complexity）で許容される場合でも存在するかを問いました。

2. 主要な結果

ヴィッサーはこの問いに対して、以下の 3 つの主要な結論を導き出しました。

A. 拡張的ロサー形式式の非存在（否定解答）

定理 2.1: $R$（タルスキ・モストフスキー・ロビンソン理論）を拡張する任意の一貫した理論 $U$ において、拡張的ロサー形式式は存在しない。

• 証明の概要: 固定点定理を用いて、$\varphi_0 \leftrightarrow \rho(\ulcorner\varphi_0\urcorner)$ と $\varphi_1 \leftrightarrow \neg\rho(\ulcorner\varphi_1\urcorner)$ を構成します。独立性の仮定から $\varphi_0$ と $\varphi_1$ はどちらも矛盾（$\bot$）と同値であることが導かれ、拡張性により $\rho(\ulcorner\bot\urcorner)$ と $\neg\rho(\ulcorner\bot\urcorner)$ が両方証明可能となり、理論 $U$ の無矛盾性と矛盾します。
• 意味: Hamkins の問いに対する直接的な答えは「No」です。完全な拡張性を持つロサー形式式は、一貫した理論では構成できません。

B. 条件付き拡張性における $\Pi^0_1$ 柔軟性の存在（肯定的解答）

拡張性を「条件付き拡張性（Conditional Extensionality）」に弱めることで、肯定的な結果が得られます。

• 条件付き拡張性: $PA \vdash \varphi \leftrightarrow \psi$ ならば、$PA + \varphi \vdash \rho(\ulcorner\varphi\urcorner) \leftrightarrow \rho(\ulcorner\psi\urcorner)$。
• $\Pi^0_1$ 柔軟性（$\Pi^0_1$-Flexibility）: $PA + \varphi$ が無矛盾であれば、任意の $\Pi^0_1$ 文 $\pi$ に対して、$PA + \varphi + (\rho(\ulcorner\varphi\urcorner) \leftrightarrow \pi)$ は無矛盾である。

定理 4.12: $PA$ を拡張する計算可能に列挙可能な（c.e.）理論 $U$ に対して、条件付き拡張性を満たし、かつ $\Pi^0_1$ 柔軟性を持つ $\Pi^0_1$ 形式式 $\rho(x)$ が存在する。

• この形式式は、Shavrukov と Visser による以前の $\Delta^0_2$ 形式式の結果を、複雑さを $\Pi^0_1$ に下げつつ、条件付き拡張性を維持する形で改良したものです。

C. 未解決の問題

問い 1.2: 「整合的拡張性（Consistent Extensionality）」を満たすロサー形式式は存在するか？

• 定義: $PA \nvdash \neg\varphi$ かつ $PA \vdash \varphi \leftrightarrow \psi$ ならば、$PA \vdash \rho(\ulcorner\varphi\urcorner) \leftrightarrow \rho(\ulcorner\psi\urcorner)$。
• これは完全な拡張性と条件付き拡張性の中間の概念です。この問いは現在も未解決（Open Question）として残されています。

3. 手法と技術的構成

この論文の証明は、以下の概念と手法を組み合わせることで構成されています。

1. 一様証明（Uniform Provability）と「小ささ（Smallness）」:

   • 証明の長さや公理の「小ささ」を定義する概念を導入します。
   • 形式式 $\varphi$ に対して、$x$ が $\varphi$-small であること（$S_\varphi(x)$）を定義します。これは、$x$ 以下の証明で導かれる $\Sigma^0_1$ 文が真であることを意味します。
   • 重要な性質として、$U+\varphi$ は任意の標準数 $n$ が $\varphi$-small であることを証明できます（定理 4.4）。これは「外側では大きくても、内部では小さい」という原理の一例です。

2. 遅延証明（Slow Provability）:

   • 通常の証明ではなく、「$\varphi$-small な公理」からの証明のみを許容する「遅延証明」$\triangle_\varphi \psi$ を定義します。
   • これはフェルマン（Feferman）型の証明可能性述語の一種であり、$\triangle_\varphi$ は $U+\varphi$ 上でロブの条件（Lob's Conditions）を満たします（定理 4.7）。

3. 排出（Emission）と吸収（Absorption）:

   • 排出（Theorem 4.10）: $\square_\varphi \psi \to \square_\varphi \triangle_\varphi \psi$。
   • 吸収（Theorem 4.11）: $\square_\varphi \triangle_\varphi \psi \to \square_\varphi \psi$。
   • これらの性質を用いることで、遅延証明可能性述語の振る舞いを制御し、$\Pi^0_1$ 柔軟性を導出します。

4. 構成:

   • 最終的に構成される $\rho(x)$ は、遅延証明可能性述語 $\triangle_\varphi \top$（すなわち、$\varphi$-small な公理から矛盾が導かれないこと）に基づいています。
   • この構成は固定点フリー（fixed-point-free）であり、Shavrukov-Visser の構成法を「遅延証明」の枠組みに適用・適応させたものです。

4. 意義と結論

• 理論的意義:
  • Hamkins の問いに対する「完全な拡張性」の不可能性を示すことで、ロサー形式文の性質に関する理解を深めました。
  • 「条件付き拡張性」というより弱い条件の下では、$\Pi^0_1$ 形式式でさえも強力な柔軟性（$\Pi^0_1$-flexibility）を実現できることを示しました。これは、ロサー形式文の複雑性と拡張性のトレードオフ関係を明確にしました。
• 方法論的貢献:
  • 「遅延証明（Slow Provability）」と「一様小ささ（Uniform Smallness）」の概念を、拡張性や柔軟性の問題に応用する新しい手法を示しました。
  • 証明可能性論（Provability Logic）の手法（特にロブの定理やフェルマン述語）を、形式式の拡張性という文脈で再解釈・拡張しています。
• 今後の課題:
  • 「整合的拡張性（Consistent Extensionality）」のケースが未解決であるため、完全な拡張性と条件付き拡張性の間の境界線がどこにあるかは、今後の研究課題として残されています。

総じて、この論文は不完全性定理の文脈における形式式の振る舞い、特に「拡張性」と「独立性」の両立可能性について、厳密な境界を引く重要な成果です。