Posted by on April 04, 2001 at 05:11:24 PM EDT:
In Reply to: Bavard macaronique : tu essayes de noyer le poisson. posted by on April 04, 2001 at 04:40:33 PM EDT:
La seconde partie est la traduction du mémoire de Gödel qui comporte lui même quatre parties :
1. Une présentation non formelle de "l'idée directrice de la démonstration ; sans prétendre encore bien entendu à l'exactitude" par Gödel qui fait référence à une analogie avec les paradoxes "de Richard" et "du menteur".
2. Le coeur de la démonstration qui consiste en
a) une exposition brève du système formel noté P (celui Principia Mathematica de Russell-Whitehead), que Gödel va étudier d'un point de vue extérieur (métamathématique),
b) "L'assignation de nombres naturels aux signes primitifs du système P" assignation qu'on dénomme depuis "codage de Gödel",
c)une "disgression" sur les fonctions et les relations récursives,
d)la construction explicite de quarante cinq relations (récursives au sens c)) traduisant pas à pas des prédicats métamathématiques du genre : "la suite de formules codée par l'entier x est une preuve de la formule codée par y" et permettant, à l'aide du théorème V la projection de ces notions intuitives dans le système formel P,
e) l'atteinte du "but final" (le théorème VI) où Gödel exhibe la fameuse formule exprimable dans le système formel P tel que ni cette formule, ni la négation de celle-ci ne soit prouvable dans le système K où K est le système P auquel on peut adjoindre n'importe quel ensemble de formule pourvu que celui-ci soit récursif et bien sûr consistant. Une telle formule est appelée indécidable par Gödel (à la suite de Hilbert).
3. Dans cette partie plus technique (mais importante pour les logiciens dans l'histoire du fondement des mathématiques) Gödel définit la notion de "relation arithmétique" et montre, via le théorème VI précédent, qu'il existe également des propositions arithmétiques indécidables.
4. Gödel montre que la formule qui affirme qu'un système formel K supposé intuitivement consistant est exprimable dans K mais n'est pas démontrable dans K.