今日も、意味のないことをやってしまったよ…
∀x[G(x) → ∀F(Perf(F) → Has(x,F))]
これは「神とは定義上すべての完全性を有する存在である」という定義命題で、Perf(Ex) は「存在すること（Ex）が完全性のひとつである」という意味です。この二つと「神の観念を我々は持つ（G(d)）」とを組み合わせれば、Has(d, Ex) が全称例化と前件肯定によって導出され、Ex(d) が帰結します。
↓
Claudeでコード化
# ================================================================
# アンセルムス＋デカルト：存在論的証明の記号論理モデル
# 推論規則：全称例化（UI）、前件肯定（MP）
# ================================================================
from itertools import product
# --- 述語の定義 ---
entities = {'d'} # d = 神の観念（概念としての神）
properties = {'Ex', 'Om', 'Bn'} # Ex=存在, Om=全能, Bn=善性（例示）
def G(x):
"""神の概念である"""
return x == 'd'
def Perf(F):
"""Fは完全性のひとつ"""
# P2: 存在は完全性。他の性質も完全性として追加可能
perfections = {'Ex', 'Om', 'Bn'}
return F in perfections
has_properties: dict[str, set] = {x: set() for x in entities}
def Has(x, F):
"""xはFという性質を持つ"""
return F in has_properties[x]
def Ex(x):
"""xは（実在として）存在する"""
# 橋渡し公理：Has(x, 'Ex') ならば Ex(x)
# ※ カントはここを批判：「存在は性質ではない」
return Has(x, 'Ex')
# --- 推論エンジン ---
def apply_P1_universal_instantiation(x):
"""
P1: ∀x[G(x) → ∀F(Perf(F) → Has(x,F))]
全称例化 x=d → G(d) → ∀F(Perf(F) → Has(d,F))
"""
if G(x):
for F in properties:
if Perf(F):
has_properties[x].add(F) # Has(x, F) を導出
return True
return False
# --- 推論を順にトレース ---
print("=" * 50)
print("存在論的証明：推論トレース")
print("=" * 50)
print(f"\n[P3] G(d) = {G('d')} ← 神の観念を我々は持つ")
print(f"[P2] Perf('Ex') = {Perf('Ex')} ← 存在は完全性のひとつ")
print("\n[Step 1-4] P1をx=dで全称例化 → MPを適用 → Has(d, F) を導出")
result = apply_P1_universal_instantiation('d')
print(f" 導出されたdの性質: {has_properties['d']}")
print(f"\n[Step 4] Has(d, 'Ex') = {Has('d', 'Ex')}")
print(f"[Step 5] Ex(d) = {Ex('d')}")
print("\n[橋渡し公理の明示]")
print(" Has(d, 'Ex') → Ex(d) は追加公理が必要")
print(" カント批判：'Ex'（存在）は述語ではなく量化子である")
print(f" → この公理を認める場合、Ex(d) = {Ex('d')}")
print(f" → この公理を拒否する場合、Ex(d) = 証明不可能")
==================================================
存在論的証明：推論トレース
==================================================
[P3] G(d) = True ← 神の観念を我々は持つ
[P2] Perf('Ex') = True ← 存在は完全性のひとつ
[Step 1-4] P1をx=dで全称例化 → MPを適用 → Has(d, F) を導出
導出されたdの性質: {'Ex', 'Om', 'Bn'}
[Step 4] Has(d, 'Ex') = True
[Step 5] Ex(d) = True
[橋渡し公理の明示]
Has(d, 'Ex') → Ex(d) は追加公理が必要
カント批判：'Ex'（存在）は述語ではなく量化子である
→ この公理を認める場合、Ex(d) = True
→ この公理を拒否する場合、Ex(d) = 証明不可能
結論
コードが炙り出す哲学的論点
このコードの核心的な価値は、証明の「裂け目」を可視化することにあります。Ex(d) が True を返すのは、Has(x, 'Ex') → Ex(x) という橋渡し公理を黙って def Ex(x) の中に埋め込んでいるからです。カントの批判はまさにここを突く——「存在は述語（properties の要素）ではない」とするならば、'Ex' を properties の集合に入れた瞬間に論証は循環しているのです。コードはその循環を、def Ex(x) の関数定義として白日の下にさらします。
【解説】
述語とは、主語についての規定与えるものです。「リンゴは赤い」において、「赤い」はリンゴという主語に新たな内容的規定を付け加えています。
主語の概念を展開・拡張するので、述語は概念の内容を豊かにします。
カントは「存在する」は、そのような述語ではないと考えます。
「神は全能である」という文では、「全能」が神概念に内容を増やしています（赤いと同じ）。しかし「神は存在する」という文では、「存在する」は神の概念に何か新たな性質（赤い）を追加しているのではなく、「実在」のレベルに無理やり持ってきているということです。
神の概念の中に「存在」が含まれている。
故に神は存在する。
は、路線が違いすぎるというわけ。
だから、「神の存在証明」はダメだってことになっています。
Nano banana2で生成
