1.C. Introduction aux théorèmes d'incomplétude

Classes existentielles

Qualifions une formule d'existentielle si elle s'écrit ∃x, A(x), avec un ∃ ouvert comme racine (ou plusieurs, qui peuvent être ré-exprimés comme un seul) suivi d'une formule bornée A. Dans cette section, cela sera entendu au sens de FOT uniquement. Les énoncés existentiels expriment essentiellement les conditions d'arrêt des algorithmes opérés par des "ordinateurs" abstraits aux ressources illimitées. De même, une classe existentielle d'un FOT, à savoir définie par une formule existentielle ∃y, A(y,x), peut de manière équivalente être qualifiée d'algorithmiquement définie, comme ensemble de toutes les données de sorties fournies en cours de route par un algorithme sans fin; elle définit la vérité sur les énoncés existentiels obtenus en remplaçant x par toute citation.

Prédicats de prouvabilité

Les concepts de provabilité sont liés aux classes existentielles comme suit. Les classes existentielles de "théorèmes" habituelles parmi les énoncés du premier ordre de langage donné, sont formées en 2 étapes:
  1. Donner une théorie du premier ordre avec une classe existentielle d'axiomes (celles habituelles, dont toutes les théories de notre liste, ont même des définitions bornées);
  2. Lui appliquer le concept de preuve de la logique de premier ordre.
La classe de théorèmes qui en résulte est indépendante de la définition formelle choisie pour un concept correct et complet de preuve en logique du premier ordre, en ce sens que deux d'entre elles donnant des formules V, V', exprimant la vérification de preuve dans la même théorie (définie par les symboles τ, L, X), elles donnent les mêmes théorèmes:

FOT (+ symboles τ, L, X avec axiomes) ⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p, V'(p,s))

Comme la première étape définit τ, L, X dans FOT, elle simplifie ce qui précède en FOT ⊢ ...

Inversement, si C est une classe existentielle de "théorèmes" parmi les énoncés du premier ordre d'une théorie, et contient les conséquences logiques du premier ordre de toute conjonction de ses éléments (intuitivement, le cadre de démonstration contient la puissance de la logique du premier ordre), alors C est la classe des énoncés T-prouvables par la logique du premier ordre, pour une théorie du premier ordre algorithmiquement définie T: au moins trivialement, la théorie prenant C comme classe d'axiomes.

Premier théorème d'incomplétude

Soit C une classe d'énoncés FOT "T-prouvables" pour une théorie algorithmiquement définie T capable de les exprimer (C est une classe existentielle d'énoncés FOT contenant les conséquences logiques du premier ordre de toute conjonction de ses éléments). Par indéfinissabilité de la vérité faible, C étant FOT-invariant doit différer de la vérité : C(⌜A⌝) ⇎ A pour certains A.
Si T est FOT-correct (C(⌜A⌝) ⇒ A pour tout A), alors pour chaque A sur lequel C diffère de la vérité, A est T-indémontrable mais vrai, et donc T-indécidable. Ainsi T est incomplet (il existe des énoncés FOT indécidables par T). D'où l'incomplétude de la logique du second ordre (1.11). Cela approche, mais ne donne pas, le célèbre

Premier théorème d'incomplétude. Toute théorie définie par algorithme cohérente et plus forte que FOT est incomplète.

L'écart peut être négligé, car c'est un défaut pire pour une théorie d'être FOT-incorrecte que d'être incomplète. Mais il peut encore être réduit en utilisant notre version raffinée de l'indéfinissabilité faible comme suit.
Supposons T plus fort que FOT (C contient tous les axiomes de FOT, et donc ses théorèmes). Alors pour tout A existentiel, et donc pour A de la forme C(B) pour tout B,

A ⇒ (A est FOT-prouvable) ⇒ C(⌜A⌝)

Si T est cohérent et décide tous les C(A), alors C opère fidèlement les connecteurs sur les instances de C (en déduisant les résultats des valeurs prouvées de C, même si elles sont incorrectes). Donc: (La littérature rapporte des possibilités de prouver les deux théorèmes d'incomplétude par le paradoxe de Berry, mais cela semble très compliqué, au-delà de la portée de cette introduction.)

Second théorème d'incomplétude

Le second théorème d'incomplétude (dont la preuve utilise la version forte de l'indéfinissabilité de la vérité) dit que C(A) est T-iirréfutable pour tous les énoncés A si seulement T est cohérent :

¬C(⌜0⌝) ⇒ ∀AS, ¬C(⌜¬C⌝:A)

