La prueba ontológica de Gödel es un argumento formal para la existencia de Dios propuesto por el matemático Kurt Gödel (1906-1978).

Continúa una línea de desarrollo que viene desde Anselmo de Canterbury (1033-1109). El argumento ontológico de S. Anselmo, en su forma más resumida, es como sigue: «Dios, por definición, es lo más grande concebido. Dios existe en nuestro entendimiento. Si Dios existe en nuestro entendimiento, lo podríamos imaginar como el más grandioso por existir en la realidad. Por lo tanto, Dios tiene que existir». Una versión más elaborada fue dada por Gottfried Leibniz (1646–1716); esta es la versión que Gödel estudió e intentó aclarar con su argumentación.

La primera versión de la prueba ontológica en los escritos de Gödel es de ca. 1941. No se sabe si Gödel comentó con alguien su trabajo en la demostración hasta 1970, cuando pensó que se estaba muriendo. En febrero, le permitió a Dana Scott copiar una versión de la prueba, la cual circuló en privado. En agosto de 1970, Gödel le dijo a Oskar Morgenstern que estaba «satisfecho» con la prueba, pero Morgenstern anotó en su diario el 29 de agosto de 1970, que Gödel no la publicaría porque temía que otros pudieran pensar «que de hecho cree en Dios, mientras que simplemente está interesado en una investigación en lógica (esto es, en mostrar que tal prueba con las suposiciones clásicas (completitud, etc.) correspondientemente axiomatizada, es posible)».^[1]​ Gödel murió el 14 de enero de 1978. Otra versión, ligeramente diferente de la de Scott fue encontrada entre sus papeles. Finalmente fue publicada, junto con la versión de Scott, en 1987.^[2]​

El diario de Morgenstern es una fuente importante y generalmente fiable para los años más tardíos de Gödel, pero la implicación de la entrada del diario de agosto de 1970 —que Gödel no creía en Dios— no es compatible con otras evidencias. En cartas a su madre, quien no era practicante y había apoyado a Kurt y a su hermano como librepensadores, Gödel argumentó extensamente a favor de la creencia en una vida después de la muerte.^[3]​^[4]​ Él hizo lo mismo en una entrevista con el escéptico Hao Wang, quién dijo: «Expresé mis dudas según G habló [...] Gödel sonrió mientras respondía a mis preguntas, evidentemente convencido de que sus respuestas no me convencerían».^[5]​ Wang comentó que la esposa de Gödel, Adele, dos días después de la muerte de Gödel, le dijo a Wang que «Gödel, a pesar de que no iba a la iglesia, era religioso y leía la Biblia en la cama cada domingo por la mañana».^[6]​ En una carta no enviada como respuesta a un cuestionario, Gödel describió su religión como «bautizado luterano (pero no pertenezco a ninguna congregación religiosa). Mi creencia es teísta, no panteísta, pareciéndose más a Leibniz que a Spinoza».^[7]​

La prueba utiliza lógica modal, que distingue entre verdades necesarias y verdades contingentes. Una verdad es necesaria si es verdadera en todos los mundos posibles. Por contraste, una verdad es contingente si puede o no pasar, por ejemplo , «más de la mitad del planeta está cubierto por agua». Si una declaración es cierta en nuestro mundo, pero falsa en otro mundo, entonces es una verdad contingente . Una declaración que es verdadera en algún mundo (no necesariamente nuestro propio) es llamada verdad posible.

Además, la prueba utiliza lógica modal de alto orden porque la definición de Dios emplea una cuantificación explícita sobre propiedades.^[8]​

Del axioma 1 al axioma 4, Gödel argumentó que en algún mundo existe Dios. Él usó una especie de principio de plenitud modal para argumentar esto a partir de la consistencia lógica de la semejanza con Dios. Notar que esta propiedad es en sí misma positiva, ya que es la conjunción de (infinitamente muchas) propiedades positivas.

