A Comment on Modal Collapse and Ultrafilters in Gödel's Ontological Argument

技術的要約：ゲーデルの存在論的証明における様相崩壊と超フィルターに関する考察

問題提起
本論文は、ゲーデルの存在論的証明に関するオドリフレディ（Odifreddi）とゴメス（Gomes）による構造的主張を取り上げる。オドリフレディとゴメスは、「様相崩回の帰結（$\varphi \supset \Box\varphi$：ある事柄が真であるならば、それは必然的に真であるという導出）」は、正的な性質を超フィルターとして特徴付け、神をその超フィルターの主要な生成者と見なすあらゆる理論に内在する構造的特徴であると断じている。彼らは、この崩壊を回避するには公理を弱める必要があるが、そうすると超フィルターの主要性や神的な存在の絶対的な最大性が犠牲になると示唆している。

著者のクリストフ・ベンツミューラー（Christoph Benzmüller）は、この崩壊は超フィルターの構造によって引き起こされるのではなく、特定の様相条件である「正性の剛性（rigidity of positivity）」（公理A4）によって引き起こされるものであると主張し、この説に異議を唱える。さらに、本論文は、ゲーデルの定理IVの導出可能性および正性の外延性に関して、オドリフレディとゴメスの分析における2つの具体的な技術的誤りを特定し、修正を行っている。

方法論
本論文は、**計算形而上学（computational metaphysics）**を用い、**対話型および自動定理証明（IATP）**を採用している。

• 形式化: 引数は、高階様相論理（HOML）の浅い埋め込みを用いたIsabelle/HOL（高階論理）を用いて形式化されている。
• 検証: 著者は、導出を検証するために自動定理証明器を使用し、反モデルを生成するためにモデルファインダーであるNitpickを利用している。
• 比較分析: 本研究では、ゲーデルの議論の異なる変種（スコット、アンダーソン、フィッティング）と、超フィルターの性質が公理（U1）として仮定されたもの、あるいは神らしさがフィルターを生成するもの（F1）といった簡略化された理論を体系的に比較している。
• 区別: 内包（intensions）（世界に依存する概念、型 $\gamma$）と外延（extensions）（個体の集合、型 $\delta$）の間の決定的な方法論的区別が維持されている。著者は、これらを混同することが超フィルターの解釈ミスにつながると論じている。

主な貢献と結果

1. 構造的崩壊の主張に対する反駁:

   • 本論文は、正的な性質が様相超フィルターを形成し、神がその主要な生成者であるという条件を満たしながらも、様相崩壊を意味しない理論が存在することを示す、機械検証済みの反例を提供する。
   • 命題1: 正的な性質が様相超フィルターを形成すると仮定し（公理U1）、含意および連言の公理（A2, A3）のみを保持した場合、神的な存在の存在は最も弱い正規様相論理（K）において導出可能であるが、様相崩壊（$\varphi \supset \Box\varphi$）は導出不可能である。
   • 命題2: さらに弱い条件、すなわち神らしさの超集合集合が様相フィルターを形成するという条件（公理F1）であっても、崩壊や一神教を意味することなく、神的な存在の必然的存在を導出するには十分である。
   • 診断: 論文は、様相崩壊の要因は超フィルターの構造ではなく、公理A4（正性の剛性：$\forall X. (PX \supset \Box(PX))$）であることを特定している。A4が除去または修正された場合（アンダーソンやフィッティングの変種のように）、超フィルターの構造が維持されたままであっても、崩壊は消失する。

2. 定理IV（神の可能性）に関する修正:

   • オドリフレディとゴメスは、ゲーデルの元の不整合性を修復した後、自動証明器が定理IV（神的な存在の可能性、$\Diamond \exists x. Gx$）を導出できないと主張した。
   • 本論文は、これが証明器の失敗ではなく、論理的事実であることを明らかにする。すなわち、ゲーデルの連言公理（Ax1）が二項連言に限定されている場合、定理IVは導出不可能である。可算個体の集合上の非主要超フィルターを含む反モデルが存在し、そこでは正的な性質の共通部分が空となる。
   • 定理IVは、公理がAx1Gen（任意、すなわち無限の連言を含む閉包）へと一般化された場合にのみ導出可能となり、これにより超フィルターが有限モデルにおいて主要であることが強制され、$P(G)$（神らしさは正的な性質である）の導出が可能となる。

3. 正性の外延性に関する修正:

   • オドリフレディとゴメスは、「正性の外延性（同じ外延を持つ性質は同様に正性的である）」は公理Ax2aおよびAx4から導出可能であると主張した。
   • 本論文は、**局所的（local）**な読み方（評価されている世界における同一の外延）の下では、これが偽であることを示している。Nitpickは、現在の世界では一致しているが、他の世界では異なり、異なる正性の判定を受ける2つの性質が存在する反モデルを見出した。
   • この前提は、**大域的（global）**な読み方（必然的な共外延）の下では成立するが、これはAx4のみから従うものである。本論文は、オドリフレディとゴメスの特定の適用においては局所的な読み方は必要ではないが、ゲーデルの直観論理からフリードマンの外延的集合論的代用物への移行を理解する上で、この区別が極めて重要であると指摘している。

4. 超フィルターの型の明確化:

   • 本論文は、$\gamma$-超フィルター（内包を扱う）と$\delta$-超フィルター（外延を扱う）を区別している。
   • 崩壊のない変種（アンダーソンのものやフィッティングのもの）において、超フィルターの構造は、内包から剛性化された外延へと移行することで生き残ることを示している。「正的な性質の超フィルター」という主張が崩壊を意味するかどうかは、それが内包的な読み方を指しているのか、外延的な読み方を指しているのかに依存する。

意義と主張
本論文は、ゲーデルの存在論的証明における様相崩壊の構造的な不可避性に関する論争を解決することを目的としている。

• 内在的崩壊の反駁: 正的な性質を主要な生成者を持つ超フィルターとして特徴付けること自体が、様相崩壊を必然的に伴うというテーゼを反駁している。崩壊は、超フィルターの構造そのものではなく、特定の様相的剛性公理（A4）の結果であることが示されている。
• ゲーデルの意図の保存: 超フィルターの構造が（剛性を緩和すれば）崩壊なしに存在し得ることを示すことで、オドリフレディとゴメスの簡略化（様相性を排除すること）は、元の議論を明確化しているのではなく、実際には異なる体系（外延的代用物）に置き換えてしまっていることを示唆している。
• 技術的精密さ: 本論文は、定理IVの導出可能性および外延性の条件に関する文献における特定の技術的な誤解を修正しており、これらの問題が、内包的および外延的な読み方の区別と、連言公理の範囲に依存していることを強調している。

著者は、「超フィルター解釈の驚くべき数学的帰結」は、様相崩壊の不可避性ではなく、「その解釈が、崩壊を避けるために、どれほどの様相性を密かに放棄しなければならないか」であると結論づけている。歴史的なテーゼ（ゲーデルは崩壊を欠陥とは見なしていなかったという点）は、これらの構造的な発見とは独立して、依然として有効であると本論文は維持している。