哥德尔对上帝存在的本体论证明

为方便阅读, 我把形式化了的哥德尔的本体论证明截图放在下面. 注意, 我在下文会用 □ 代替oldgoat的圆圈中有个点的符号(不会在Latex里打那个符号, 哈哈), 来表示模态逻辑中的必然算子：

Ax. 1. ∀φ∀ψ (P)φ) ∧ □∀x(φ(x)→ψ(x)))→P(ψ)

Ax. 2. ∀φ P(¬φ) ⇔ ¬P (φ)

Th. 1.∀φ P (φ)→♢∃x(φ(x))

Df. 1. G(x)⇔∀φ(P(φ))→φ(x))

Ax. 3.P(G)

Th. 2.♢∃xG(x)

Df. 2.∀φ φ ess x⇔φ(x)∧∀ψ(ψ(x)→□∀y(φ(y)→ψ(y)))

Ax. 4.∀φ P(φ)→□P(φ)

Th. 3.∀x G(x)→G ess x

Df. 3 E(x)⇔∀φ(φ ess x→□∃yφ(y))

Ax. 5 P(E)

Th. 4. □∃xG(x)

引用oldgoat老师对Ax.1和Ax.2的翻译：

翻译：Ax.1. 任意由积极性质衍推而来的（如严格蕴涵的）性质都是积极性质。

翻译：Ax.2. 一个性质是积极的，当且仅当其否定是不积极的。

我们证明Th.1.∀φ P(φ) → ◇∃x φ(x)，翻译： 所有积极性质都有可能存在例示(或: 所有积极性质都在某个可能世界被实例化)

证明：

我们采用反证法, 假设¬(∀φ P(φ) → ◇∃x φ(x)) , 根据经典逻辑可得: ∃φP(φ) ∧ □ ∀x ¬φ(x)，即"存在一必然无实例的积极性质". 为方便阅读, 我们把这个积极性质在接下来的证明里暂且叫做 φ .

所以对于任意语句ψ , φ(x) → ψ(x) 必然为真. 此时用 ¬φ 替换 ψ , 得到 φ(x) → ¬φ(x). 由于 φ 蕴含其否定, 所以 φ 和 ¬φ 同为积极性质, 与Ax.2.矛盾. 证毕.

此时我们再需要Df.1. 和Ax.3. 再次引用oldgoat的翻译(注意, 对于"类上帝的"这一性质的定义我们两个的不一样, 这个在文末会有说明.)

Df.1. x是类上帝的，当且仅当它的属性是所有积极的（positive）性质

Ax.3. 性质“类上帝的”是积极性质

此时我们可以证明Th.2.◇∃x G(x). 翻译: 可能存在(即在某个可能世界上存在)类上帝属性的实例.

证明：

因为性质“类上帝的”是积极性质, Th.1.中用G替换φ , P(G)使前件得到满足, 所以Th.2.得证.

现在引入Df.2.和Ax.4. 注意, 我这里的Df.2.跟oldgoat老师的Df.2.略有不同, 所以我的翻译是基于他的之上改动的. 至于不同的原因后面会说.

Df.2.φ 是x的本质属性，当且仅当，[[x是 φ 的一个实例]并且[对任意性质 ψ 而言, "x具有 ψ" 可推出如下: 必然地, φ 蕴涵 ψ ]]. 人话版本: φ 是x的本质属性, 定义为: x具有 φ , 并且x的所有属性都必然地是 φ 的后果.

Ax.4. 如果一个性质是积极的，那么它就必然是积极的

我们可以证明Th.3.∀x G(x) → G ess x. 翻译: "类上帝的"属性对于任何拥有这个属性的对象来说都是本质属性. 证明如下：

如果x具有类上帝的的属性, 那么根据Ax.2.和"类上帝的"的定义, x具有所有积极属性并且只具有积极属性. 此时根据Ax.4., x所具有的属性都是必然积极的. 则必然地, "类上帝的"这个属性蕴涵所有积极属性. Th.3.得证.

我们引入最后一条定义和定理：

Df.3. x必然存在，当且仅当x的所有本质属性都必然有例示

Ax.5. "必然存在"是积极性质

现在我们可以证明所要的定理, Th.4.□∃x G(x) . 翻译: 必然地, "类上帝的"性质有实例. 或: 在所有可能世界中都存在一个类上帝的对象. 证明：

根据定义, Th.2.♢∃xG (x). 即为 ♢∃x∀φ(P(φ) → φ(x)). Ax.5. 规定了P(E), 即"必然存在"是积极性质, 所以可能世界中的具有"类上帝的"性质的x也会具有"必然存在"这一积极性质. 也就是说：♢∃xG(x)∧∀φ(φ ess x → □∃yφ(y))，即在某个可能世界中存在一个类上帝的对象, 并且该对象的所有本质属性都必然地(在所有可能世界中)有实例. 注意, Th.3. 告诉我们"类上帝的"这一属性对于具有它的对象来说是本质属性, 也就是说Th.2. 中某可能世界里的类上帝对象的"类上帝的"属性在所有可能世界中都有实例. Th.4. 得证.