Entonces, Gödel definió la esencia: si ${\displaystyle x}$ es un objeto en algún mundo, entonces la propiedad ${\displaystyle \varphi }$ es una esencia de ${\displaystyle x}$ si ${\displaystyle \varphi (x)}$ es cierto en ese mundo y si ${\displaystyle \varphi }$ es más fuerte que todas las propiedades que ${\displaystyle x}$ tiene en ese mundo. También decimos que ${\displaystyle x}$ es necesariamente existente si para cada esencia ${\displaystyle \varphi }$ lo siguiente es cierto: en cualquier mundo posible, existe un elemento ${\displaystyle y}$ con ${\displaystyle \varphi (y)}$.

Dado que la existencia necesaria es positiva, se concluye: ser como Dios es positivo. Además, la semejanza con Dios es una esencia de Dios, porque implica todas las propiedades positivas, y cualquier propiedad no positiva es la negación de alguna propiedad positiva, por lo tanto Dios no puede tener ninguna propiedad no positiva. Como cualquier objeto semejante a Dios es necesariamente existente, entonces cualquier objeto semejante a Dios en un mundo, lo es en cualquier otro mundo, por la definición de existencia necesaria. Dado la existencia de un objeto semejante a Dios en un mundo, probado anteriormente, podemos concluir que existe un objeto semejante a Dios en cualquier otro mundo posible.

A partir de estas hipótesis, también es posible probar que existe solo un Dios en cada mundo por la ley de Leibniz, la identidad de indiscernibles: dos o más objetos son idénticos (es uno y el mismo) si tienen todas sus propiedades en común, y solo habría un objeto en cada mundo que posee la propiedad G. Gödel no intentó hacer esto, solo limitó su prueba al asunto de existencia, más que a la unicidad. Esto fue para preservar más la precisión lógica del argumento que debido a su inclinación por el politeísmo. Esta prueba de unicidad solo puede ser si uno supone que el positivismo de una propiedad es independiente del objeto al cual está referenciado, un argumento que puede ser considerado no cierto ^{[cita requerida]}.

Para formalizar el argumento anterior, las siguiente definiciones y axiomas son necesarios:

• Definición 1: x es como Dios si y solo si x tiene propiedades tan esenciales si y solo si esas propiedades son positivas.
• Definición 2: A es una esencia de x si y solo si para cada propiedad B, x tiene a B necesariamente si y solo si A implica B.
• Definición 3: x necesariamente existe si y solo si cada esencia de x es necesariamente ejemplificada.

• Axioma 1: Cualquier propiedad implicada por (estrictamente implicada por) una propiedad positiva, es positiva.
• Axioma 2: Una propiedad es positiva si y solo si su negación no es positiva.
• Axioma 3: La propiedad de ser como Dios es positiva.
• Axioma 4: Si una propiedad es positiva, entonces es necesariamente positiva.
• Axioma 5: La existencia necesaria es una propiedad positiva.

El axioma 4 supone que es posible determinar propiedades positivas de todas las propiedades. Gödel comenta que «Positivo significa positivo en el sentido estético moral (independientemente de la estructura accidental del mundo)... También puede significar atribución pura opuesta a la privatización (o conteniendo privatizado)». (Gödel 1995). Axiomas 1, 2 y 3 puede ser resumidos al decir que las propiedades positivas forman un filtro maximal.

A partir de estos axiomas y definiciones y otros axiomas de la lógica modal, los siguiente teoremas pueden ser probados:

• Teorema 1: Si una propiedad es positiva, entonces es compatible, i.e., posiblemente ejemplificada.
• Teorema 2: La propiedad de ser como Dios es compatible.
• Teorema 3: Si algo es como Dios, entonces la propiedad de ser como Dios es una esencia de aquella cosa.
• Teorema 4: Necesariamente, la propiedad de ser como Dios está ejemplificada.

Simbólicamente:

