Preuve de Gödel

@christophe : tes deux axiomes qui ne sont pas des "évidences logiques" (3 et 4 donc) sont fortement criticables et c'est probablement une des raisons pour laquelle cette preuve n'est pas véritablement reconnue (bien sûr, dans la théorie {1,2,3,4}, G est un théorème, mais bon, c'en est aussi un dans {G})

La logique modale(*) (celle dont il est question dans ce fil) consiste à rajouter au calcul propositionnel des adjectifs qualifiant éventuellement les formules. Par exemple ici on a $\Box p$ pour "$p$ est nécessaire" et donc par exemple $q \to \neg \Box p$ se lit "$q$ entraîne que $p$ n'est pas nécessaire"
Il y a une théorie des modèles de la logique modale: https://en.wikipedia.org/wiki/Kripke_semantics. Ca permet de beaucoup démystifier le truc. Noter qu'en se plaçant dans S5 et qu'en interprétant le sulfureux axiome 4: "$\Box(G \to \Box G)$" selon les outils présentés dans le lien ci-dessus, ben il apparaît beaucoup moins naturel que ça avait été promis.

[size=x-small](*) il faudrait dire "les" logiques modales, il y a plusieurs choix d'axiomes différents.[/size]

christophe c:
On se donne $(W,R)$ comme dans wikipédia. $W$ est un ensemble de "mondes" et $R$ une relation binaire sur $W$. A toute variable propositionnelle $V$ on fait correspondre une application $\varphi_V:W \to \{0,1\}$ (on exige $\varphi_{\perp}(x)=0$ pour tout $x\in W$)
et on prolonge récursivement $\varphi$ à toutes les formules en posant (rappel: $\neg A=A \to \perp$ ):
1°$\varphi_{A \to B}(x)=1$ si $\varphi_A(x)=0$ ou $\varphi_B(x)=1$
2° $\varphi_{\Box P}(x)=1$ si: $\forall y \in W, xRy \implies \varphi_{P}(y)=1$ (et $0$ dans le cas contraire).

Un énoncé $E$ est dit "vrai en $x$" si $\varphi_E(x)=1$ (la page wiki note "x $\Vdash P$").
$E$ est dit vrai (tout court) si $\varphi_E$ est constante égale à $1$ (ie si pour tout $x$, $E$ est vrai en $x$).
Si les éléments d'un ensemble d'énoncés sont tous vrais, toutes leurs conséquences prouvables le sont aussi (évident par récurrence sur la taille de la preuve).
On peut vérifier que si $R$ est une relation d'équivalence, tous les axiomes de S5 sont vrais(*).

Venons en aux axiomes 3 et 4 critiqués plus haut. Il s'avère qu'on a:
axiome 3: $\Diamond G= \neg \Box \neg G$ est vrai si et seulement si dans toute classe d'équivalence de $R$, il existe au moins un $x$
tel que $G$ est vrai en $x$. Bon c'est douteux.
axiome 4: $\Box(G \to \Box G)$ vrai si et seulement si $\varphi_G$ est constante sur les classes d'équivalence de $R$.
Ce n'est pas du tout naturel à mes yeux.
En fait si $W$ désigne un ensemble de mondes et $R$ signifie "ressemble", l'axiome 4 dit un truc du genre "dans tous les mondes $x$ ressemblant au mien, si Dieu existe dans $x$, il existe aussi dans tous les mondes ressemblant à $x$".


Et sinon, bien sûr que tout est subjectif (l'interprétation du mot nécessaire ci-dessus est-elle raisonnable).


[size=x-small](*)apparemment il y aurait un théorème de complétude: si pour tout $W$, toute relation d'équivalence $R$ et tout $\varphi$ comme ci-dessus, $\varphi_E$ est constante égale à $1$ alors $E$ est prouvable dans S5[/size]

Pour ceux qui seraient intéressés, Foys parle ici des modèles de Kripke.
Je donne le lien wiki car c'est très intéressant comme théorie : https://fr.wikipedia.org/wiki/Sémantique_de_Kripke

D'une certaine façon c'est ce qui remplace les tables de vérité pour la logique modale.

Christophe : certes c'est très philosophique, et pas mathématique, mais je ne suis pas d'accord avec ta deuxième certitude, avec la parenthèse en particulier.

3) A la Socrato-Desproges : ma seule certitude est que je ne suis sûr de rien.

S

PS : les 2 dîtes certitudes énoncés par CC ont pour hypothèse implicite :
"ce qui est certain pour moi est certain pour les autres"

Comme l'a déjà fait remarquer, Alannaria.

christophe que penses tu la demonstration de l'existence de Dieu de Spinoza?

Au contraire les axiomes sont parfaitement spécifiés dès le début.
Le problème c'est que ce sont des axiomes très forts et très contestables par beaucoup de gens.

Je te donne si tu veux ici les axiomes pour la partie concernant la démonstration de Dieu.
(Ca reste de la philosophie par contre :-D mais je vais essayer de faire des traductions mathématiques même si ce n'est pas ultra pertinent)

A1 : Tout ce qui est, est ou bien en soi ou bien en toute autre chose. (Traduction mathématique si tu veux $\forall x ( x \in x \,\text{ou}\, \forall y (x \in y))$, déjà là tu vois qu'on est dans un axiome assez spécial :-D)

A2 : Tout ce qui ne peut être conçu par autre chose doit être conçu par soi. (Traduction mathématique$ \forall x (\text{non}(\exists y : y \to x))\to (x\to x))$, ça par contre c'est une trivialité pour nous, donc axiome acceptable.)

A3 : D'une cause donnée et déterminée suit nécessairement un effet, mais si par contre aucune cause déterminée n'est donnée, il est impossible qu'un effet en suive. (Principe de causalité)

A4 : La connaissance de l'effet dépend de la connaissance de la cause et l'enveloppe.

A5 : Les choses qui n'ont entre elles rien de commun ne peuvent pas, non plus, être réciproquement comprises l'une par l'autre, c'est à dire le concept de l'une n'enveloppe pas le concept de l'autre. (Si on traduit "x est compris par y" par $x \subset y$, c'est trivial)

A6 : L'idée vraie doit s'accorder avec ce dont elle l'idée. (Vraiment flou et contestable)

A7 : De tout ce qui peut être conçu comme non existant, l'essence n'enveloppe pas l'existence.

Oui mais après ça commence à devenir dur (ça reste de la philosophie)
On peut éventuellement en traduire d'autres, par exemple en rajouter un symbole unaire traduisant la connaissance. (Une logique modale où carré x veut dire "je sais x".

Mais bon, bon courage pour traduire 6. :-D

Edit : Ce problème (traduire Spinoza) commence vraiment à me plaire je dois y réfléchir.
Notamment pour l'instant j'ai traduit "y conçoit x" par $y \to x$. Mais pour Spinoza ce n'est PAS pareil que "y est la cause de x", il faut donc 2 symboles différents. Il doit y avoir moyen de tout encoder dans un langage ensembliste avec un ajout d'un opérateur modal. L'axiome 6 reste par contre complètement opaque. Il faudrait que je relise les définitions et les commentaires pour le retraduire.
Je créerai un fil complet quand j'aurai fait tout ça. :-D
Merci pour ce chouette exercice de vacances.

Bon j'ai regardé plus en détail et tout ça semble atrocement compliqué, il y a tellement de concepts à mettre (de nouveaux symboles) et si peu d'axiomes qu'à mon avis il y a une dizaine d'axiomes "de bon sens" sous-entendus.

Déjà il part d'une théorie à deux types. Certaines variables sont des corps et d'autres des esprit.

Les deux concepts de base sont l'essence et l'existence. Mais l'existence ne doit pas être régie par $\exists$ puisque ce symbole doit se mettre devant une formule atomique or lui il veut pouvoir dire "x existe" et non pas "il existe x tq". (Enfin il veut les deux) Il faut donc introduire un premier symbole unaire $\square x$ qui veut dire "x existe".

Ensuite pour l'essence on a $x \in y$ qui voudra dire "x est dans l'essence d'y". Mais attention on a PAS $x = \{y : y \in x\}$ (Oublions ZF ici, il faut voir cette appartenance comme un nouveau symbole).

On peut maintenant définir la notion de cause (pour l'instant tout ça marche pour les deux types donc je ne précise pas). On dira que $y$ est la cause de $x$ si $$\forall t (t\in y \to \square x).$$ Autrement dit chaque élément de l'essence de $y$ doit impliquer l'existence de $x$. Il est commode de noter $y$ est cause de $x$ par $x \leq y$. Cette relation ne vérifie aucun des axiomes de relation d'ordre (même pas l'anti-symétrie) mais c'est pratique de considérer qu'une cause englobe (est plus grande) que sa conséquence. On a l'axiome $$\forall y (\square y \to \exists x (x \leq y))$$ A savoir "toute chose a une conséquence (au moins une) à condition que cette chose existe".

Maintenant il faut introduire des symboles propres aux types. Un symbole fonctionnel $c$ binaire qui veut dire "machin conceptualise truc". Ainsi $c(x,y)$ veut dire que $x$ est une conceptualisation de $y$. Au niveau type $x$ doit être du type "esprit" (ou "idée" si on préfère) et $y$ de type corps. Il faut imaginer le premier type comme étant notre monde intellectuel et le second type comme les phénomènes physiques. Enfin il faut un opérateur de connaissance, mais je pense qu'on peut le définir avec le reste en réfléchissant bien.

En particulier on a l'axiome $$\forall x \forall y ((x \leq y) \to (\exists t (c(t,y))\to \exists u (c(u,x))))$$ qui veut dire que si on sait conceptualiser la cause alors on sait conceptualiser toute conséquence de cette cause. (Logique puisqu'une cause "englobe" sa conséquence pour spinoza)

La suite au prochain épisode mais tout ça me semble sans grand intérêt, ça reste de la philosophie après tout. Dans le meilleur des cas cela peut donner naissance à des idées mathématiques mais qui n'auront plus rien à voir avec ce que faisait Spinoza. ;-)

Non pour moi ça a du sens. En maths on a toujours un "tel que" sous-entendu. On ne peut pas juste dire "x existe" autrement dit, on ne peut pas écrire $\exists x : x$. (Il faut une formule atomique après et pas juste une variable) Il y aurait un truc pour contourner ça ?

Ca, ça va énormément changer les choses. Certaines propriétés fausses pour Spinoza deviennent vraie si je prends cette définition.

Surtout que quand il dit "x existe" il n'y voit pas de quantification. Il utilise cette expression, d'une certaine façon, comme un synonyme de "x est nécessaire". Et c'est typiquement pour ce genre de chose qu'on utilise la logique modale. Voilà pourquoi j'ai pris un symbole $\square$.