# Preuve ontologique de Gödel

La preuve ontologique de Gödel est un argument ontologique sous la forme d'un argument formel de logique modale du mathématicien Kurt Gödel (1906-1978) en faveur de l'existence de Dieu. L'idée de l'argumentation ontologique pour démontrer logiquement la nécessité de l'existence de Dieu et sa cohérence remonte à Anselme de Cantorbéry (1033-1109) ; aujourd'hui elle est reprise, reformulée, discutée et critiquée par plusieurs philosophes et logiciens contemporains.

## Démonstration

La preuve s'appuie sur les définitions et axiomes suivants :
* Définition 1 : x est divin (propriété que l'on note G(x)) si et seulement si x contient toutes les propriétés qui sont positives.
* Définition 2 : A est une essence de x si et seulement si pour chaque propriété B, si x contient B alors A implique B.
* Définition 3 : x existe nécessairement si et seulement si chaque essence de x est nécessairement exemplifiée.
* Axiome 1 : Toute propriété nécessairement strictement impliquée par une propriété positive est positive.
* Axiome 2 : Une propriété est positive si et seulement si sa négation n'est pas positive.
* Axiome 3 : La propriété d'être divin est positive.
* Axiome 4 : Si une propriété est positive, alors elle est nécessairement positive.
* Axiome 5 : L'existence nécessaire est positive.
De ceux-ci et des axiomes de la logique modale, on déduit, dans l'ordre :
* Théorème 1 : Si une propriété est positive, alors elle est possiblement exemplifiée.
* Théorème 2 : La propriété d'être divin est possiblement exemplifiée.
* Théorème 3 : Si x est divin, alors la propriété d'être divin est une essence de x.
* Théorème 4 : La propriété d'être divin est nécessairement exemplifiée.
Pour faciliter la compréhension, on rappellera que :
* "Une propriété A implique une propriété B" signifie qu'il est nécessaire que tout élément qui contient A contienne également B.
* "Une propriété est exemplifiée" signifie qu'il existe un élément qui contient cette propriété.

### Écriture symbolique

${\begin{array}{rl}{\mbox{Ax. 1.}}&P(\varphi )\land \Box \;\forall x[\varphi (x)\rightarrow \psi (x)]\rightarrow P(\psi )\\{\mbox{Ax. 2.}}&P(\neg \varphi )\iff \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 y[\varphi (y)\rightarrow \psi (y)]\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 y\;\varphi (y)]\\{\mbox{Ax. 5.}}&P(E)\\{\mbox{Th. 4.}}&\Box \;\exists x\;G(x)\end{array}}$
Où :
* $\Diamond \;A$ signifie « A est possible »
* $\Box \;A$ signifie « A est nécessaire ».
* $P(\varphi )$ signifie « $\varphi$ est positive ».
* $E(x)$ signifie « x existe nécessairement ».
* $G(x)$ signifie « x est divin ».
* $\varphi \;\operatorname {ess} \;x$ signifie « $\varphi$ est une essence de x ».

## Historique

Kurt Gödel n'a jamais publié ce travail, qu'il a commencé en 1941 et perfectionné en 1954 et 1970. Piergiorgio Odifreddi estime que Gödel n'a pas voulu donner l'impression qu'il s'intéressait à la théologie, alors qu'il ne se souciait que de la partie logique de la réflexion. Il a, à plusieurs reprises, présenté cette preuve à des amis vers 1970 mais elle n'a été publiée qu'en 1987, neuf ans après sa mort.
L'axiome 3 disait à l'origine qu'une conjonction de propriétés positives est également une propriété positive. Mais des propriétés positives pourraient être incompatibles entre elles : leur conjonction serait une propriété impossible et G(x) serait faux pour chaque x (c'est-à-dire que la propriété d'être divin ne serait pas exemplifiée).

## Critiques
### Critique du raisonnement

La démonstration elle-même, c'est-à-dire le fait que la conclusion découle logiquement des axiomes et définitions choisis, est maintenant pratiquement irréfutable étant donné qu'elle a été vérifiée par ordinateur.

### Notion de positivité

Un point important à noter est qu'aucune définition de la notion de positivité n'est fournie avec la preuve. Tout au plus, les différents axiomes qui s'y rapportent peuvent être considérés comme fournissant une définition implicite partielle.
Leibniz, dont Gödel s'est inspiré, utilise cet adjectif pour les qualités qui rendent quelque chose « meilleur » que ce qu'il est sans elles.