${\displaystyle {\begin{array}{rl}{\text{Ax. 1.}}&\left\{P(\varphi )\wedge \Box \;\forall x[\varphi (x)\to \psi (x)]\right\}\to P(\psi )\\{\text{Ax. 2.}}&P(\neg \varphi )\leftrightarrow \neg P(\varphi )\\{\text{Th. 1.}}&P(\varphi )\to \Diamond \;\exists x[\varphi (x)]\\{\text{Df. 1.}}&G(x)\iff \forall \varphi [P(\varphi )\to \varphi (x)]\\{\text{Ax. 3.}}&P(G)\\{\text{Th. 2.}}&\Diamond \;\exists x\;G(x)\\{\text{Df. 2.}}&\varphi {\text{ ess }}x\iff \varphi (x)\wedge \forall \psi \left\{\psi (x)\to \Box \;\forall y[\varphi (y)\to \psi (y)]\right\}\\{\text{Ax. 4.}}&P(\varphi )\to \Box \;P(\varphi )\\{\text{Th. 3.}}&G(x)\to G{\text{ ess }}x\\{\text{Df. 3.}}&E(x)\iff \forall \varphi [\varphi {\text{ ess }}x\to \Box \;\exists y\;\varphi (y)]\\{\text{Ax. 5.}}&P(E)\\{\text{Th. 4.}}&\Box \;\exists x\;G(x)\end{array}}}$

Existe un gran esfuerzo para formalizar la prueba de Gödel a un nivel adecuado para un método automatizado de prueba de teoremas. El método estuvo en los titulares de diarios alemanes. Según los autores de este método, estuvieron inspirados en el libro de Melvin Fitting.^[9]​

La mayoría de la críticas de la prueba Gödel se debe a sus axiomas: como cualquier prueba en cualquier sistema lógico, si los axiomas de la prueba pueden ser cuestionados entonces las conclusiones también pueden ser cuestionados. Esto se puede aplicar a la prueba de Gödel porque los 5 axiomas en que se apoya son todos cuestionables. La prueba no quiere decir que las conclusiones tienen que ser verdaderas, sino que si se aceptan los axiomas entonces las conclusiones son correctas.

Muchos filósofos han cuestionado estos axiomas. Lo primero es que no hay argumentos suficientes que justifiquen porqué estos axiomas son verdaderos. También estos axiomas permiten que se saquen conclusiones no favorables. Esta línea de pensamiento se debe a Sobel,^[10]​ mostrando que si estos axiomas son aceptados, entonces cada declaración que es verdadera es necesariamente verdadera.

La prueba también ha sido cuestionada por Oppy,^[11]​ preguntando que quizás otros casi-dioses pueden ser probados por los axiomas de Gödel. Este contraargumento ha sido cuestionado por Gettings,^[12]​ quien dice que estos axiomas pueden ser cuestionados, pero no está de acuerdo con el contraejemplo de Oppy porque no es seguro que esto se pueda probar con los axiomas de Gödel.

Existen muchas más críticas, la mayoría enfocadas en cuestiones filosóficas acerca de si estos axiomas «deben» ser rechazados para evitar conclusiones raras. La mayor crítica se basa en que si no se puede argumentar que estos axiomas son falsos, esto no significa que tiene que ser verdaderos.

• Lógica modal
• Saul Kripke
• Filosofía analítica
• Gottfried Wilhelm Leibniz
• Teoría de la demostración
• Argumento ontológico
• Teología natural

• John W. Dawson, Jr (1997). Logical Dilemmas: The Life and Work of Kurt Godel. Wellesley, Mass: AK Peters, Ltd. ISBN 1-56881-025-3. 
• Melvin Fitting, "Types, Tableaus, and Godel's God" Publisher: Dordrecht Kluwer Academic, 2002, ISBN 1-4020-0604-7, ISBN 978-1-4020-0604-3
• Kurt Gödel (1995). "Ontological Proof". Collected Works: Unpublished Essays & Lectures, Volume III. pp. 403–404. Oxford University Press. ISBN 0-19-514722-7
• 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)
• Wang, Hao (1987). Reflections on Kurt Gödel. Cambridge, Mass: MIT Press. ISBN 0-262-23127-1. 
• Wang, Hao (1996). A Logical Journey: from Gödel to Philosophy. Cambridge, Mass: MIT Press. ISBN 0-262-23189-1. 
• Small, Christopher. «Reflections on Gödel’s Ontological Argument». University of Waterloo. Archivado desde el original el 22 de diciembre de 2009. Consultado el 14 de diciembre de 2015. 

• Kurt Gödel's Ontological Argument by Christopher Small
• Annotated bibliography of studies on Gödel's Ontological Argument
• Benzmueller & Paleo 2014, "Automating Goedel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers"