La preuve gödélienne est une démonstration mathématique formelle de l'existence de Dieu développée par Kurt Gödel entre 1941 et 1970, employant la logique modale et la théorie axiomatique des ensembles. L'argument affirme que si nous acceptons certains axiomes concernant les propriétés positives—qu'elles forment un ultrafiltre fermé sous l'implication et la nécessité—alors nous pouvons formellement dériver qu'il existe un être possédant nécessairement toutes les propriétés positives. Gödel définit Dieu comme l'être ayant toutes les propriétés positives, prouve qu'un tel être est possible, puis démontre par la logique modale que si l'existence de Dieu est possible, elle est nécessaire. La structure inférentielle de la preuve procède des axiomes sur le comportement logique des propriétés positives à travers des théorèmes intermédiaires sur l'essence et l'existence nécessaire pour conclure qu'il existe nécessairement exactement un être avec toutes les propriétés positives.
Gödel a d'abord esquissé la preuve dans des carnets de 1941, la raffinant dans les années 1940, bien qu'il ne l'ait jamais publiée de son vivant, craignant qu'elle soit mal comprise comme une confession religieuse personnelle plutôt qu'un exercice logique. La preuve a été rendue publique pour la première fois par les notes du séminaire de Dana Scott de 1970 et les conversations de Gödel avec Oskar Morgenstern enregistrées dans le journal de ce dernier. Les principaux exposants incluent C. Anthony Anderson dans « Some Emendations of Gödel's Ontological Proof » (1990), Jordan Howard Sobel dans « Logic and Theism » (2004), et Alexander Pruss dans « A Gödelian Ontological Argument Improved » (2009). Les travaux récents de Christoph Benzmüller et Bruno Woltzenlogel Paleo ont vérifié la validité formelle de la preuve en utilisant des démonstrateurs automatiques de théorèmes, confirmant dans « Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers » (2014) que la dérivation est logiquement valide étant donné les axiomes.
Les objections les plus fortes visent les axiomes plutôt que la dérivation formelle. Sobel a démontré dans « Gödel's Ontological Proof » (1987) que les axiomes de Gödel entraînent un effondrement modal—chaque proposition vraie devient nécessairement vraie—ce que la plupart des philosophes trouvent inacceptable. Les critiques contestent également la cohérence de « propriété positive », arguant qu'elle reste indéfinie au-delà de son comportement formel, et questionnent si l'existence devrait compter comme positive. Anderson répond en affaiblissant les axiomes pour éviter l'effondrement modal tout en préservant la conclusion de la preuve. Pruss défend une notion de propriétés positives comme perfections pures dépourvues de limitations intrinsèques. Robert Maydole dans « The Ontological Argument » (2012) soutient que l'objection de l'effondrement modal présuppose inutilement la logique modale S5. La vérification formelle de Benzmüller et Paleo contourne les questions interprétatives, montrant que quelles que soient les propriétés positives, si elles se comportent selon les axiomes de Gödel, la conclusion suit nécessairement.
Contrairement à l'argument conceptuel d'Anselme à partir de l'idée de « ce dont rien de plus grand ne peut être conçu », la preuve de Gödel opère par pure logique formelle sans analyse phénoménologique. Là où Descartes argumente à partir de la perception claire et distincte de l'essence de Dieu et où Leibniz se concentre sur la preuve de la possibilité d'un être parfait par la compossibilité des perfections, Gödel axiomatise directement la notion de propriétés positives. L'approche gödélienne diffère de la formulation en mondes possibles de Plantinga en travaillant dans la logique modale d'ordre supérieur plutôt que dans la sémantique des mondes possibles du premier ordre, et contrairement à l'argument modal de Hartshorne, ne fait aucun appel aux intuitions sur l'adoration ou l'adéquation religieuse.