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.

Une théorie T plus forte que FOT sera qualifiée de FOT-correcte si, dans la classe des énoncés FOT, la T-prouvabilité implique la vérité (dans le modèle standard de FOT).

La diversité des modèles non standard

Au-delà du simple fait d'existence des modèles, les diverses façons de les construire et leurs cas d'utilisation (théories) fourniront une diversité de modèles, y compris des modèles non standard de théories fondatrices, plus ou moins similaires aux modèles standard.

Même avec des propriétés de premier ordre identiques (une condition qu'on peut adopter en prenant comme «axiomes» tous les énoncés vrais d'un modèle donné, bien que ce ne soit pas TT-invariant pour les modèles standard de théories plus fortes que TT), les modèles peuvent différer par des propriétés de niveau méta: cela sera vu pour l'arithmétique en 4.7, et pour toute théorie avec un modèle infini par le théorème de Löwenheim-Skolem.
Mais l'indéfinissabilité de la vérité implique que certains modèles construits diffèrent également par des propriétés du premier ordre à cause de leur invariance. Ceci vaut même pour des théories fondatrices "presque complètes" (pouvant notamment approcher une théorie complète du second ordre par élimination universelle du second ordre).

Toutes les théories fondatrices étant TT-invariantes, ont des modèles aux propriétés FOT-invariantes, donc déjà non standard pour leurs propriétés FOT.
Toute théorie T invariante MT, cohérente et plus forte que MT, a des modèles MT-invariants (et MT-interprétables), donc une classe de propriétés MT non standard (une fois clarifié un concept de "modèle standard de MT" ...). Si de plus T est FOT-correcte, l'ajout de tous les énoncés vrais FOT aux axiomes donne encore une théorie cohérente et invariante MT, donnant des modèles de T avec la classe standard de propriétés FOT mais d'autres propriétés MT non standard (et très probablement un modèle de FOT non standard).

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 (laissant indécidables certains énoncés FOT). 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 ne contenant 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).

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 (notamment 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