Bonsoir à tous
Je ne désespère pas de trouver un angle de compréhension mutuelle
Après l'autoreferentialité qui, visiblement, n'a pas convaincu les logiciens du forum (et pourtant...), j'aimerais évoquer la notion d'émulation
On dit d'un système formel A qu'il est capable d'emuler un systeme formel B s'il est capable d'énoncer dans son propre langage un résultat de prouvabilité (ou de refutabilité) qui concerne un énoncé q de B quel que soit q
Cet énoncé est trivial si B est inclu dans A bien sûr
Mais, par exemple, il est possible de prouver le theoreme de Fermat dans le cadre de ZFC alors que Fermat est un énoncé qui s'exprime dans Robinson tout en étant un indecidable de Robinson
Ceci ne constitue cependant pas une preuve de Fermat dans Robinson ..,
Bien...
Un systeme S capable de s'auto emuler doit être capable de formaliser en son sein la proposition autoreferentielle suivante que j'ai déjà evoqué sous une autre forme :
P1- je, P1, ne suis pas prouvable dans S (S consistant)
Si P1 est prouvable dans S, S est incorrect car contradictoire
Si P1 est réfutable, on réussit à refuter une proposition valide donc c'est tout aussi intolérable
Seule l'indecidabilité de P1 dans S est une solution à cet énoncé...
Et veuillez noter que l'indecidabilité a pour conséquence directe que cet énoncé est.... Vrai...
Oui, P1 n'est pas prouvable dans S !
Existerait il des assertions vraies mais non decidables ?
Ce qui vous est apparu comme un joke de ma part n'est qu'une transcription simplifiée de la demonstration de Godel...
Les ressources de Robinson suffisent même pour réaliser cette performance d'insérer la proposition telle que je l'ai rédigée (j'attire l'attention sur le fait que, seul ce cadre m'intéresse pour le sujet dont nous parlons)
Mais, il n'est pas demontré que la condition d'être dans Robinson a minima pour formaliser depuis l'axiomatique et là logique de premier ordre de la theorie considerée un tel énoncé soit nécessaire...
L'histoire de la demonstration de Godel demarre ici puisque il parvient à partir de l'axiomatique de l'arithmétique de Robinson et de sa logique de premier ordre à construire une proposition autoreferentielle G qui s'enonce ainsi : "je ne suis pas prouvable dans le systeme"
Ici, la question n'est pas d'ajouter des axiomes et de construire une nouvelle theorie en axiomatisant P1 car la nouvelle theorie rencontrerait à son tour un nouvel énoncé indecidable...
Ici est l'essence du premier theoreme s'il ne fallait retenir que ça...
Un systeme recursivement axiomatisable consistant integrant Peano est definitivement incomplet
D'autre part, il ne s'agit pas de dogmatiser cet énoncé par un axiome en forçant l'indecidabilité à vrai ou à faux en créant une infinité de theories !
Il s'agit de prouver l'assertion de S en la fixant a vrai ou a faux en demontrant l'assertion indecidable initiale par une demonstration issue d'un autre système
Ça, c'est ce qu'il faut retenir du second theoreme
Fermat dans Robinson est prouvé par une demonstration dans ZFC
Gentzen demontre l'arithmétique de Peano au moyen d'une recurrence transfinie dans le cadre de la theorie des ensembles
Et, globalement, tout ce qu'on fait alors c'est de repousser d'un cran le problème car la consistance de ZFC ne sera jamais demontrée dans ZFC
Voila l'enseignement principal du second theoreme
Amicalement
-----