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.
- Tout ∃x, A(x) est la condition d’arrêt
d'un algorithme qui énumère tous les x, interprète A sur chacun, et
s'arrête quand il y trouve A vrai;
- La condition d'arrêt de tout algorithme est un énoncé existentiel
∃t, A(t) où A(t) dit qu'il s'arrête au temps t
(les détails sont bien sûr bien plus complexes).
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.
- La vérité d'un énoncés existentiel (∃x, A(x)) implique sa FOT-prouvabilité
(par introduction existentielle
sur la citation de x), donc les deux sont équivalents;
- Tout concept effectif de théorème (classe d'énoncés prouvables s) de toute théorie
dans n'importe quel cadre, doit être une classe existentielle (∃p,
V(p,s)) pour un certain V(p,s), qui signifie que
p est une preuve valide de s.
Les classes existentielles de "théorèmes" habituelles parmi les énoncés du premier ordre de
langage donné, sont formées en 2 étapes:
- 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);
- 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.9, 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 (en particulier, tout modèle
FOT-invariant est TT-interprétable), 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:
- Si T est complète (C(B)∨C(¬B)) alors elle
prouve sa propre incohérence: C(⌜C(⌜0⌝)⌝).
- Si T est FOT-incorrecte, alors C coïncide avec la vérité sur
tous les énoncés existentiels, donc sur tous les C(A). Il existe
donc des C(A) T-indécidables.
Un tel C(A) est faux mais T-irréfutable : A est
T-indémontrable mais cette indémontrabilité est elle-même T-indémontrable.
(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⌝) ⇒ ∀A∈S, ¬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:
- Aucune limite à la taille attendue des plus petites preuves (ou exemple x
tel que B(x) pour certains B bornés) ne peut être systématiquement
exprimée (prédite) juste en fonction de la taille du théorème (ou de la taille de B,
au-delà des plus petites): ces preuves peuvent être trop grandes pour être stockées
dans notre galaxie, ou même indescriptiblement grandes. (Un exemple d'énoncé
censé nécessiter une très grande preuve est donné comme objet du théorème d'accélération de Gödel).
- Les énoncés existentiels indécidables (donc faux) (∃x, A(x))
n'ont que des exemples non standard de x tels que A(x);
mais ceux-ci semblent très similaires au cas vrai, car les objets non standard
sont précisément ceux qui apparaissent "indescriptiblement grands" dans le
modèle non standard qui les contient (en étendant simplement l'ensemble de
ce qu'on entend par "taille descriptible" à toutes les tailles standard).
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).
Other languages:
EN : 1. First
foundations of mathematics : 1.C. Introduction
to incompleteness