où les deux points ( : ) signifient la substitution entre les expressions décrites de sorte que (⌜B⌝:⌜a⌝) = ⌜B(a)⌝. Ceci se résume au cas A=⌜0⌝, à savoir C(⌜¬C(⌜0⌝)⌝) ⇒ C(⌜0⌝) autrement dit la cohérence de T, si elle est vraie, est T-indémontrable.
Reformulant ceci par complétude, si T n'a pas de contradiction standard, alors elle a un modèle contenant une contradiction non standard (et donc pas de modèle vérifiable).

Aussi de manière équivalente, T ne peut prouver l'existence d'aucun prédicat de vérité sur une notion qu'elle décrit comme l'ensemble de ses propres énoncés. Ceci est en quelque sorte expliqué, bien que pas directement impliqué, par la faible indéfinissabilité de la vérité, qui empêche d'utiliser le modèle actuel comme exemple, car la vérité sur tous les énoncés standard ne peut pas y être T-définie comme un prédicat invariant (même pas spéculativement, c'est-à-dire valable uniquement dans certains modèles).

Autres concepts de force

Par la perspective donnée par les théorèmes d'incomplétude, deux autres conceptions (définitions) de l'ordre de force entre les théories fondatrices peuvent être considérées, généralement équivalentes à notre définition de 1.A (les exceptions possibles sont hors de portée ici): Il ne peut y avoir aucune théorie fondatrice ultime bien décrite : pour chacune étant FOT-correcte, ajouter l'énoncé de sa cohérence comme axiome en donne une "meilleure", c'est-à-dire plus forte et toujours FOT-correcte (mais c'est beaucoup moins efficace comme effet renforçant pour la complexité supplémentaire, que d'autres axiomes possibles tels que ceux énumérés en 1.A).

Les justifications pour accepter toute théorie forte (version de la théorie des ensembles) comme fondement valide (correct) des mathématiques doivent rester quelque peu philosophiques car elles ne peuvent pas être complètement formalisées comme preuves.

Le temps des démonstrations

Comme la T-prouvabilité de tout énoncé A ne peut pas être T-réfutée, quelle que soit la quantité de recherche vaine de T-preuves, cela signifie que T continue de "voir une chance" que A soit T-prouvable par des preuves plus longues. Une théorie T' strictement plus forte que T peut réfuter la T-prouvabilité de certains A (comme en trouvant une T-réfutation de A) mais reste indécise pour d'autres (comme A = l'incohérence de T').
Toute théorie fondatrice FOT-correcte (prise comme critère de connaissance) laissera toujours certains énoncés existentiels pratiquement indécidables, qu'ils soient réellement vrais ou faux, la recherche de preuves ou de réfutations semblant vaine dans les limites données de ressources de calcul disponibles: Comme autre aspect du même fait, les prédicats de prouvabilité sont inexprimables par les formules bornées (en raison de l'indéfinissabilité de la vérité, car ils sont équivalents à la vérité dans la classe des énoncés bornés).
Intuitivement, interpréter la vérité sur des énoncés existentiels (ou tout prédicat de T-provabilité), nécessite une vue réaliste : une utilisation de l'infini actuel de ℕ précisément entendu comme son interprétation standard (qui ne peut pas être complètement axiomatisée).

Par une sorte de paradoxe, alors que le théorème de complétude est prouvé en construisant (à l'aide de l'infini actuel) un contre-exemple (modèle) à partir du fait de l'absence de preuve, il n'y a pas de "construction inverse" qui, partant du fait sur l'infini qu'aucun système ne peut exister avec des propriétés données, produirait un témoin fini qui en est la preuve (qui doit néanmoins exister).
Au lieu de cela, l'analyse de cette construction révèle que la taille (complexité) d'une preuve reflète en gros le nombre d'éléments bien choisis qui doivent être décrits dans une tentative de construction d'un contre-exemple, pour découvrir l'échec nécessaire d'une telle construction; la formalisation choisie de la théorie de la démonstration ne peut affecter la taille des preuves que dans des proportions plus modérées (descriptibles).

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
1.1. Introduction au fondement des mathématiques
1.2. Variables, ensembles, fonctions et opérations
1.3. Forme des théories
1.4. Structures mathématiques
1.5. Expressions et structures définissables
1.6. Connecteurs
1.7. Classes en théorie des ensembles
1.8. Symboles liants
1.9. Axiomes et preuves
1.10. Quantificateurs
1.11. Quantificateurs du 2e ordre
Aspects philosophiques
1.A. Temps en théorie des modèles
1.B. Indéfinissabilité de la vérité
1.C. Théorèmes d'incomplétude
1.D. Le cadre ensembliste unifié
2. Théorie des ensembles - 3. Algèbre

Other languages:
EN : 1. First foundations of mathematics : 1.C. Introduction to incompleteness