# 哥德爾本體論證明

## 證明

$\begin{array}{rl} \mbox{Ax. 0.} & \Box\; \exists \varphi\; P(\varphi)\\ \mbox{Ax. 1.} & \Box\; \forall x \lbrace [\varphi(x) \rightarrow \psi(x)] \land P(\varphi)\rbrace \rightarrow P(\psi)\\ \mbox{Ax. 2.} & P(\neg \varphi) \leftrightarrow \neg P(\varphi)\\ \mbox{Th. 1.} & P(\varphi) \rightarrow \Diamond\; \exists x\; [\varphi(x)]\\ \mbox{Df. 1.} & G(x) \iff \forall \varphi[P(\varphi) \rightarrow \varphi(x)]\\ \mbox{Ax. 3.} & P(G)\\ \mbox{Th. 2.} & \Diamond\; \exists x\; G(x)\\ \mbox{Df. 2.} & \varphi\;\operatorname{ess}\;x \iff \varphi(x) \land \forall\psi\lbrace\psi(x) \rightarrow \Box\; \forall x[\varphi(x) \rightarrow \psi(x)]\rbrace\\ \mbox{Ax. 4.} & P(\varphi) \rightarrow \Box\; P(\varphi)\\ \mbox{Th. 3.} & G(x) \rightarrow G\;\operatorname{ess}\;x\\ \mbox{Df. 3.} & E(x) \iff \forall \varphi[\varphi\;\operatorname{ess}\;x \rightarrow \Box\; \exists x\; \varphi(x)]\\ \mbox{Ax. 5.} & P(E)\\ \mbox{Th. 4.} & \Box\; \exists x\; G(x) \end{array}$

## 模态逻辑

$\Diamond p = \lnot\, \Box\, \lnot\, p$；及
$\Box p = \lnot\, \Diamond\, \lnot\, p$

## 參考文獻

• C. Anthony Anderson, "Some Emendations of Gödel's Ontological Proof", Faith and Philosophy, Vol. 7, No 3, pp. 291–303, July 1990
• Kurt Gödel (1995). "Ontological Proof". Collected Works: Unpublished Essays & Lectures, Volume III. pp. 403–404. Oxford University Press. ISBN 0195147227
• A. P. Hazen, "On Gödel's Ontological Proof", Australasian Journal of Philosophy, Vol. 76, No 3, pp. 361–377, September 1998
• Jordan Howard Sobel, "Gödel's Ontological Proof" in On Being and Saying. Essays for Richard Cartwright, ed. Judith Jarvis Thomson (MIT press, 1987)
• Melvin Fitting, "Types, Tableaus, and Godel's God" Publisher: Dordrecht Kluwer Academic ©2002, ISBN 1402006047 9781402006043