到了这一步, 上述证明已经确保了每个可能世界都存在一个类上帝的对象. 接下来我们证明这个对象是唯一的：

我们把结论中的x在某个世界中叫做j, 得出(在那个世界里)G(j) . 此时令 φ(x) 缩写 x＝j . 注意： x＝j 是j的一个性质, 同时因为j是类上帝的, 所以j有且仅有积极性质. 所以任何一个godlike being都会有 φ(x) 这个性质. 唯一性得证. 当然, 这个证明里用到了一些比较宽松的property abstraction principles和比较宽松的transworld identity principles.

下面是一些对这个证明的评价：

值得一提的是, 上面截图中所包含的证明并不是哥德尔手稿原稿中的证明, 而是Dana Scott做出微小修正之后的证明. 修改原因被不少人津津乐道: 哥德尔手稿原稿中的公理和定义是不自洽的(!). Dana Scott所作的修改在于对"本质属性"的定义上. 对比如下：

哥德尔原稿：

φ ess x ⇔ ∀ψ(ψ(x) → □∀y(φ(y) → ψ(y)))

Dana Scott修正：

φ ess x ⇔ φ(x) ∧ ∀ψ(ψ(x) → □∀y(φ(y) → ψ(y)))

可以看出, 两者的区别就在于有没有要求x具有φ . 哥德尔的定义中并没有要求, 所以我们可以得出如下矛盾：令 φ 作Falsum常元 ⊥ (或任意逻辑矛盾的语句，或者是"self-different"这一性质)，则易见 □∀x ⊥ ess x. 由于"必然存在"是积极性质, 所以根据Th.1.可得 ◇∃x E(x) . 根据定义, "必然存在"即所有本质属性都必然地有实例. 综上所述, 我们可以推出：♢∃x (⊥ess x → □∃y⊥(y)) . 此时前文中已证 □∀x ⊥ ess x，所以可得 ♢∃x (□∃y⊥(y)) . 由于两个存在量词都没有bind任何变元, 所以可以消去, 最后证得 ◇□⊥ . 在证明所采用的逻辑S5中, ◇□⊥ → ⊥ .

Dana Scott所增加的约束条件φ(x) 则可以防止这种情况发生. 顺便说一句, 很多做自动化定理证明的人都喜欢拿哥德尔/Scott的证明来测试自己写的码, 例如上述矛盾就曾经被Isabelle(一个自动化证明的program)证出过: ijcai.org/Proceedings/1...

有关自动化定理证明对哥德尔本体论证明的热爱, 见 Holy Logic: Computer Scientists 'Prove' God Exists - SPIEGEL ONLINE - International

"类上帝的"的定义：

oldgoat：G(x) ⇔ ∀φ P(φ) → φ ess x

Dana Scott：G(x) ⇔ ∀φ P(φ) → φ(x)

"本质属性"的定义：

oldgoat：φ ess x ⇔ ∀ψ(□ψ(x) ↔ (φ(x) → ψ(x))).

Dana Scott：φ ess x ⇔ φ(x) ∧ ∀ψ(ψ(x) → □∀y(φ(y) → ψ(y))).

实际上,@oldgoat 老师所采用的公理和定义是C. A. Anderson为了修复J. H. Sobel的一个批评而修改的: appearedtoblogly.files.wordpress.com...

Sobel通过哥德尔/Scott的公理, 证出了一个modal collapse theorem：p → □p . 如果我们将必然算子以S5常见的解读读作"形而上必然"的话, 那么这个modal collapse theorem说的就是"任意事实都是必然的事实", 例如2018年世界杯法国队夺冠, 则modal collapse告诉了我们在所有可能世界的2018年世界杯法国队都夺了冠. 这对许多人来说是反直觉的. modal collapse theorem证明如下：

我们令p为任意在本世界为真的语句, 并且证明□p . 首先通过哥德尔的结论, 我们知道本世界存在一个类上帝的对象, 称其为j. 因为G(j), 所以j具有且仅具有积极性质. 我们注意 [(x＝x)∧p] 是j的性质, 并且"类上帝的"是j的本质属性, 所以根据定义, □∀y(G(y) → (j＝j∧p))) 成立. 由于已证在每个可能世界"类上帝的"都存在实例, 所以在每个可能世界, j＝j∧p 都成立, 即 □(j＝j∧p), 通过模态命题逻辑的推理, 可得 □p.

不难发现, Anderson的改动是加强了"类上帝的"和"本质属性"的约束, 直接防止了下面这步推理的成立：

所以根据定义，□∀y(G(y) → (j＝j∧p))) 成立. 由于已证在每个可能世界"类上帝的"都存在实例, 所以在每个可能世界, j＝j∧p 都成立, 即 □(j＝j∧p) , 通过模态命题逻辑的推理, 可得 □p.

更感兴趣的同学可以读一下Anderson的原文, 里面还评价了不少关于该证明的别的方面.

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。