C'est un théorème bien connu, et que j'ai expliqué il y a quelques
années dans cette longue entrée,
que ZFC (:= le système d'axiomes standard de la théorie
des ensembles), s'il est consistant, ne peut pas démontrer
que ZFC est consistant. C'est là le « second » théorème
d'incomplétude de Gödel dans le cas particulier de ZFC.
De même, PA (:= l'arithmétique de Peano du premier ordre)
ne peut pas démontrer que PA est consistant. (Dans les
deux cas, l'affirmation que le système est consistant
signifie
qu'il n'existe pas de suite finie de symboles partant des axiomes et
suivant les règles de la logique pour arriver à la conclusion
absurde 0=1 : et on a le droit de parler de suites finies de
symboles
parce qu'elles peuvent se remplacer par des entiers grâce
à ce qu'on appelle le codage de Gödel. Je ne rentre pas dans les
détails puisque j'ai déjà expliqué ça et qu'il y a déjà quantité de
bonne vulgarisation sur le sujet.)
Du coup, on peut être tenté d'ajouter
à ZFC un nouvel axiome Consis(ZFC), qui
affirme ZFC est consistant
, formant un nouveau
système ZFC₁ ; puis, comme le théorème de Gödel
s'applique aussi à lui, on peut encore ajouter un nouvel axiome
Consis(ZFC₁) qui affirme que celui-là est consistant,
formant un nouveau système ZFC₂ ; « et ainsi de suite ».
(En réalité, il y a beaucoup de subtilités ici dans le ainsi de
suite
, et de toute façon ce n'est pas une bonne façon
d'enrichir ZFC, ces axiomes étant à la fois beaucoup
moins forts, moins maniables et moins intéressants, que les axiomes de
grands cardinaux par lesquels on l'étend usuellement. S'agissant
de PA, on peut aussi faire cette construction, en gardant
à l'esprit que PA, PA₁, PA₂,
etc., et leurs consistance, sont de toute façon des conséquences
(théorèmes) de ZFC.)
Ce point est bien connu, donc, et peut-être même trop connu, à tel point qu'on fait dire à ce théorème de Gödel un peu n'importe quoi. Les deux faits suivants, en revanche, sont bien moins connus, et mériteraient pourtant de l'être autant, parce qu'ils invitent à reconsidérer la manière dont on interprète (au moins sur le plan intuitif ou philosophique) ce théorème d'incomplétude. J'ai mentionné ces faits en passant lors de l'entrée passée vers laquelle je viens de faire un lien, mais je pense que je n'ai pas assez attiré l'attention dessus, ce qui est dommage.
(Les deux points suivants sont indépendants l'un de l'autre.)
✱ Le premier fait, c'est qu'on peut tout à fait fabriquer une
théorie ZFC† dont les axiomes sont ceux
de ZFC plus un axiome supplémentaire qui
dit ZFC† est consistant
. Oui, c'est circulaire
(la théorie affirme sa propre consistance), mais ce n'est pas très
difficile d'arriver à formaliser ça en utilisant
les astuces de points
fixes habituelles. Et de même, on peut former PA†
dont les axiomes sont ceux de PA (Peano) plus un axiome
supplémentaire qui dit que PA† est consistant
. Il
s'agit d'une façon assez naturelle d'essayer de contourner le théorème
d'incomplétude (au moins quand on a mal compris celui-ci), en se
disant puisque je ne peux pas démontrer que mon système formel est
consistant, je vais l'ajouter comme axiome
(et affirmer
directement que l'ensemble est consistant plutôt qu'ajouter un axiome
qui dit que la théorie de départ est consistante, puis un autre qui
dit que cette nouvelle théorie est encore consistante, et encore un
autre qui dit que celle-ci est consistante « et ainsi de suite »).
Bref, on peut fabriquer cette théorie ZFC† ou PA†, mais le problème c'est elle est inconsistante (elle démontre 0=1). Parce que le théorème de Gödel s'applique à elle aussi, et comme il affirme que si la théorie est consistante elle ne peut pas démontrer sa consistance, et qu'elle démontre effectivement sa consistance (puisque c'est un axiome, et qu'un axiome compte bien comme une démonstration), du coup, elle n'est pas consistante.
Alors voilà, ce n'est pas bien passionnant, certes : j'ai construit
une théorie et j'ai expliqué qu'elle ne marchait pas — mais je pense
que c'est quand même instructif, au moins sur le plan de l'intuition.
Quand on présente le théorème d'incomplétude de Gödel, que ce soit au
grand public, à des mathématiciens non-spécialistes, ou à des
débutants en logique, l'idée qui en résulte typiquement — et je ne
prétends pas qu'elle soit fausse — est qu'un système formel
consistant T (récursivement axiomatisable, et
contenant un fragment suffisant de l'arithmétique) n'est
jamais assez « puissant » pour démontrer sa propre consistance, mais
que (a) il s'agit d'une notion un peu constructive de démonstration,
et (b) la raison pour laquelle on est conduit à ajouter des axiomes
qui disent T est consistant
et cette théorie-là
est consistance
et cette théorie-là est
consistante
, « et ainsi de suite », est qu'on ne peut jamais tout
faire d'un coup. Or l'exemple de la construction que je viens de
donner montre qu'il faut se méfier de cette intuition : (b) on peut
tout à fait écrire une théorie qui affirme sa propre
consistance, et (a) cette théorie est forcément inconsistante parce
que le théorème de Gödel interdit à une théorie
consistante (récursivement axiomatisable, et contenant un
fragment suffisant de l'arithmétique) non
seulement démontre sa propre consistance, mais même
simplement qu'il l'affirme (un axiome compte bien comme
une démonstration). Je vais citer la présentation de Torkel
Franzén (Inexhaustibility, 2004, chap. 12)
parce que je trouve qu'il est particulièrement clair :
It is often emphasized that the resources of a theory T
do not themselves suffice to enable a proof of the consistency
of T. Again it is only by “going outside the system” than
one can prove that T is consistent.
A weakness of this emphasis is that it doesn't take into account
that the relevant concept of proof
is a very liberal one. The
consistency of T is provable in the
theory T+Consis(T). This is not because any new
fundamental principle has been introduced or because the
theory T+Consis(T) incorporates any new insight
that goes beyond those expressed in T, but simply because
the consistency of T has been postulated. We
don't require any more of a proof, as the term is used in logic.
Accordingly, the second incompleteness theorem makes a stronger
statement than one might naturally suppose. The consistency
of T not only cannot be derived from the basic principles
embodied in T, it cannot even be consistently asserted
in T. A theory cannot consistently postulate its
own consistency. By the diagonal lemma, we can produce a
formula φ formalizing This sentence is consistent
with T
, but since T+φ then proves
its own consistency, we know that in fact it is inconsistent.
Why is it impossible for T to consistently postulate
Consis(T)? Because a paradox results from such a
postulate, or so Gödel's proof of the second theorem suggests.
If T asserts its own consistency, it must both assert and
deny the provability of the sentence formalizing This sentence is
not provable in T
. It's not just a matter
of T lacking the resources to establish a particular truth
(that T is consistent) but of it being impossible to
consistently sneak in this truth as an assertion or postulate in the
theory itself. Saying that one must go outside the system
to
prove the consistency of T conveys the suggestion
that T metaphorically speaking has a kind of “blind spot”,
that it cannot reflect on or understand or inspect itself sufficiently
to establish its own consistency—and indeed in extrapolations from the
incompleteness theorem to other fields (religion, physics, psychology)
this suggestion is frequently made explicit. The fact
that T cannot even consistently assert its own consistency,
without attempting any inspection or justification whatever, would
seem to indicate that this suggestion is a bit of a red herring.
Je trouve que cela illustre très bien la manière dont on a tendance à mal se représenter le théorème d'incomplétude comme traduisant un problème profond de « manque de force » — alors qu'il s'agit de quelque chose d'à la fois plus trivial et plus profond. (Bien sûr, tout ceci est juste une question d'interprétation intuitive : il n'y a aucune difficulté ou subtilité mathématique dans tout ce que j'ai écrit.)
Mais si ce point est un peu trivial et en quelque sorte négatif, le suivant est beaucoup plus intéressant mathématiquement, et il est plutôt positif. Par ailleurs, il concerne spécifiquement ZFC et PA (pas que ce soient les seules théories auxquelles il s'applique, mais il ne s'applique pas à « à peu près n'importe quoi » comme le point que je viens de faire).
✱ J'en viens donc au second fait que je voulais signaler. Il faut d'abord que je rappelle que ZFC et PA ont un nombre infini d'axiomes : ils comportent en effet des schémas d'axiomes (le principe de récurrence dans le cas de PA, et pour ce qui est de ZFC, les schémas de séparation (=compréhension, =sélection) et ceux de remplacement). Ces axiomes veulent affirmer certains faits pour toute propriété P (des entiers naturels dans le cas de PA, ou des ensembles dans le cas de ZFC) : comme la logique du premier ordre ne permet pas de quantifier sur les propriétés, on s'en tire en postulant tous les énoncés dans lesquels P est remplacé par n'importe quelle formule explicitement écrite dans le langage où on se place — ce qui fait donc une infinité d'axiomes.
(Digression : Il y a d'autres façons de faire, consistant plus ou moins à faire de la logique du second ordre, et qui permettent de ramener cette infinité d'axiomes à un nombre fini au prix d'une complication de la logique, et parfois un renforcement du système : ce sont par exemple la théorie des ensembles de Gödel-Bernays, essentiellement aussi forte que ZFC, ou celle, strictement plus forte, de Morse-Kelley, les deux permettant de parler de classes, ce qui revient à permettre de quantifier sur les propriétés, et, s'agissant de l'arithmétique, le système ACA₀ qui est exactement parallèle de Gödel-Bernays et l'arithmétique du second ordre Z₂=PA² qui est exactement parallèle de Morse-Kelley. Mais je vais m'abstenir de plus parler de toutes ces théories, d'autant que ça devient vite technique quand il s'agit de distinguer la vraie logique du second ordre de la logique du second ordre « réifiée » au premier ordre au sens où on a une logique du premier ordre à deux types d'objets qui fait semblant d'être une logique du second ordre en décrétant que l'un de ces types est le type des « classes » ou « propriétés » de l'autre type, ce qui revient finalement au même sauf que la notion de modèle et toute la sémantique qui va avec est différente.)
Un point qui me semble très important, et qui est rarement suffisamment souligné dans les cours élémentaires de logique, est le suivant :
Chacun de ZFC et de PA prouve la consistance de tous ses sous-ensembles finis d'axiomes.
Autrement dit, ZFC ne prouve pas la consistance de ZFC (c'est ce par quoi j'ai commencé : le second théorème d'incomplétude), mais ZFC prouve la consistance de n'importe quel ensemble fini d'axiomes de ZFC. Et la même chose vaut pour PA. On dit que ce sont des théories réflexives. En fait, il y a mieux : n'importe quelle extension de l'une ou l'autre de ces théories, écrite dans le même langage, est elle-même réflexive (on dit que ZFC et PA sont essentiellement réflexives : dans le cas de PA, c'est un théorème de 1952 dû à Andrzej Mostowski, et dans le cas de ZFC, je crois que le résultat est dû à Richard Montague et/ou Azriel Lévy vers 1960).
Une des conséquences de ce théorème est que ni ZFC ni PA, s'ils sont consistants, ne peut pas être axiomatisé par un nombre fini d'axiomes (si un ensemble fini T₀ de théorèmes de ZFC, ou du coup, d'axiomes de ZFC, suffisait à impliquer tous les axiomes de ZFC, alors ZFC prouverait la consistance de T₀, donc T₀ prouverait la consistance de T₀, et en prenant T₀ assez fort pour faire de l'arithmétique basique — je ne rentre pas dans les détails — ceci contredit le théorème de Gödel appliqué à la théorie T₀ ; et exactement le même raisonnement vaut pour PA). Mieux : comme ZFC et PA sont essentiellement réflexifs, aucune théorie consistante contenant ZFC ou PA et écrite dans le même langage ne peut être axiomatisée par un nombre fini d'axiomes. Mais ce n'est pas vraiment de ça que je veux parler.
Le résultat ci-dessus doit surprendre, parce qu'il paraît contredire le théorème de Gödel. L'argument serait le suivant : s'il y avait une contradiction dans ZFC, la démonstration de cette contradiction n'utiliserait qu'un nombre fini d'axiomes de ZFC (si on veut, c'est le théorème de compacité syntaxique, mais c'est une trivialité : une démonstration, étant de longueur finie, ne peut faire appel qu'à un nombre fini d'axiomes !) ; mais d'après ce que j'ai dit, ZFC prouve que ceci ne peut pas se produire (tout ensemble fini d'axiomes de ZFC est consistant) — du coup, ZFC est consistant, et on semble avoir prouvé ce fait dans ZFC ! Quelle est l'arnaque ?
L'arnaque est que le théorème de réflexivité ci-dessus est un
métathéorème ; plus exactement, donné un ensemble T₀
quelconque d'axiomes de ZFC, on a une recette tout à fait
explicite qui fabrique une démonstration à partir des axiomes
de ZFC dont la conclusion est T₀ est
consistant
, et c'est un théorème
(de ZFC, PA ou de systèmes encore plus
faibles) que cette recette marche, i.e., l'énoncé encadré ci-dessus
est bien un théorème. Mais, s'il est vrai que pour
tout T₀ fini ⊆ZFC, T₀ est
consistant
est un théorème de ZFC, et
que ceci est aussi un théorème de ZFC
ou PA (i.e., pour tout T₀ fini
⊆ZFC,
), en revanche, l'affirmation T₀ est consistant
est un théorème
de ZFCpour
tout T₀ fini ⊆ZFC, T₀ est
consistant
, elle, n'est pas un théorème de ZFC (si ce
dernier est consistant), car elle implique la consistance
de ZFC d'après le raisonnement que j'ai fait au
paragraphe ci-dessus.
Je répète : pour tout ensemble fini T₀ d'axiomes de ZFC, on sait fabriquer une démonstration dans ZFC que cet ensemble T₀ est consistant, et on sait montrer dans ZFC (ou PA ou moins) que ce procédé marche bien, mais on ne peut pas en conclure dans ZFC que tout ensemble fini T₀ d'axiomes de ZFC est consistant. On peut résumer cette situation ainsi : il est vrai que pour tout ensemble fini T₀ d'axiomes de ZFC, ZFC démontre la consistance de T₀, mais il ne le fait pas uniformément en T₀. C'est un cas du phénomène appelé la ω-incomplétude : pour tout n on démontre P(n) selon une recette générale et explicite, mais on ne peut pas démontrer ∀n.P(n) (ici, s'imaginer que n est un codage de T₀ et P(n) est l'affirmation que ce T₀ est consistant).
Absolument tout ceci vaut en remplaçant ZFC par PA partout (i.e., pour tout sous-système fini T₀ de PA, PA démontre que T₀ est consistant, mais ne le fait pas de façon uniforme). Ce fait est, d'ailleurs, étonnamment difficile à trouver écrit dans des bouquins de logique arithmétique.
Pour autant, pour tout usage philosophique ou épistémologique, je
suis tenté de dire que ce qui précède (je veux dire, le résultat
encadré ci-dessus) est exactement aussi bien qu'une démonstration de
la consistance de ZFC dans ZFC,
resp. de PA dans PA. Je ne sais pas au
juste ce qu'on espérerait accomplir à avoir une démonstration de la
consistance de ZFC dans ZFC ou de celle
de PA dans PA (le projet de Hilbert était
plutôt d'avoir une démonstration de la consistance d'un système fort
dans un système faible, donc disons quelque chose comme celle
de ZFC dans PA, or ça c'est vraiment hors de
question). Mais je suppose que l'idée serait quelque chose
comme je suis prêt à admettre comme mathématiquement vrais et
certains les résultats — au moins arithmétiques — dont j'ai une
démonstration dans ZFC, et je me sentirais plus rassuré
si j'étais certain qu'il n'y a pas de démonstration de résultats
absurdes dans ZFC
, ce qui n'est pas si idiot que ça
même si c'est circulaire (admettre que ZFC
est vrai — ne serait-ce qu'arithmétiquement — est beaucoup
plus fort qu'admettre qu'il est consistant, donc à partir du
moment où on l'admet comme vrai, l'étape épistémologique à l'admettre
comme consistant devrait être gratuite). Le principe de réflexion que
j'ai encadré ci-dessus rend la réticence à admettre
que ZFC est consistant encore plus bizarre dans ce
contexte : si je suis prêt à admettre la consistance de tous ses
sous-systèmes finis, je devrais bien admettre la consistance de la
théorie tout entière ; plus exactement, si on me fournit un modèle
simple permettant de construire, pour tout ensemble fini T₀
d'axiomes de ZFC, une preuve du fait que T₀
est consistant (et en outre, une méta-preuve du fait, d'ailleurs plus
ou moins évident, que ce procédé fonctionne bien), il serait
extrêmement bizarre de ne pas en admettre la conclusion, à savoir que
tout ensemble fini T₀ d'axiomes de ZFC est
consistant.