décidabilité

Dans ce topics, \lien{http://www.les-mathematiques.net/phorum/read.php?16,358198,358198#msg-358198}


je vais parler en détails du forcing (laisse-moi juste un peu de tps), sinon, marco t'a plutot bien résumé les idées godelienne.

D'une manière générale, et ce n'est qu'un exercice, tu peux faire toutes les autoréférences** que tu veux, et arbitrer seulement ensuite

**
"je ne suis pas prouvable" (voir marco)
"je suis fausse"
"ma plus courte preuve est plus longue que toute preuve du faux"
etc

Une manière assez "informatique" d'aborder les liens entre ça et un genre de shéma
ensembliste est la suivante:

{\it le "appartient" $\in$ qui suit est juste formel}

Soit $f$ une application

Etant donné $x$, on note $x^+$ "l'ensemble" des $y$ tels que $(x,y)\in x$
Puis on note $a$ l'ensemble des couples $(u,v)$ tels que $v\in f(u^+)$

si $x\in a^+$ alors $(a,x)\in a$ et donc $x\in f(a^+)$ et réciproquement.

Ainsi $a^+$ est un ensemble $b$ tel que $b$ et $f(b)$ contiennent les mêmes éléments.

Donc toute contradiction qui utilise des "points fixes" implique que les "ensembles" précédents ne peuvent exister dans aucune théorie extensionnelle (où contenir les mêmes éléments implique égalité)...

S'agissant de "$f(x):=$ <<$x$ est indémontrable>>", il est presque "trivial" (remarque de Godel) que le procédé "marche"