David Madore's WebLog: Ce que « vrai » veut dire en mathématiques

[Index of all entries / Index de toutes les entrées • Latest entries / Dernières entrées • XML (RSS 1.0) • Recent comments / Commentaires récents]

↓Entry #2093 [older|※ permalink|newer] / ↓Entrée #2093 [précédente|※ permalien|suivante] ↓

(samedi)

Ce que « vrai » veut dire en mathématiques

Une des difficultés que rencontrent les gens qui font un peu de logique mathématique mais qui n'en ont pas trop l'habitude — et une difficulté qui sous-tend beaucoup de discussions sur la philosophie des mathématiques — c'est que les gens ne savent plus ce que « vrai » veut dire. Par exemple, quand on discute du théorème de Gödel ou de la différence entre l'ensemble des théorèmes de l'arithmétique de Peano et l'ensemble des énoncés vrais de l'arithmétique, ceci cause souvent un certain malaise (voir par exemple la note #2b de l'entrée précédente). J'ai souvent tourné autour de cette question dans ce blog, mais je n'ai jamais essayé de présenter les choses de façon synthétique. En réponse à une question, je vais donc essayer de dissiper la confusion (ce qui me permettra de renvoyer à la présente entrée quand la question se reposera à l'avenir).

(Eh oui, ce qui suit est très long. Je croyais avoir trois fois rien à raconter, et une fois de plus j'ai pondu des pages… et des pages… et des pages, en essayant de « parler » à la fois à plusieurs niveaux d'expertise différents. J'ai mis en plus petits caractères les passages qui sont une digression par rapport à l'essentiel de mon propos, mais de façon générale j'ai essayé de faire en sorte qu'on puisse comprendre un passage même en ayant lu ce qui précède en diagonale. Peut-être que j'aurais dû publier tout ça sous forme de feuilleton, en plusieurs entrées de blog, mais je trouvais que ça nuisait à la cohérence de l'ensemble.)

Énoncés mathématiques : énoncés ensemblistes et énoncés arithmétiques

Avant de commencer, il faut expliquer un peu comment sont fichus les énoncés mathématiques. Sans rentrer immensément dans les détails, ce qu'on appelle formule ou prédicat, formellement, c'est un machin formé à partir des formules élémentaire x=y et x∈y (pour x,y deux variables quelconques), reliées par des connecteurs logiques ∧ (conjonction), ∨ (disjonction), ¬ (négation), ⇒ (implication), et précédés des quantificateurs ∀ (universel) et ∃ (existentiel) qui servent à lier les variables libres. (On peut toujours, si on veut, s'arranger pour que les quantificateurs soient en tête de formule.) Quand il n'y a aucune variable libre (toutes sont quantifiées), on dit qu'on a affaire à un énoncé (ou formule close). Par exemple, ∀x∃y(x∈y) est un énoncé qu'on lira informellement comme tout ensemble x est un élément d'un autre ensemble y. A priori, on a envie qu'un énoncé soit vrai ou faux (et celui qui précède est certainement vrai), mais il s'agit justement d'expliquer un peu mieux ce que ça veut dire.

Ce que je viens de définir, ce sont les formules et énoncés [du langage] de la théorie des ensembles (ou plus exactement, du langage de la théorie des ensembles du premier ordre), ou plus simplement : ensemblistes. La convention orthodoxe des mathématiques veut que toutes les mathématiques soient faites dans la théorie des ensembles, donc tout énoncé mathématique doit pouvoir se formuler dans ce langage. Par exemple, l'hypothèse de Riemann, la conjecture de Poincaré, ou le problème P=NP sont des énoncés de la théorie des ensembles. En général, les énoncés mathématiques réels utilisent beaucoup d'autres notations que celles que j'ai autorisées ci-dessus, mais ce n'est pas grave parce qu'on est censé croire qu'elles sont toujours définissables dans la théorie des ensembles — on peut toujours s'y ramener.

Maintenant, il y a des énoncés auxquels je vais accorder une importance particulière dans ma discussion, ce sont les énoncés dits arithmétiques (du premier ordre). Moralement, les énoncés arithmétiques sont ceux qui ne parlent que des entiers naturels (et pas d'ensembles d'entiers naturels, de nombres réels ou d'autres ensembles plus compliqués). Formellement, les formules arithmétiques s'obtiennent en partant des termes 0, 1, x+y, x·y et x↑y (notation puissance), où x et y sont des variables ou bien eux-mêmes des termes, qui servent à former des formules élémentaires u=v où u et v sont deux termes, qu'on relie ensuite par les connecteurs logiques comme précédemment, en gardant à l'esprit que cette fois-ci les quantificateurs sont censés se comprendre, moralement, comme des quantificateurs sur les entiers naturels. Par exemple, ∀x∃y(x=2y∨x=2y+1) est un énoncé arithmétique (qui exprime informellement le fait que tout entier naturel x est soit pair soit impair, et dont on va certainement vouloir dire qu'il est vrai).

A priori, ce que j'ai défini comme énoncés arithmétiques formels est quelque chose de totalement distinct des énoncés formels de la théorie des ensembles (il n'y a pas d'inclusion des uns dans les autres). En fait, on peut transformer un énoncé arithmétique en un énoncé ensembliste : ce qui permet de faire cette transformation, c'est le fait que l'ensemble ℕ des entiers naturels (et des opérations +, ×, ↑ dont on veut le munir) est définissable de façon unique en théorie des ensembles (autrement dit, il existe une certaine formule Nat(x) qui dit x est l'ensemble des entiers naturels muni de ses opérations standard et c'est un théorème — de toute formalisation raisonnable de la théorie des ensembles, notamment de ZFC — qu'il existe un unique x=(ℕ,+,×,↑) qui vérifie cette formule Nat(x)). Une fois ce fait établi, quand on a un énoncé arithmétique, on peut le transformer en énoncé ensembliste essentiellement en faisant porter tous ses quantificateurs sur des éléments de ℕ (et en interprétant les opérations arithmétiques, dans les termes, au moyen des opérations dont ℕ est muni), c'est-à-dire par exemple que l'énoncé arithmétique ∀x∃y(x=2y∨x=2y+1) se réécrit en énoncé ensembliste ∀x∈ℕ.∃y∈ℕ.(x=2y∨x=2y+1). J'identifierai audacieusement l'énoncé arithmétique de départ avec l'énoncé ensembliste ainsi obtenu. Si on veut être précis sur la différence, il faudrait noter ℕ⊧P l'énoncé ensembliste qui dit la même chose que l'énoncé arithmétique P (et ceci se lit P est vrai dans ℕ : on voit poindre ici le mot dangereux).

On va voir que cette distinction entre énoncés arithmétiques et énoncés qui ne le sont pas va avoir énormément d'importance pour la discussion. Mais la première chose à signaler, c'est que les énoncés ensemblistes ont beaucoup plus de pouvoir expressif que les énoncés arithmétiques : toutes les mathématiques se font dans le cadre ensembliste, alors que le cadre arithmétique ne permet de dire que certaines choses — mais ces choses sont néanmoins fort importantes.

À titre d'exemple, le théorème de Fermat est un énoncé arithmétique. L'hypothèse de Riemann n'est pas prima facie un énoncé arithmétique (car il y est question d'une fonction de la variable complexe), mais en fait on sait trouver un énoncé arithmétique qui lui est démontrablement équivalent, donc on peut faire semblant que l'hypothèes de Riemann est arithmétique. Il y a beaucoup d'énoncés mathématiques importants qui, s'ils ne sont pas formellement arithmétiques, peuvent en fait s'y ramener assez facilement : par exemple, un énoncé du style tout graphe fini qui n'admet pas K5 ou K3,3 comme mineur est coloriable au moyen de 4 couleurs ou tout groupe simple fini d'ordre impair est cyclique peut se réécrire comme un énoncé arithmétique, parce que le concept de groupe fini ou de graphe fini peut se « coder » comme un entier naturel. Même P=NP, si on est assez astucieux, peut se voir comme un énoncé arithmétique. (Évidemment, si on veut pinailler, le concept d'énoncé « se ramenant » à un énoncé arithmétique n'est pas parfaitement bien défini puisque, si on veut, tout énoncé qui est un théorème est démontrablement équivalent à 2+2=4 qu'on peut qualifier d'énoncé arithmétique.) En revanche, quelque chose comme l'hypothèse du continu n'est pas un énoncé arithmétique et ne peut pas s'y ramener.

Je devrais peut-être aussi mentionner, comme intermédiaires entre les énoncés arithmétiques et les énoncés ensemblistes, ceux qu'on appelle les énoncés arithmétiques du second ordre : ce sont essentiellement les énoncés qui ont le droit de parler d'entiers naturels et aussi d'ensembles d'entiers naturels (ou, si on préfère, de suite d'entiers naturels, ou de nombres réels : tout ceci revient essentiellement au même), mais pas plus. Les énoncés arithmétiques du second ordre ont deux sortes de variables, des variables d'« individus » qui portent sur les entiers naturels et des variables de « prédicats » qui portent sur des propriétés (ou ensembles) d'entiers naturels. Néanmoins, je souligne que quand on dit qu'un énoncé est arithmétique tout court, cela veut dire arithmétique du premier ordre (comme défini plus haut).

Maintenant qu'est établie cette notion d'énoncé ensembliste et d'énoncé arithmétique, qu'est-ce que la vérité ?

Le cadre des mathématiques

Deux points de vue philosophiques

Je commence par un peu d'agitage de mains philosophique (ne serait-ce que pour dire qu'il n'est pas vraiment pertinent). La plupart des gens qui réfléchissent sur l'épistémologie des mathématiques vont adopter une position proche de l'une ou l'autre des points de vue qui suivent :

  • Le point de vue formaliste (en simplifiant à l'extrême) considère les mathématiques comme une sorte de jeu typographique : on part d'un système formel qui a un certain nombre d'axiomes (donc typiquement, ZFC s'il s'agit de faire de la théorie des ensembles, ou peut-être Peano si on se limite à l'arithmétique), on applique mécaniquement des règles de déduction et on arrive à des énoncés qu'on qualifie de théorèmes. La notion de vérité n'a alors pas de sens à ce niveau-là (comme je vais l'expliquer, elle en a quand même un par réflexion), seul importe le fait que tel ou tel énoncé soit un théorème.
  • Le point de vue platoniste suppose au contraire (et toujours en simplifiant de façon caricaturale) que les objets mathématiques ont une existence réelle (dans ce qu'on appelle parfois avec humour le paradis platonicien), les énoncés mathématiques ont réellement un sens concernant ces objets, donc une valeur de vérité, et les théorèmes ne servent qu'à approcher cette vérité — on part d'axiomes « évidemment vrais » et on en déduit des choses toujours vraies mais qu'on espère moins évidentes.

Évidemment, toutes sortes de nuances et de points de vue intermédiaires sont possibles : par exemple, on peut penser — et c'est plus ou moins ma position — que les entiers naturels existent dans le paradis platonicien, donc que les énoncés arithmétiques ont une « vraie vérité » indépendante de notre volonté, mais que les énoncés concernant la théorie des ensembles sont avant tout une question de définition de ce qu'on appelle « ensemble ».

Voilà pour le regard philosophique. Mais j'insiste sur le fait qu'il ne doit pas vraiment avoir d'incidence sur ce que je vais dire : si je prétends par exemple (cf. l'entrée précédente) que l'ensemble des énoncés arithmétiques vrais n'est pas un ensemble récursivement énumérable contrairement à l'ensemble des théorèmes de l'arithmétique de Peano, c'est une affirmation mathématique et non philosophique, et c'est un théorème, cela ne dépend en rien du point de vue philosophique qu'on peut adopter.

Deux systèmes formels : PA et ZFC

Je ne chercherai pas à expliquer de façon générale ce qu'est un système formel, ni quelles sont les conditions exactes dont j'ai besoin à leur sujet : disons juste, informellement, que c'est une collection — éventuellement infinie — d'axiomes à partir desquelles on produit des théorèmes par les règles de la logique. (On aura généralement besoin, entre autres choses, que l'ensemble des axiomes soit au moins récursif, c'est-à-dire essentiellement, produit par une règle simple, de façon qu'il n'y a aucune difficulté à décider si quelque chose est un axiome ou non. Par ailleurs, la logique utilisée pour faire des démonstrations est celle qu'on appelle la logique du premier ordre.)

Je me contenterai de deux exemples, que je ne vais même pas chercher à décrire exactement : l'arithmétique de Peano [du premier ordre] (que je noterai aussi : PA), et la théorie des ensembles de Zermelo-Fraenkel (avec choix) (ZFC).

L'arithmétique de Peano est un système formel pour faire de l'arithmétique : il utilise le langage de l'arithmétique, et ses axiomes sont des énoncés arithmétiques ; tous ses théorèmes sont donc, eux aussi, arithmétiques : l'arithmétique de Peano ne connaît rien d'autre que les entiers naturels. Ses axiomes sont constitués d'un petit nombre d'axiomes extrêmement simples (leur nature exacte dépend des opérations arithmétiques qu'on admet, notamment si on admet la fonction puissance, la relation d'ordre, etc. — mais ce n'est pas très important) et d'une famille infinie d'axiomes appelé le schéma de récurrence du premier ordre qui affirme le principe de récurrence pour tout prédicat (=toute formule) qu'on peut écrire dans le langage (i.e., pour toute formule Φ(n) ayant au moins une variable libre n et éventuellement d'autres variables libres m1,…,mr, on postule un axiome ∀m1⋯∀mr(Φ(0)∧∀n(Φ(n)⇒Φ(n+1))⇒∀n(Φ(n)))). Il existe des variantes affaiblies de l'arithmétique de Peano dans lesquelles on ne postule ce principe de récurrence que pour certaines formules Φ particulières.

La théorie des ensembles de Zermelo-Fraenkel, elle, est un système d'axiomes pour la théorie des ensembles. Ses axiomes, de nouveau, sont en nombre infini à cause d'un ou deux schémas d'axiomes appelés le schéma de compréhension et le schéma de remplacement (on peut éventuellement omettre le schéma de compréhension qui est impliqué par le schéma de remplacement correctement formulé). Le C de ZFC indique que l'axiome du choix est inclus (celui-ci ne me concerne pas particulièrement ici entre autres parce qu'il n'a aucune conséquence arithmétique). La convention orthodoxe veut que toutes les mathématiques soient faites — par défaut — dans ce système. Autrement dit, quand un mathématicien prétend avoir démontré l'hypothèse de Riemann, il faut croire par défaut qu'il prétend en avoir produit une démonstration qui pourrait se formaliser dans ZFC. On peut aussi chercher à affaiblir ZFC en considérant des variantes dans lesquelles les schémas de compréhension et de remplacement sont limités à certaines formules (et éventuellement en supprimant d'autres axiomes comme celui de l'ensemble des parties : par exemple, la théorie des ensembles de Kripke-Platek est une théorie assez importante obtenue en affaiblissant ZFC ; une autre, qui est incomparable avec elle mais plutôt plus faible et beaucoup moins intéressante, est la théorie des ensembles de Zermelo, qui s'obtient en retirant de Zermelo-Fraenkel la partie Fraenkel c'est-à-dire le schéma de remplacement). À l'inverse, on peut renforcer ZFC en y ajoutant différents axiomes dits de grands cardinaux (le plus petit d'entre eux étant l'axiome IC qui affirme l'existence d'un cardinal inaccessible).

Sur le rapport entre les deux systèmes PA et ZFC, il faut souligner plusieurs choses :

  • 1º, que les axiomes de PA sont des théorèmes de ZFC. Plus exactement, ZFC démontre l'existence (et l'unicité) d'un ensemble ℕ muni de différentes opérations +, ×, ↑, qui vérifient les axiomes de Peano. Par conséquent, tout théorème de PA (interprété dans ℕ pour transformer l'énoncé arithmétique en énoncé ensembliste) est un théorème de ZFC. (Bien entendu, comme ZFC peut parler d'ensembles alors que PA ne parle que d'entiers naturels, il n'y a aucune chance d'avoir une réciproque générale.)
  • 2º, si tout théorème de PA est un théorème de ZFC, un des fruits du théorème de Gödel sera que même si on se limite aux énoncés arithmétiques, la réciproque n'est pas vraie : il existe des énoncés arithmétiques qui sont des théorèmes de ZFC et qui ne sont pas démontrables dans PA. (Un tel énoncé sera celui qui affirme que 0=1 n'est pas démontrable à partir des axiomes de Peano en suivant les règles de la logique du premier ordre — voir ci-dessous pour l'explication de pourquoi ceci est bien un énoncé arithmétique.) En fait, ZFC est immensément plus puissant que PA et démontre énormément de choses, y compris des énoncés arithmétiques, et notamment des énoncés arithmétiques qui « parlent de » PA que PA ne peut pas atteindre.
  • 3º, que, malgré tout, cette différence forte du point de vue de la logique n'est pas visible dans les mathématiques « usuelles ». En effet, une sorte de métaconjecture des logiciens prétend que tout théorème mathématique naturel (c'est-à-dire, pas concocté exprès par un logicien pour réfuter la métaconjecture) qui peut s'écrire de façon arithmétique est, en fait, démontrable dans PA. Autrement dit : même si les mathématiciens prétendent vouloir travailler dans ZFC, et même si ce système est incroyablement plus fort que PA, les mathématiciens ne savent pas utiliser cette force, et ne démontrent en fait que des choses qui — lorsqu'il s'agit d'énoncés arithmétiques — sont déjà des théorèmes de PA. Bon, il y a quelques contre-exemples à cette métaconjecture, mais la théorie de l'analyse ordinale nous apprend que ces contre-exemples se manifestent lorsque interviennent des ordinaux supérieurs ou égaux à ε₀, ce qui est excessivement rare en dehors de la logique.

Puisque j'ai très brièvement mentionné plus haut le langage de l'arithmétique du second ordre, où on a le droit de parler à la fois d'entiers naturels et d'ensembles d'entiers naturels, je peux aussi dire un mot sur les systèmes formels qui servent à raisonner dans ce langage : ils s'obtiennent généralement en prenant les axiomes de Peano, pour lesquels cette fois l'axiome d'induction peut s'écrire au second ordre (c'est-à-dire ∀X(X(0)∧∀n(X(n)⇒X(n+1))⇒∀n(X(n))), la différence étant que maintenant on a le droit de quantifier sur une propriété X des entiers naturels et on n'a donc qu'un seul axiome à écrire), et en ajoutant un schéma dit de compréhension qui affirme que toute formule Φ(n) donne naissance à une propriété correspondante, i.e., ∀⋯∃X∀n(X(n)⇔Φ(n)) (la notation ∀⋯ indique simplement qu'il faut quantifier universellement sur toutes les autres variables de Φ, ce n'est pas très important). Si on postule ce schéma pour toutes les formules Φ, y compris celles qui ont des variables de propriété/prédicat liées dans Φ, on obtient la théorie de l'arithmétique du second ordre entière (ou traditionnellement, analyse classique), parfois notée PA², et c'est une théorie beaucoup plus forte que PA (mais beaucoup plus faible que ZFC). En revanche, si on se limite aux formules Φ qui n'ont pas de quantificateur sur les propriétés/prédicats, on obtient une théorie beaucoup plus faible, parfois notée ACA₀ ou parfois appelée analyse élémentaire, et elle démontre les mêmes formules arithmétiques que PA.

Vérité et démontrabilité

Le point crucial dans ce qui va suivre est que les mathématiques peuvent parler d'elles-mêmes (c'est ce que j'appelle de façon un peu vague la réflexion). Et notamment que, au moins dans certaines conditions, comme je vais tenter de l'expliquer, des phrases comme P est vrai ou P est un théorème, si P est un énoncé mathématique, deviennent elles-mêmes des énoncés mathématiques. Ou même l'énoncé si P est un théorème, alors P est vrai. Il va falloir distinguer soigneusement le cas d'un énoncé ensembliste général et d'un énoncé arithmétique, et aussi distinguer selon que P dans ce qui précède est un énoncé précis fixé ou bien une variable libre.

Un mot sur le codage de Gödel

J'ai expliqué brièvement que les énoncés arithmétiques pouvaient servir à parler de toutes sortes de données combinatoires finies, par exemple des graphes finis : ceux-ci peuvent se coder comme des entiers naturels. Il en va de même des suites finies de symboles (i.e., « mots ») choisis parmi un alphabet fini (ou dénombrable) : par exemple, sur un alphabet de moins de 1000 symboles on pourrait choisir un code à trois chiffre pour chaque symbole, et coder chaque mot par la concaténation des codes en question (i.e., lire le mot comme un nombre en base 1000).

L'important est de se rendre compte — et ce n'est pas totalement trivial mais ce n'est pas non plus difficile — que toutes sortes de manipulations syntaxiques sur les suites de symboles, y comprises celles qui servent à définir les règles de la logique formelle, peuvent s'écrire par des formules arithmétiques opérant sur ce codage. (En fait, toute manipulation algorithmique peut se décrire par une formule arithmétique.) C'est ce qui permet aux mathématiques, et plus précisément à des énoncés arithmétiques, de parler d'autres énoncés mathématiques (pas forcément eux-mêmes arithmétiques).

La réflexion : être vrai

Commençons par quelque chose de trivial, qui n'utilise pas le codage de Gödel.

Si P est un énoncé précis fixé, définir ce que signifie P est vrai est extrêmement simple : cela signifie simplement… P. Autrement dit, le ciel est bleu est vrai est complètement synonyme de le ciel est bleu, ou encore le ciel est bleu est vrai est vrai. La notion de vérité est alors une simple redondance oratoire (dire j'ai démontré l'hypothèse de Riemann ou dire j'ai démontré que l'hypothèse de Riemann est vraie est équivalent). Néanmoins, cette remarque n'est pas inutile, parce que, par exemple, on va voir que P est un théorème, lui, a un sens bien différent de P. Je souligne aussi que, à cause de ma définition totalement triviale, P est vrai est un énoncé arithmétique exactement quand P l'est (ceci étant, on peut choisir de considérer un énoncé arithmétique P comme un énoncé ensembliste, comme je l'ai expliqué, et pour insister sur ce fait, on peut dire P est vrai dans ℕ, auquel cas cette précision doit laisser comprendre qu'on regarde l'énoncé comme un énoncé ensembliste).

La réflexion : être un théorème

Maintenant, qu'est-ce que cela signifie de dire qu'un énoncé P est un théorème ? D'abord, cela sous-entend un système formel dont on prétend qu'il découle des axiomes — typiquement ZFC ou PA. Mais par ailleurs, dire qu'un énoncé P est un théorème peut être considéré comme une affirmation du langage courant (i.e. : un mathématicien en a effectivement trouvé ou publié une démonstration), ou peut aussi se comprendre comme un énoncé mathématique à part entière : en effet, les systèmes formels considérés (ZFC et PA, au moins) sont des ensembles mathématiquement bien définis de suites de symboles, et les règles de la logique sont elles aussi mathématiquement bien définies au niveau des suites de symboles, de sorte que l'affirmation il existe une démonstration, dans le cadre de ce système formel, de la suite de symboles P, i.e., P est un théorème (ou de façon complètement synonyme, P est démontrable), devient elle-même un énoncé mathématique, grâce au codage de Gödel. C'est surtout ça qu'on appelle la réflexion : les mathématiques parlent d'elles-mêmes (ou plutôt, parlent des systèmes formels qui nous servent à faire des mathématiques).

Pour ce qui est des notations, on écrit ZFC⊢P (resp. PA⊢P) pour l'énoncé P est un théorème de ZFC (resp. P est un théorème de l'arithmétique de Peano). Si on ne veut pas préciser le système formel dont on affirme que P est un théorème, on peut aussi l'écrire □P (le carré est une notation inspirée de la logique modale, avec laquelle il y a des liens) : ceci signifie donc T⊢P pour une certaine théorie T qui est censée être claire d'après le contexte. Pour varier le langage, on dit souvent est démontrable, ce qui est complètement synonyme de est un théorème.

Ce qui est peut-être un peu surprenant, d'ailleurs, c'est que cet énoncé mathématique P est un théorème est toujours un énoncé arithmétique, même si P est un énoncé ensembliste (et qu'il faut alors comprendre P est un théorème de ZFC), parce que les démonstrations formelles sont des manipulations de suites finies de symboles, qui peuvent se coder comme des entiers naturels : c'est très fastidieux à faire explicitement, mais il n'y a aucune difficulté fondamentale. Au moins dans des systèmes formels vaguement raisonnables comme ZFC ou PA. Par exemple, autant l'hypothèse du continu est un énoncé ensembliste qui ne se ramène pas à un énoncé arithmétique, autant l'énoncé l'hypothèse du continu est indécidable dans ZFC (c'est-à-dire : l'hypothèse du continu n'est pas démontrable dans ZFC et sa négation ne l'est pas non plus) est, pour sa part, un énoncé arithmétique.

Le rapport entre vérité et démontrabilité

Une petite fiction mathématique

Je devrais peut-être évoquer une petite fiction mathématique qui aidera à mettre en lumière la distinction entre les concepts.

J'ai souligné que dire j'ai démontré l'hypothèse de Riemann est exactement équivalent à dire j'ai démontré que l'hypothèse de Riemann est vraie (puisque être vrai est juste, dans ce contexte, une redondance oratoire). Mais que signifierait j'ai démontré que l'hypothèse de Riemann est démontrable [i.e. est un théorème] ? Ce serait une situation étrange : j'aurais non pas constitué une suite de symboles sur papier formant une démonstration de l'hypothèse de Riemann mais produit une (autre) suite de symboles démontrant qu'une telle démonstration existe ! Et comme cette (méta-)démonstration n'a pas de raison d'être constructive, ceci ne nous donne pas une démonstration de l'hypothèse de Riemann, on a juste démontré un énoncé arithmétique qui prétend qu'une telle démonstration existe.

(Évidemment, dans la pratique, si un mathématicien disait j'ai démontré que l'hypothèse de Riemann est un théorème, il y a fort à parier qu'il voudrait en fait dire j'ai démontré l'hypothèse de Riemann, parce qu'il serait assez hautement invraisemblable d'arriver à produire une démonstration du fait que l'hypothèse de Riemann est un théorème autrement qu'en démontrant l'hypothèse de Riemann. C'est la raison pour laquelle la différence n'intéresse surtout que les logiciens, les autres matheux confondent allègrement les notions. Mais ça n'a rien de conceptuellement impossible : continuons donc sur cette expérience de pensée.)

Le formaliste le plus extrême pourrait s'offusquer de ma terminologie : pour lui, les symboles mathématiques ne veulent rien dire, et avoir démontré l'énoncé que je traduis l'hypothèse de Riemann est un théorème n'a pas de signification particulière, c'est une suite opaque de symboles (qui correspond formellement à ce que j'ai appelé un énoncé arithmétique) mais qui n'a rien à voir avec l'autre suite de symboles qu'on appelle l'hypothèse de Riemann, et tant qu'on n'a pas produit une suite de symboles correspondant à une démonstration de l'hypothèse de Riemann, on ne passe pas par la case gagner un million de dollars. C'est-à-dire que, pour le formaliste, il y a un énoncé de la vie courante l'hypothèse de Riemann est un théorème (i.e., un mathématicien en a effectivement trouvé ou publié une démonstration) et un énoncé mathématique formel ZFC⊢RH, et il n'y a pas particulièrement de lien entre eux : c'est moi qui, dans ma définition de l'énoncé formel, ai prétendu qu'elle reflétait arithmétiquement la notion de preuve que le formaliste utilise, mais comme le formaliste n'admet pas que les énoncés mathématiques ont un sens réel, cet énoncé arithmétique formel n'a aucun rapport, à ses yeux, avec l'énoncé courant qui dit que l'hypothèse de Riemann a été démontrée. Donc le formaliste va m'accuser soit d'essayer d'arnaquer le lecteur, soit au moins d'utiliser une terminologie confusante. Néanmoins, même pour le formaliste, il y a certains rapports entre ces énoncés, comme il s'agit d'expliquer.

Le mathématicien qui a démontré l'hypothèse de Riemann (i.e., que l'hypothèse de Riemann est vraie, on notera ça RH), doit recevoir un million de dollars. Qu'en est-il du mathématicien qui aurait démontré que l'hypothèse de Riemann est un théorème (i.e., □RH) ?

La première observation qu'on peut faire, c'est que si je possède une démonstration sur papier de RH, je peux — en principe — la transformer en une démonstration de □RH. En effet, la démonstration de RH, si elle est correctement formalisée, définit une suite de symboles explicitement connue qui vérifie les règles de la logique et qui aboutit à RH : je peux alors démontrer □RH en disant voyez, la suite de symboles suivante convient. A priori, donc, démontrer □RH est moins bien que démontrer RH. (Ce fait peut surprendre si on a à l'esprit que être un théorème est plus fort que être vrai, mais ce que je dis ici est que si on sait démontrer que quelque chose est vrai alors on sait démontrer que cette chose est un théorème — tout ceci sous-entendu dans le même système formel, par exemple démontrer RH dans PA permet de démontrer PA⊢RH, lui-même dans PA, mais je vais y revenir.)

Y a-t-il néanmoins une réciproque ? Je vais plus ou moins pouvoir rassurer le mathématicien qui aurait démontré □RH en cherchant à démontrer RH. Mais ceci dépend du système formel sous-entendu par □RH :

  • Si on a démontré PA⊢RH, alors on peut en déduire RH, mais seulement dans ZFC (ou en tout cas, il faut un système plus fort que PA) : on touche donc le million de dollars. En effet, comme je vais tenter de l'expliquer plus loin, (PA⊢RH)⇒RH (qui se lit : si l'hypothèse de Riemann est démontrable dans l'arithmétique de Peano, alors elle est vraie) est un théorème de ZFC. Il suffira donc d'appliquer ce théorème après la démonstration qu'on a trouvée de PA⊢RH.
  • Si on a démontré ZFC⊢RH, alors on est moins heureux : aussi surprenant que ça puisse paraître, il n'y a a priori pas de raison que (ZFC⊢RH)⇒RH soit un théorème de ZFC (et même, dans un certain sens, cela ne se produit que si, justement, RH est déjà un théorème de ZFC, mais je vais y revenir). A-t-on pour autant perdu tout espoir de gagner le million de dollars ? Non, car si on n'obtient pas une démonstration de RH dans ZFC, on en obtient une dans un système plus fort, par exemple ZFC+IC où IC signifie il existe un cardinal inaccessible : en effet, l'énoncé (ZFC⊢RH)⇒RH est un théorème de ZFC+IC, et on a donc démontré RH dans ce système. Ce sera au jury de décider si cela mérite la récompense, mais il est fort probable qu'ils en conviennent, car IC est un axiome passablement standard et il n'y a pas spécialement plus de raison de demander que les mathématiques se fassent dans ZFC que dans ZFC+IC.

Démontrer P permet de démontrer □P

Une des choses que j'ai expliquées dans le cours de ma petite fiction ci-dessus est que si on possède une démonstration d'un énoncé mathématique P, on peut en tirer une démonstration de l'énoncé □P qui affirme, justement, que P est démontrable (la démonstration se « reflète »). Il suffit pour cela de prendre la démonstration de P dont on dispose, la rendre complètement formelle, la transformer en un nombre codant cette suite de symboles, entrer ce nombre dans l'énoncé qui dit D est une démonstration de P, et vérifier que toutes les règles de logique ont été suivies à chaque étape.

On peut même être plus précis : si j'ai démontré P dans ZFC, alors j'en déduis une démonstration de ZFC⊢P, et cette démonstration-là, elle peut se faire dans un système beaucoup plus faible, comme PA ou comme certains sous-ensembles extrêmement faibles de PA, puisqu'il s'agit simplement de vérifier que des règles de déduction ont bien été suivies (je rappelle que ZFC⊢P est un énoncé arithmétique, donc ça a bien un sens de se demander s'il est démontré par PA). De même, si j'ai démontré P dans PA, alors j'en déduis une démonstration de PA⊢P et cette démonstration elle-même peut se faire dans PA ou dans un système encore plus faible.

Mais il y a mieux, et c'est assez subtil : cet argument-là se reflète à son tour. C'est-à-dire que □P⇒□□P (lire si P est prouvable, alors il est prouvable que P est prouvable) est un théorème (de l'arithmétique de Peano, quel que soit le système formel raisonnable impliqué par le symbole « carré »). C'est un point important, et souvent mal expliqué, dans la démonstration du théorème d'incomplétude de Gödel.

Le schéma de réflexion

Que penser de l'énoncé □P⇒P (qu'il faut parenthéser comme (□P)⇒P) ? Sa lecture naturelle est si P est un théorème, alors P est vrai. On a certainement envie de penser que ceci est vrai, quel que soit l'énoncé P : philosophiquement, c'est, après tout, la justification qu'on utilise, à moins d'être extrêmement formaliste, pour s'intéresser aux théorèmes des mathématiques, on espère bien qu'ils sont vrais.

Pourtant, comme on va le voir autour du théorème d'incomplétude de Gödel (et plus exactement, il s'agit du théorème de Löb dont je vais parler plus loin), même si nous avons envie de croire en la vérité de □P⇒P pour tout énoncé P, les seuls pour lesquels il s'agit effectivement d'un théorème sont ceux pour lesquels P est lui-même un théorème. Autrement dit, ces énoncés □P⇒P, dont on a certainement envie de penser (au moins philosophiquement) qu'ils sont vrais, et qui sont même le postulat épistémologique fondamental des mathématiques, ne sont généralement pas démontrables dans notre système formel. On marche sur de la glace.

Il y a néanmoins des cas favorables : comme je l'expliquerai plus loin quand j'aurai mieux formalisé le concept de vérité, ZFC, par exemple, prouve (PA⊢P)⇒P pour tout énoncé arithmétique P (il le prouve même, d'une certaine manière, uniformément en P) : on dira que ZFC prouve la correction (véracité, ou, en anglais, soundness) arithmétique de PA, ou prouve son schéma de réflexion. Donc même si PA lui-même ne peut pas prouver (PA⊢P)⇒P (au moins pour certains énoncés P), le système plus fort qu'est ZFC, lui, le peut. (Pour ce qui est de (ZFC⊢P)⇒P, les choses sont plus problématiques, mais au moins ceci devrait nous convaincre que le principe général n'est pas sans intérêt.)

La collection de tous les énoncés □P⇒P s'appelle parfois le schéma de réflexion sur le système formel considéré, même si ce terme peut malheureusement aussi désigner d'autres choses (pas totalement sans rapport, mais distinctes). On peut aussi parler de correction (véracité) du système formel. Si on se limite aux énoncés P arithmétiques, on parlera par exemple de correction arithmétique chacune des instances □P⇒P de ce schéma est alors elle-même un énoncé arithmétique).

Modification () : La version initialement publiée de cette entrée utilisait le terme véracité pour traduire l'anglais soundness. Il me semble que correction est plus… correct. Encore que la terminologie est fluctuante : justesse doit se dire aussi (et il y a plein de francophones qui utilisent simplement le mot anglais soundness). Bref, j'ai remplacé véracité par correction, mais en signalant les deux çà et là.

La consistance du système

Il faut faire une mention spéciale des énoncés qui disent 0=1 n'est pas un théorème. Ici 0=1 peut être arbitrairement remplacé par la négation de n'importe quel théorème fixé ; ou encore par le symbole logique ⊥ qui représente le faux. Ces énoncés ¬□⊥, qui sont des énoncés arithmétiques puisque être un théorème est arithmétique, expriment la consistance du système formel considéré (celui sous-entendu par le mot théorème). Par exemple, la consistance de ZFC et la consistance de PA, notées Consis(ZFC) et Consis(PA) sont des énoncés arithmétiques particulièrement importants (et le second sera un exemple d'un énoncé arithmétique qui est un théorème de ZFC mais qui n'en est pas un de PA).

Il faut remarquer que cet énoncé ⊥ n'est pas un théorème se réécrit encore comme si ⊥ est un théorème alors ⊥ (car ¬Q est logiquement équivalent à Q⇒⊥), autrement dit, il est de la forme □P⇒P pour P l'énoncé ⊥ (tautologiquement faux). L'énoncé de consistance du système considéré est donc un cas particulier de ce que j'ai appelé de façon générale ci-dessus schéma de réflexion ou correction du système formel.

Comment rendre les choses uniformes ?

Pour l'instant, dans la présentation que j'ai faite des énoncés P est vrai (qui, je le rappelle, est simplement synonyme de P) et P est un théorème (qui est un énoncé arithmétique sous-entendant un système formel), l'énoncé P était supposé bien défini et fixé. Ce que j'appelle rendre les choses uniformes, c'est permettre à P d'être une variable, c'est-à-dire un objet mathématique (un nombre qui code une suite de symboles) et non plus un énoncé précis fixé (e.g., l'hypothèse de Riemann). Ceci permettra, par exemple, de mettre des quantificateurs sur P (au niveau du discours mathématique lui-même, et pas seulement du discours méta-mathématique où j'explique qu'on peut faire telle ou telle chose pour tout énoncé P).

Être un théorème

Il n'y a pas de difficulté particulière, quand on dit P est un théorème, à faire de P une variable (un entier naturel, qui code une suite de symboles) : de toute façon, la définition que j'ai donnée de P est un théorème sous-entendait déjà tout un codage des énoncés et des démonstrations sous la forme d'entiers naturels, donc cette définition donne naturellement un sens à P est un théorème pour P une variable. Bref, il n'y a ici rien de nouveau.

Points fixes et astuce de diagonalisation

À partir du moment où on dispose d'un moyen uniforme de dire quelque chose sur les énoncés mathématiques, une astuce générale, qu'on appelle l'astuce de diagonalisation, ou parfois astuce de Quine même si elle est largement antérieure (c'est l'adaptation par Gödel du procédé diagonal de Cantor) permet de faire des énoncés qui parlent d'eux-mêmes.

Par exemple, il est possible de créer des énoncés qui disent je suis un théorème ou je ne suis pas un théorème. L'astuce qui permet de faire ça est exactement identique à celle qui permet d'écrire des programmes qui s'écrivent eux-mêmes (même dans un langage de programmation qui ne permet pas simplement au programme d'inspecter son propre code) : quand on dit je suis un théorème, on veut en fait dire quelque chose comme si on remplace la variable dans si on remplace la variable dans Q par la même chose, l'énoncé ainsi obtenu est un théorème par la même chose, l'énoncé ainsi obtenu est un théorème. Il se trouve que l'énoncé je suis un théorème est effectivement un théorème (i.e., il est vrai !), ce n'est pas du tout trivial à montrer et ce n'est pas non plus bien passionnant (c'est le théorème le plus remarquablement zen des mathématiques) ; un énoncé plus intéressant est celui qui dit je ne suis pas un théorème (qui joue un rôle essentiel pour démontrer le théorème de Gödel).

En revanche, si on se penche sur la vérité, on voit qu'il y aura nécessairement un problème : il ne faut surtout pas qu'un énoncé mathématique puisse dire je ne suis pas vrai, sans quoi tout l'édifice des mathématiques s'effondrerait sous le paradoxe. Mais l'astuce de diagonalisation fait que le problème dans cet énoncé n'est pas tant le je de je ne suis pas vrai, c'est l'idée qu'on pourrait définir le vrai de façon uniforme. Il y a donc forcément une limitation sur la manière dont on peut dire P est vrai avec P une variable.

Vérité uniforme des énoncés arithmétiques

Néanmoins, si P est un énoncé arithmétique (variable), on peut écrire dans la théorie des ensembles une définition uniforme de P est vrai (c'est-à-dire, P est vrai dans ℕ, qu'on peut noter ℕ⊧P). Je souligne la différence avec la convention triviale précédente qu'ici P est variable, c'est un codage d'un énoncé arithmétique.

Plus exactement, il existe une fonction « valeur de vérité » bien définie, qui part de l'ensemble des formules arithmétiques à k variables libres, et qui va dans l'ensemble des fonctions de ℕk vers {0,1} (il faut considérer ℕk comme l'ensemble de toutes les substitutions possibles d'un entier naturel aux variables libres de la formule). Cette fonction « valeur de vérité » est définie par induction sur la complexité de la formule. Par exemple, la valeur de vérité de ∃x(P(x)) est obtenue, comme on s'y attend, en considérant celle de P(x) et donnant la valeur 1 pour une certaine substitution des variables lorsqu'il existe une valeur de x pour laquelle la valeur de vérité de P vaut 1. (Si on préfère voir la valeur de vérité comme une partie de ℕk plutôt qu'une fonction ℕk→{0,1}, cela revient à faire une projection.) De nouveau, il n'y a pas de difficulté fondamentale, il suffit d'écrire les choses : ce qui permet de tout faire marcher c'est que ℕ est manipulable dans la théorie des ensembles. Bien entendu, les deux définitions que j'ai données de P est vrai (la définition triviale pour un P explicite, et celle uniforme qui permet à P d'être variable) coïncident — démontrablement — pour tout P explicite.

Mais il faut bien que je souligne ceci : avec la définition que je viens de donner, P est vrai (où P est variable, i.e., une définition uniforme en P) n'a de sens que si P parcourt les énoncés arithmétiques, et lorsque c'est le cas, la formule P est vrai [dans ℕ] est une formule de la théorie des ensembles, on ne peut pas la ramener à une simple formule arithmétique.

En théorie des ensembles, on peut donc, par exemple, définir l'ensemble des énoncés arithmétiques vrais (c'est-à-dire, vrais dans ℕ). On ne peut pas définir l'ensemble des énoncés ensemblistes vrais, sans quoi l'astuce de diagonalisation conduirait à une contradiction : la raison est qu'on ne peut pas manipuler de façon uniforme l'univers de tous les ensembles. On doit donc se contenter de la définition triviale où dire P est vrai signifie simplement P.

On pourrait s'en sortir en introduisant une nouvelle sorte d'objets, les classes, si on se donne des règles assez flexibles pour les manipuler : dans la théorie des ensembles+classes on pourra alors construire l'ensemble des énoncés vrais de la théorie des ensembles ; mais la définition de celui-ci fait nécessairement intervenir les classes, et la théorie des ensembles+classes sera de nouveau impuissante pour définir l'ensemble des énoncés vrais de la théorie des ensembles+classes : il faudrait une nouvelle sorte d'objets, et on n'en finit jamais. Ajouter des types de la sorte n'est pas très intéressant, et il est beaucoup plus intéressant de rester dans la théorie des ensembles et d'ajouter des grands cardinaux, qui sont nettement plus puissants.

Conséquences sur PA vu par ZFC

Pourquoi pensons-nous, intuitivement, que les théorèmes mathématiques sont vrais ? Parce que nous pensons que (1) les axiomes sont vrais et que (2) les règles de logique préservent la vérité. À partir du moment où on peut définir la vérité de façon uniforme, ce raisonnement peut être rendu formel. C'est le cas, par exemple, pour la vérité arithmétique vue depuis la théorie des ensembles : je viens d'expliquer que, dans la théorie des ensembles, il n'y a pas de difficulté à définir une formule ℕ⊧P qui énonce le fait qu'une formule arithmétique variable P est vraie (i.e., vraie dans ℕ), et il n'y a pas non plus de difficulté à définir PA⊢P qui énonce le fait que P est démontrable dans l'arithmétique de Peano : en suivant le fait que les axiomes de Peano sont des théorèmes de ZFC et que la notion de vérité dans ℕ satisfait aux règles de la logique, on arrive assez facilement à démontrer dans ZFC que ∀P((PA⊢P)⇒(ℕ⊧P)) (tout théorème de l'arithmétique de Peano est vrai), c'est-à-dire une variante uniforme de ce que j'ai appelé le schéma de réflexion sur Peano, ou encore sa correction (véracité ou soundness) arithmétique.

En particulier, Consis(PA), l'énoncé (arithmétique !) qui affirme que l'arithmétique de Peano est consistante, est un théorème de ZFC. Le théorème d'incomplétude de Gödel va nous dire qu'il n'est pas un théorème de PA.

Des considérations du même genre permettent de montrer dans le système ZFC+IC, qui ajoute à ZFC l'axiome d'existence d'un cardinal inaccessible, que tout énoncé arithmétique démontré par ZFC est vrai, i.e., ∀P((Arith(P)∧ZFC⊢P)⇒(ℕ⊧P)). (Le point-clé est que l'existence d'un cardinal inaccessible κ permet de construire un modèle — à savoir les ensembles hériditairement plus petits que κ — de ZFC et dont l'ensemble des entiers naturels est bien le même ℕ que dans l'univers.) C'est pour cette raison que j'ai affirmé dans ma petite fiction qu'un mathématicien qui aurait démontré (dans ZFC) que l'hypothèse de Riemann est un théorème de ZFC aurait du coup démontré l'hypothèse de Riemann dans ZFC+IC.

Le théorème de Gödel, thème et variations

Puisque les notions de vérité et de démontrabilité ont des caractéristiques aussi différentes (la vérité arithmétique n'est pas définissable dans l'arithmétique alors que la démontrabilité dans PA l'est), elles doivent forcément être différentes, donc si les théorèmes de PA sont vrais c'est forcément qu'il existe des énoncés vrais qui ne sont pas des théorèmes de PA. Les différentes variantes du théorème de Gödel brodent sur cette idée.

L'énoncé de Gödel

L'astuce de diagonalisation permet de construire un énoncé G (arithmétique !) qui affirme je ne suis pas un théorème (selon ce qu'on voudra, soit de PA soit de ZFC), i.e., G⇔¬□G (ce fait étant démontrable dans le système considéré : on a donc aussi □(G⇔¬□G)). C'est la manipulation de cet étrange énoncé G qui permet de dévoiler les différentes facettes du théorème de Gödel.

Gödel regarde Peano depuis ZFC

Commençons par le cas le plus facile : on travaille dans ZFC et on regarde Peano. On construit donc l'énoncé arithmétique G qui dit je ne suis pas un théorème dans l'arithmétique de Peano.

Comme je l'ai expliqué, ZFC prouve la correction de PA, c'est-à-dire qu'il prouve que tout théorème de PA est vrai (au sens : □P⇒P pour tout énoncé arithmétique). Ainsi, si G était un théorème de PA, il serait vrai, et du coup ne serait pas un théorème de PA (puisque c'est justement ce qu'il affirme), ce qui est une contradiction. Donc G n'est pas un théorème de PA. Mais du même coup, G est vrai (puisqu'il affirme, justement, ne pas être un théorème).

Ce qui précède était un raisonnement tenu dans ZFC : on a donc démontré que G est vrai, et aussi que G n'est pas un théorème de PA (et bien sûr, ¬G n'est pas non plus un théorème de PA puisqu'il est faux). C'est la variante la plus simple de Gödel : on a démontré que Peano ne démontrait pas certains énoncés arithmétiques pourtant vrais.

Les choses étaient ici simplifiées, justement, par le fait que, en travaillant dans ZFC, on peut affirmer sans vergogne que tout théorème de PA est vrai.

Un lemme fondamental

Si on veut travailler dans le système lui-même, il faut être un chouïa plus soigneux. Convenons donc maintenant que je travaille, soit dans PA soit dans ZFC, et que par théorème je parle du système en question ; je considère toujours l'énoncé G de Gödel qui dit qu'il n'est pas un théorème (G⇔¬□G), dans ce même système, donc.

Je tiens le raisonnement suivant (dans lequel j'utiliserai souvent le fait que les règles de la logique peuvent s'appliquer à l'intérieur de du « carré » : par exemple, □(P⇒Q) et □P impliquent □Q — ce qui est clair puisque exprime le fait que si P⇒Q et P sont des théorèmes alors Q en est un).

Supposons □G (i.e., G est démontrable) : alors on a □□G (puisque, comme je l'ai souligné, on a □P⇒□□P pour tout énoncé P). Mais d'autre part, on a □(G⇒¬□G) (cela fait partie de la propriété □(G⇔¬□G) de G). De □G et □(G⇒¬□G) on déduit donc □¬□G. Et de □□G et □¬□G (deux choses contradictoires sont démontrables) on déduit □⊥ (0=1 est démontrable, c'est-à-dire encore le système est inconsistant).

Bref, j'ai obtenu (en raisonnant entièrement dans le système formel considéré) le lemme-clé suivant : □G⇒□⊥ (si G est démontrable alors 0=1 l'est). Remarquons que ce n'est pas pareil que de dire que G n'est pas démontrable (et, comme on va le souligner, □⊥ n'est pas la même chose qu'une contradiction).

Le second théorème d'incomplétude

Le raisonnement du lemme-clé ci-dessus se reflète : on a □(□G⇒□⊥), ou encore □(¬□⊥⇒¬□G) par contraposée, et donc □¬□⊥⇒□¬□G. Faisons maintenant l'hypothèse □¬□⊥ (le système prouve sa propre consistance) : alors on a □¬□G, donc encore (comme □(¬□G⇒G)) □G, ce qui d'après le lemme donne □⊥ (le système est inconsistant).

On a montré, en hiéroglyphes : □¬□⊥⇒□⊥ ; et en français : si le système montre sa propre consistance, alors il est inconsistant. C'est le contenu assez étonnant du « second » théorème d'incomplétude de Gödel : si le système formel (dans lequel j'ai fait tout le raisonnement) montre qu'il n'est pas inconsistant, alors en fait il est inconsistant. Ou, si on préfère la contraposée (¬□⊥⇒¬□¬□⊥) : si le système formel est consistant, alors il ne peut pas montrer qu'il l'est.

Tout ce raisonnement (j'insiste) était fait dans le système formel considéré, qui peut être à peu près n'importe quoi (je n'ai pas envie d'expliquer les conditions précises, mais ZFC comme PA conviennent ; l'idée essentielle est qu'il permette de formaliser l'arithmétique et qu'il soit lui-même défini de façon arithmétique).

Si ZFC regarde Peano, il peut dire la chose suivante : PA est consistant (puisqu'il est vrai, il ne peut pas démontrer le faux), donc il ne peut pas démontrer sa propre consistance. (C'est un nouvel exemple d'un énoncé arithmétique vrai que PA ne démontre pas, mais il est plus parlant que l'énoncé G donné précédemment.)

Ajout () : Voir cette entrée ultérieure pour une reformulation des quelques paragraphes qui précèdent (avec un peu plus de détails sur les conditions de prouvabilité).

Itération et inexhaustibilité

Si on part d'un système formel T raisonnable pour faire des mathématiques — par exemple PA ou ZFC — et qu'on adopte une position épistémologique pas trop formaliste, on a envie de croire que les théorèmes de T, ou au moins ses théorèmes arithmétiques, sont vrais (après tout, le but des mathématiques est de dire des choses vraies, pas juste de manipuler formellement des symboles sur un morceau de papier). Ou à tout le moins, on a envie de croire que T est consistant, c'est-à-dire qu'il ne va pas prouver ⊥ (i.e., 0=1). Comme on vient de le voir, le théorème de Gödel assure que (si c'est effectivement le cas), T ne peut pas le prouver ce fait (Consis(T)). À plus forte raison, il ne peut pas prouver le schéma de réflexion □P⇒P (en fait, le théorème de Löb montrera que les seules instances qu'il prouve effectivement sont celles pour lesquelles il prouve déjà P).

On peut donc avoir envie de définir un système T1 obtenu en ajoutant à T l'énoncé Consis(T) qui affirme la consistance de T, ou peut-être même la totalité du schéma de réflexion sur T : du point de vue épistémologique, comme on pensait que T était non seulement consistante mais même vraie, il est raisonnable d'admettre que T1 l'est aussi (puisqu'elle ajoute à T des énoncés qu'on a eux-mêmes admis comme vrais étant donné que T l'est), et cette nouvelle théorie T1, si elle est effectivement consistante, est strictement plus forte que la théorie T de départ. Du coup, on peut recommencer pour passer de T1 à T2 (en ajoutant soit l'énoncé Consis(T1) ≡ Consis(T+Consis(T)) de la consistance de T1, soit de façon plus audacieuse tout le schéma de réflexion), puis de même à T3, etc. On peut alors définir la théorie Tω qui est formée de la réunion des Tn pour tous les entiers naturels n. Comme chaque théorie Tn+1 (et donc Tω) prouve la consistance de Tn, et qu'une preuve de ⊥ dans Tω devrait forcément en donner une dans un certain Tn, on pourrait penser conclure que Tω va prouver sa propre consistance : il n'en est rien, bien sûr, car Tω prouve bien la consistance de chaque Tn, mais elle ne le fait pas uniformément en n. Si on ajoute l'axiome de la consistance de Tω (ou de façon équivalente, de tous les Tn de façon uniforme), ou peut-être le schéma de réflexion sur Tω, on obtient une théorie Tω+1, sur laquelle on peut recommencer.

On peut avoir envie de penser qu'on obtient ainsi une théorie Tα pour chaque ordinal dénombrable α, mais il y a une difficulté cachée sous le tapis : en effet, quand on écrit T est consistante pour une théorie T, l'énoncé arithmétique en question dépend non seulement de l'ensemble des axiomes de T mais aussi de la manière dont ils sont énumérés. J'ai toujours supposé une énumération « raisonnable » des axiomes de T, notamment si T est PA ou ZFC, mais en itérant de façon transfinie le sens du mot raisonnable devient moins clair.

((Si l'énumération n'est pas « raisonnable », des choses bizarres peuvent se passer. Par exemple, considérons la théorie T dont le n-ième axiome est égal au n-ième axiome de l'arithmétique de Peano dans une énumération raisonnable, sauf si le nombre entier 2n n'est pas somme de deux nombres premiers, auquel cas le n-ième axiome est 0=1. Manifestement, cette théorie est récursivement axiomatisée — c'est-à-dire qu'on peut algorithmiquement décider en temps fini si un énoncé est ou n'est pas un de ses axiomes —, puisque tester si un nombre est somme de deux nombres premiers se fait de façon sûre en temps fini. Si la conjecture de Goldbach est vraie, alors les axiomes de T sont exactement ceux de Peano, tandis que si elle est fausse, T affirme 0=1. Donc Consis(T) implique la conjecture de Goldbach, mais elle l'implique de façon totalement saugrenue.))

(En fait, si on veut monter loin dans les ordinaux, la question ne devient plus d'ajouter des itérations de la consistance de la théorie ou de tel ou tel schéma de réflexion, mais simplement d'axiomes qui disent <telle présentation explicite d'un grand ordinal> est effectivement un ordinal (l'expression effectivement un ordinal sous-tend, en fait, un principe d'induction écrit sous forme d'un schéma d'axiomes). Par exemple, ajouter une variante uniforme du schéma de réflexion sur PA équivaut à ajouter à celui-ci le principe d'induction sur (la présentation explicite standard de) l'ordinal ε₀. De même, si on ajoute à PA un schéma d'axiomes qui traduit, pour tous les segments initiaux de la présentation explicite standard de l'ordinal de Bachmann-Howard, le principe d'induction bien-fondé pour toutes les formules, alors la théorie résultante démontre exactement les mêmes énoncés arithmétiques que la théorie des ensembles de Kripke-Platek que j'ai brièvement mentionnée. On ne sait pas faire ce genre de description explicite pour quelque chose d'aussi fort que ZFC, cependant.)

Un petit malin pourrait être tenté de contourner tout le problème d'ajouter de façon transfinie l'énoncé Consis(T) à une théorie T en créant une théorie T formée en ajoutant à PA (par exemple) l'axiome la théorie T formée en ajoutant à PA cet axiome-ci est consistante, autrement dit, T affirme à la fois les axiomes de Peano et sa propre consistance. L'astuce de diagonalisation permet de fabriquer une telle théorie, ce n'est pas là que réside le problème. Cette astuce permet-elle d'éviter le problème du théorème de Gödel ? Pas du tout : la théorie T est tout simplement inconsistante. En effet, quand Gödel interdit à une théorie consistante de prouver sa propre consistance, le mot prouver doit se comprendre de façon large : il n'est pas non plus possible de postuler sa propre consistance (du point de vue logique, les axiomes sont des théorèmes particuliers dont la démonstration tient en une ligne, et le raisonnement s'applique aussi bien à eux [cf. cette entrée ultérieure]).

Le théorème de Löb

Le théorème de Löb (illustré ici de façon graphique) s'obtient en prenant la démonstration du second théorème d'incomplétude que j'ai donnée plus haut et en remplaçant systématiquement les ¬X par X⇒P (où P est un énoncé fixé une fois pour toutes) et les ⊥ par P (ou, si on veut, le théorème de Gödel est le cas particulier du théorème de Löb lorsque P est le faux logique). L'énoncé du théorème de Löb est donc : si □(□P⇒P) alors □P (soit, complètement en symboles : □(□P⇒P)⇒□P) ; autrement dit, si on peut démontrer P dans le système en prenant pour hypothèse que P est démontrable, alors on peut le démontrer sans cette hypothèse. (Si on préfère, on peut aussi le démontrer en appliquant le second théorème d'incomplétude à la théorie obtenue en ajoutant à la théorie de départ l'axiome ¬P.)

Un cas particulier anecdotique mais amusant est le théorème de Henkin : on applique l'astuce de diagonalisation pour fabriquer un énoncé H qui dit cette fois-ci je suis un théorème, c'est-à-dire qu'on a H⇔□H ; comme en particulier □H⇒H, le théorème de Löb assure que □H, i.e., l'énoncé qui dit je suis un théorème est, effectivement, un théorème (et il est vrai !).

Théories affirmant leur inconsistance, et Gödel-Rosser

Nous savons maintenant que PA ne démontre ni Consis(PA) (qui est pourtant une affirmation vraie) ni ¬Consis(PA) (qui est fausse). La théorie PA′ := PA+Consis(PA), qui ajoute à PA l'affirmation de la consistance de cette dernière, ne démontre pas non plus ni Consis(PA′) ni ¬Consis(PA′). J'ai vaguement expliqué ce qui se passe si on continue à ajouter (de façon éventuellement transfinie) des consistances itérées. Mais d'un autre côté, le fait que PA ne démontre pas Consis(PA) signifie que la théorie PA♠ définie comme PA+¬Consis(PA) est elle aussi consistante (si on arrivait à une contradiction à partir des axiomes de PA♠, ceci fournirait une démonstration par l'absurde de Consis(PA) à partir de PA).

Cette théorie PA♠ := PA+¬Consis(PA) est assez étonnante : elle affirme l'inconsistance de PA et à plus forte raison sa propre inconsistance, et pourtant, elle n'est pas inconsistante. (En particulier, cette théorie n'est pas vraie : l'axiome ¬Consis(PA) est tout simplement faux.) Le théorème de complétude de Gödel permettra d'y voir plus clair mais, en attendant, on peut se demander : la théorie PA♠ est-elle incomplète ? Autrement dit, existe-t-il des énoncés P tels que ni P ni ¬P ne soit un théorème de PA♠ ? Cette fois, on ne peut pas prendre l'énoncé Consis(PA♠), puisque, comme on l'a souligné, ¬Consis(PA♠) (c'est-à-dire □⊥) est un théorème de PA♠ (même s'il est faux). L'énoncé G de Gödel (je ne suis pas un théorème) ne marche pas non plus : car ici, comme PA♠ démontre □⊥, en particulier, il démontre □P pour tout P, et notamment □G, c'est-à-dire ¬G.

Pourtant, PA♠ n'est pas non plus complète, c'est un cas particulier du théorème de Gödel-Rosser, mais c'est plus technique à voir ; il se démontre en changeant un peu l'énoncé G : au lieu de dire je ne suis pas démontrable, l'énoncé modifié affirme il y a une démonstration de ma négation qui soit plus courte que toute démonstration de moi. Je ne rentrerai pas dans les détails de pourquoi. Mais je mentionne brièvement que ce genre d'astuce permet aussi de fabriquer, par exemple, un énoncé arithmétique vrai P tel que PA ne démontre pas P (ni ¬P, bien sûr !) et que PA même enrichi de Consis(PA) ne démontre pas non plus ¬(PA⊢P) (ni bien sûr PA⊢P) : autrement dit, P est vrai, indémontrable par Peano, et ce fait-là est aussi indémontrable par Peano (même relativement à la consistance de Peano, qui est certainement nécessaire dans l'histoire).

Un mot sur les modèles et le théorème de complétude de Gödel

Dans toute cette présentation, j'ai évité très soigneusement de parler de modèle. La raison est que ce concept a tendance à embrouiller les idées : quand je raconte que l'énoncé de Gödel G formé sur l'arithmétique de Peano est vrai, des gens qui sont légèrement familiers avec ce concept me demandent parfois mais vrai dans quel modèle ? — la réponse est dans l'ensemble ℕ des entiers naturels, bien sûr !, mais en fait la question traduit une certaine confusion de l'esprit, parce que si je dis tout entier est somme de quatre carrés personne ne me demande dans quel modèle ? alors il n'y a aucune raison de poser cette question pour l'énoncé de Gödel (quand on dit d'un énoncé arithmétique qu'il est vrai, cela signifie : vrai dans l'ensemble ℕ des entiers naturels).

La théorie des modèles semble donc quelque chose qu'il faut surtout éviter quand on expose le sujet aux débutants. Néanmoins, à ce stade-là, je peux en dire un tout petit mot, en petits caractères, pour présenter l'idée générale qu'un modèle est une sorte de monde alternatif et que la « raison » pour laquelle certains énoncés, bien que vrais, ne soient pas démontrables, est qu'il existe des modèles non-standards où ils sont faux.

Comme les seuls systèmes formels dont je veux vraiment parler sont PA et ZFC, je peux les discuter séparément.

Un modèle de PA est un ensemble M muni d'opérations +M, ×M et ↑M (et d'éléments 0M et 1M) qui, quand on exprime les axiomes de Peano du premier ordre (ce que j'ai noté PA) sur ces objets, les vérifie. Et par conséquent, il vérifie aussi tous les théorèmes de PA (par exemple, les opérations +M et ×M seront commutatives et associatives puisque ce sont des théorèmes de PA). Un exemple de modèle de PA est, bien sûr, l'ensemble ℕ des entiers naturels muni de ses opérations usuelles : c'est ce qu'on appelle le modèle standard de PA, et tout autre modèle (c'est-à-dire, tout modèle non isomorphe à ℕ) est donc dit non-standard. En fait, il s'avère que tout modèle de PA « commence » par le modèle standard ℕ, au sens où ℕ est isomorphe à une partie de M située au début (tout élément plus petit qu'un de ses éléments est lui-même dedans) : on dit qu'il s'agit de la partie standard de M, et les éléments qui ne sont pas dedans sont appelés non-standards.

Tout ceci pourra surprendre le mathématicien : mais ℕ est manifestement (à isomorphisme près) le seul ensemble vérifiant le principe de récurrence, et celui-ci fait partie des axiomes de Peano pourra-t-on m'objecter, donc comment peut-il exister des modèles non-standards ? L'explication est que le principe de récurrence définit ℕ à isomorphisme près si on le comprend comme le principe de récurrence sur toute partie de l'ensemble, ou principe de récurrence du second ordre, mais PA n'énonce pas vraiment ce principe, il énonce un succédané au premier ordre, à savoir le principe de récurrence sur toute partie qui peut se définir par une formule du premier ordre. C'est ce qui explique l'existence de modèles non-standards.

On peut en fait distinguer deux « sources » de modèles non-standards de PA : la première, le théorème de Löwenheim-Skolem (ascendant), assure l'existence de modèles non-standards de PA qui vérifient exactement les mêmes énoncés (arithmétiques du premier ordre !) que le modèle standard : on dit qu'ils lui sont élémentairement équivalents. On peut fabriquer de tels modèles plus ou moins « explicitement », par la technique des ultraproduits. Ces modèles, cependant, ne sont pas très intéressants pour la discussion puisque la logique du premier ordre ne les distingue pas vu qu'ils ont exactement les mêmes énoncés vrais que ℕ. La seconde « source » de modèles non-standards est la combinaison du théorème d'incomplétude de Gödel et du théorème de complétude du même homme : ce dernier assure qu'une théorie consistante a toujours un modèle, ou, de façon équivalente, qu'un énoncé est démontrable si et seulement si il est vrai dans tous les modèles. Par exemple, comme PA ne démontre pas Consis(PA), ceci signifie qu'il existe un modèle de PA dans lequel Consis(PA) est faux (même si, « en fait », il est vrai, c'est-à-dire, vrai dans ℕ, le modèle standard) : il s'agit d'une sorte de monde fictif où l'arithmétique de Peano serait inconsistante. Autrement dit, il existe un ensemble M, vérifiant les axiomes de Peano du premier ordre, et dans lequel on peut trouver un élément qui « code » une démonstration du fait que l'arithmétique de Peano du premier ordre est inconsistante : une démonstration non-standard de l'inconsistance de l'arithmétique. Ceci peut sembler paradoxal, mais cela signifie simplement que cette démonstration n'en est pas une, elle vit dans ce monde fictif M où elle ressemble à une démonstration, elle en vérifie formellement les contraintes, mais sans en être une (pour commencer, elle est « infiniment longue », i.e., de longueur non-standard : ce n'est pas une suite de symboles au sens où on l'entend habituellement, c'est un objet qui fait semblant d'être une suite de symboles).

Notons que si ℕ est une partie de tout modèle M non-standard de PA, ce n'est jamais une partie définissable (par une formule de l'arithmétique du premier ordre), sans quoi le principe de récurrence s'appliquerait pour montrer que c'est tout l'ensemble M.

Passons à ZFC : un modèle de ZFC est, comme on s'en doute, un ensemble M muni d'une relation ∈M qui vérifie les axiomes de ZFC [du premier ordre]. Là les choses sont un chouïa plus compliquées parce que ZFC ne peut pas prouver l'existence d'un tel ensemble (à cause, justement, du théorème d'incomplétude : l'existence d'un modèle de ZFC équivaut à la consistance de ZFC, que ZFC ne prouve pas — du moins s'il est cohérent). Par ailleurs, même dans une théorie plus forte (comme ZFC+IC, qui prouve l'existence d'un modèle de ZFC), il n'existe pas un modèle privilégié de ZFC qu'on pourrait qualifier de standard comme on a qualifié ℕ dans le cas de l'arithmétique. À la place, on va définir des modèles standards, également appelés modèles transitifs de ZFC, c'est-à-dire des modèles M de ZFC qui sont des ensembles transitifs (=tout élément d'un élément de M est un élément de M), munis de la relation ∈ naturelle ; cela revient plus ou moins à imposer que la relation ∈M soit « bien fondée », c'est-à-dire qu'il n'existe pas de suite infinie d'éléments chacun appartenant au précédent, mais surtout, cela implique que le ℕ construit par le modèle M est le ℕ standard. L'existence d'un modèle standard de ZFC est une hypothèse encore plus forte que l'existence d'un modèle de ZFC (mais les deux sont impliquées par l'existence d'un cardinal inaccessible). Et même avec cette hypothèse, il n'y a pas unicité du modèle standard.

Une difficulté est que les ordinaux ne sont jamais achevés : il faut s'imaginer, au moins philosophiquement, que fixer un modèle standard de ZFC revient à arrêter la construction des ordinaux à une certaine hauteur, mais qu'en ce faisant on définit donc un ordinal « omis » par le modèle. Par exemple, en raisonnant dans ZFC+IC, il résulte de l'existence d'un cardinal inaccessible κ celle d'un modèle standard de ZFC, à savoir l'ensemble Vκ des ensembles hériditairement plus petits que κ, qui revient essentiellement à arrêter les ordinaux à κ (et si κ était le plus petit cardinal inaccessible, il n'y a pas de cardinal inaccessible dans le modèle en question). Il n'y a donc pas de sens à chercher un unique modèle standard de ZFC sauf à vouloir en limiter artificiellement la longueur (par exemple en postulant que les cardinaux inaccessibles n'existent pas).

Une autre difficulté est que, même à longueur ordinale fixée, les modèles standards de ZFC peuvent différer par leur « largeur », c'est-à-dire contenir plus ou moins d'ensembles. Le maximum et le minimum possible de la largeur sont, en un certain sens, donnés par la hiérarchie de von Neumann Vα (qui inclut tous les ensembles jusqu'à la profondeur ordinale prescrite) et par la hiérarchie constructible de Gödel Lα (qui n'inclut que les ensembles « absolument nécessaires », ou « calculables » dans une sorte de généralisation monstrueuse de la notion de calculabilité). Il est vrai que — si on suppose l'existence de modèles standards de ZFC — il existe un plus petit modèle standard, mais il ne joue pas le rôle spécial que ℕ a dans le cas de l'arithmétique. (À la limite, ceux qui joueraient le rôle le plus proche de ℕ pour l'arithmétique, ce serait les Vκ avec κ un cardinal au moins inaccessible, mais c'est plus une opinion personnelle qu'un fait mathématique.)

Hiérarchies de formules

Pour résumer les points importants jusqu'ici : si P est un énoncé fixé, dire P est vrai signifie simplement P ; si l'énoncé est variable, en revanche (i.e., s'il s'agit d'un entier naturel codant un énoncé), on n'a donné un sens à P est vrai que lorsque P est arithmétique et, dans ce cas, l'énoncé ainsi formé n'est pas, justement, arithmétique. Il est essentiel qu'il y ait une « augmentation de complexité » sans quoi on pourrait former un énoncé je ne suis pas vrai qui causerait l'effondrement des mathématiques.

On peut néanmoins faire un petit peu mieux que ce que je viens de dire. Pour cela, je dois définir une petite classification de la complexité des formules et énoncés (ensemblistes d'une part, arithmétiques de l'autre) en fonction de la complexité de leur quantificateurs. Plus exactement, ce qui va compter est le nombre d'alternances entre quantificateurs existentiels et universels, et encore, certains quantificateurs dits bornés ne vont pas compter.

Voici une définition précise. On dit qu'un quantificateur dans un énoncé ensembliste (resp. arithmétique) est borné lorsqu'il est de la forme ∀x∈y ou ∃x∈y (resp. ∀x≤y ou ∃x≤y dans le cas arithmétique, avec y un terme) ; une formule dont tous les quantificateurs sont bornés est dite Σ0 ou Π0 ou Δ0 (c'est synonyme). Puis par récurrence sur r, on appelle formule Σr+1 (resp. Πr+1) une formule qui commence par un certain nombre de quantificateurs existentiels (resp. universels) (non bornés, cette fois !) suivis d'une formule Πr (resp. Σr). Lorsqu'on a une formule Σr et une formule Πr qui sont démontrablement équivalentes, on dit parfois aussi (un peu abusivement) qu'il s'agit d'une formule Δr (c'est-à-dire que Δr signifie à la fois Σr et Πr).

Par exemple :

  • ∃y≤x(x=2y) (c'est-à-dire x est pair) est une formule arithmétique Δ0 de la variable libre x ;
  • ∀z∈x(z∈y) (c'est-à-dire x⊆y, soit x est une partie de y) est une formule ensembliste Δ0 des variables libres x et y ;
  • ∀n∀x∀y∀z(x↑n+y↑n=z↑n ⇒ (n≤2 ∨ x=0 ∨ y=0 ∨ z=0)) est un énoncé arithmétique Π1.

(Moyen mnémotechnique : la lettre grecque Σ ou Π indique le quantificateur qui commence la formule : Σ évoque une somme des valeurs de vérité donc un quantificateur existentiel, tandis que Π évoque un produit des valeurs de vérité donc un quantificateur universel. L'indice numérique indique le nombre de blocs de quantificateurs qui alternent, sachant qu'on ne compte pas les quantificateurs bornés — au moins à la fin, mais en fait on peut démontrer des équivalences qui permettent de les éliminer même ailleurs.)

On peut toujours considérer un énoncé Σr ou Πr comme Σr+1 ou Πr+1 (y compris pour l'autre lettre), quitte à ajouter un quantificateur qui ne sert à rien : donc Σr et Πr sont tous deux plus restrictifs que Δr+1, qui signifie lui-même à la fois Σr+1 et Πr+1.

Je souligne qu'on a fait des définitions rigoureusement parallèles dans le cas d'énoncés ensemblistes et dans le cas d'énoncés arithmétiques, mais les hiérarchies ainsi définies sont bien distinctes : un énoncé comme ∀x∀y(x+y=y+x) est un énoncé arithmétique Π1, mais converti en énoncé ensembliste il s'écrit ∀x∈ℕ.∀y∈ℕ.(x+y=y+x) donc tous ses quantificateurs sont bornés et a priori il a l'air d'être Δ0 ; sauf qu'en fait il faut ajouter la définition de ℕ dans l'histoire : il existe une formule Nat(M,+M,×M,↑M) qui est Δ0 comme formule ensembliste et qui est vérifiée si et seulement si (M,+M,×M,↑M)=(ℕ,+,×,↑) (égalité d'ensembles, pas juste isomorphisme !), du coup n'importe quelle formule arithmétique P peut se transformer en une formule ensembliste Δ1 en la réécrivant soit comme ∀N(Nat(N)⇒N⊧P) soit comme ∃N(Nat(N)∧N⊧P) et N⊧P est Δ0 comme je viens de l'expliquer.

On a donc deux hiérarchies de formules, une hiérarchie arithmétique et une hiérarchie ensembliste (ou hiérarchie de Lévy), et d'après le paragraphe précédent, la totalité de la hiérarchie arithmétique est en fait incluse au niveau Δ1 (qui est à peu près le plus bas possible) de la hiérarchie ensembliste.

Pour faire le lien avec d'autres concepts, un ensemble d'entiers naturels peut s'écrire de la forme E={n∈ℕ:P(n)} avec P une formule arithmétique Δ1 si et seulement si E est récursif ; il peut s'écrire sous cette forme avec P une formule Σ1 si et seulement si E est récursivement énumérable ; et il peut s'écrire sous cette forme avec P une formule Δr+1 si et seulement si le degré de Turing de E est le r-ième saut de Turing absolu (i.e., partant de 0).

La formule □P qui dit P est un théorème (que ce soit de PA ou de ZFC ou d'un autre système raisonnable) est, pour sa part, une formule arithmétique Σ1, puisqu'elle énonce le fait qu'il existe une démonstration de P. L'énoncé de Gödel, ou la consistance du système, sont, eux, des énoncés arithmétiques Π1, puisqu'ils énoncent le fait qu'il n'existe pas de démonstration de telle ou telle chose. En fait, énormément de conjectures mathématiques importantes sont arithmétiques Π1 (par exemple, le fait qu'une équation diophantienne quelconque n'ait pas de solution ; ou encore l'hypothèse de Riemann : ce n'est pas complètement évident qu'on peut la réécrire comme un énoncé arithmétique, mais il se trouve même qu'on peut le faire Π1) ; en fait, tout énoncé qui peut se réécrire sous la forme telle machine de Turing ne s'arrêtera jamais (par exemple, une machine qui vérifie successivement que les zéros de la fonction ζ sont sur l'axe critique, ce qui peut se faire même si ce n'est pas évident a priori) est arithmétique Π1.

Mais sinon, quel est l'intérêt de ces notions pour mon propos ? Le fait est qu'on peut définir P est vrai de façon uniforme lorsque le nombre d'alternations de quantificateurs de P est supposé borné :

  • au niveau arithmétique : pour chaque r (explicite et fixé), il existe une formule qui traduit P est un énoncé arithmétique Σr [resp. Πr] vraie (voire : P est une formule arithmétique Σr [resp. Πr] qui est vraie quand on substitue à ses variables les valeurs m1,…,mk), et cette formule est elle-même Σr [resp. Πr] pour r≥1, ou Δ1 si r=0 ;
  • au niveau ensembliste : pour chaque r (explicite et fixé), il existe une formule qui traduit P est un énoncé ensembliste Σr [resp. Πr] vraie (voire : P est une formule Σr [resp. Πr] qui est vraie quand on substitue à ses variables les valeurs m1,…,mk), et cette formule est elle-même Σr [resp. Πr] pour r≥1, ou Δ1 si r=0.

L'idée de la preuve, dans le cas arithmétique, peut être de construire une machine de Turing qui teste la vérité des énoncés Δ0, ce qui est facile puisqu'elles ont des quantificateurs bornés dont il n'y a qu'à énumérer un nombre fini de cas : cette machine de Turing montre que la vérité des énoncés Δ0 est Δ1, et ensuite c'est facile d'ajouter des quantificateurs. Dans le cas ensembliste, pour écrire une formule Δ1 qui reflète la vérité de P un énoncé Δ0 variable, on l'écrit sous la forme il existe un ensemble transitif M tel que M⊧P soit pour tout ensemble transitif M on a M⊧P, ces deux formules étant équivalentes, ce qui permet de dire qu'elles sont Δ1 ; de nouveau, c'est facile d'ajouter des quantificateurs.

On pourrait s'étonner du résultat ci-dessus, et surtout du fait que la formule P est un énoncé Σr [resp. Πr] vraie ait elle-même la complexité Σr [resp. Πr] : après tout, j'ai expliqué qu'il devait y avoir augmentation de la complexité pour ne pas qu'on puisse fabriquer un énoncé je suis faux avec l'astuce de diagonalisation. Où est l'arnaque ? Elle réside simplement dans le fait que la négation d'un énoncé Σr est Πr et vice versa, et la formule qui dit P est un énoncé Σr [resp. Πr] faux est donc, pour sa part, Πr [resp. Σr] ; et même si on cherche à trouver P de classe Δr, on ne s'en sort pas, parce que les formules de vérité Σr et de vérité Πr dont distinctes : il faudra choisir entre les deux, mais on ne tombera pas sur quelque chose de Δr.

Je remarque aussi au passage que ces notions permettent de donner un sens à l'ensemble des formules Σr ensemblistes vraies pour chaque r explicite. Ce qu'on ne peut pas faire, c'est une définition uniforme en r (i.e., pour r une variable), ce qui permettrait de définir l'ensemble des formules ensemblistes vraies — chose qu'on ne peut pas faire en théorie des ensembles. (Dans le même genre d'idées, pour n'importe quel r explicite et fixé, on peut définir arithmétiquement le plus petit entier qui ne peut pas être décrit par une formule Σr de longueur ≤1000000000 — ce nombre étant d'ailleurs vraiment très grand — et il n'y a pas de paradoxe à ce que cette définition tienne en moins d'un milliard de symboles, même une fois formalisée, parce que la définition en question n'est pas Σr ; sauf quand r commence à approcher le milliard, auquel cas la valeur en question stationne.)

Une autre raison pour laquelle la classification par complexité des formules est importante est qu'elle permet d'y voir plus clair dans les systèmes formels PA et ZFC : ceux-ci comportent en effet des schémas d'axiomes, c'est-à-dire une infinité d'axiomes obtenus en remplaçant une certaine « méta-variable » Φ par toutes les formules possibles. Précisément, il s'agit du schéma de récurrence dans le cas de PA et, dans le cas de ZFC, de deux schémas différents, le schéma de compréhension et le schéma de remplacement (ce dernier est plus fort que ce premier, mais il y a toutes sorte de raisons de les considérer néanmoins séparément). On obtient des versions affaiblies des deux systèmes en question en limitant les schémas en question (ou si on veut, dans le cas de ZFC, seulement le schéma de remplacement) aux formules, disons, Σr, pour un r explicite. Par exemple, dans le cas de PA, on a des variantes plus faibles où le schéma de récurrence est limité aux formules Σ0 (dans ce cas précis, il est important de noter que j'ai autorisé l'exponentiation dans les symboles arithmétiques), aux formules Σ1, aux formules Σ2, etc. (on peut montrer, mais ce n'est pas totalement évident, que le schéma de récurrence pour les formules Πr est équivalent à celui sur les formules Σr). Le système obtenu en limitant la récurrence aux formules Σ1 a été particulièrement étudié et c'est en gros le système approprié pour obtenir une théorie satisfaisante de la calculabilité de Church-Turing et pour montrer que les fonctions primitives récursives sont totales (bien définies). Par ailleurs, tous ces systèmes ont la propriété intéressante que (à cause, justement, de la possibilité de définir de façon uniforme la vérité des formules Σr) chacun peut s'écrire avec un nombre fini d'axiomes.

La classification par complexité des formules est aussi très importante dans l'étude aussi bien de l'arithmétique que de la théorie des ensembles, parce que PA et ZFC prouvent des lemmes de réflexion (à ne pas confondre avec les schémas de réflexion introduits plus haut et qui sont certes apparentés mais néanmoins distincts). Sans rentrer trop dans les détails, les lemmes de réflexion prouvés par PA énoncent pour n'importe quel r≥1 explicite, le fait que l'ensemble des énoncés arithmétiques Πr+1 vrais est consistant, et de plus, la preuve de ce lemme n'utilise que la récurrence sur les formules (arithmétiques) Σr ; en particulier, PA, et même PA-avec-récurrence-limitée-à-Σr, démontre la consistance de PA-avec-récurrence-limitée-à-Σr−1 (parce que ce dernier système est un ensemble de formules Πr+1 vraies), et, mieux, PA-avec-récurrence-limitée-à-Σr montre que tout théorème Σr+1 de PA-avec-récurrence-limitée-à-Σr−1 est vrai. Les lemmes de réflexion de ZFC sont tout à fait analogues avec des énoncés ensemblistes à la place des énoncés arithmétiques : ZFC démontre, pour n'importe quel r≥1 explicite, le fait que l'ensemble des énoncés ensemblistes Πr+1 vrais a un modèle (et même un modèle de la forme Vα, ce qui a l'avantage de modéliser automatiquement la totalité du schéma de compréhension), et de plus, la preuve de ce lemme n'utilise qu'une quantité limitée des axiomes de remplacement (j'avoue que je m'embrouille en cherchant à savoir exactement combien ; je crois que c'est démontrable dans Zermelo-avec-schéma-de-collection-pour-les-formules-Σr) ; de nouveau, en particulier, ZFC démontre la consistance et même la correction de ses sous-systèmes tels que Zermelo-avec-schéma-de-collection-pour-les-formules-Σr−1.

Quelle est la morale de toute cette histoire sur les hiérarchies de formules ? Je voudrais surtout faire retenir ceci : si PA et ZFC ne démontrent pas chacun leur propre consistance ou correction (bien sûr, ZFC démontre celle de PA), en revanche chacun de PA et de ZFC démontre la consistance, et même la correction, de n'importe lequel de ses sous-systèmes finis, ou le sous-système où un certain schéma d'axiomes — la récurrence dans le cas de PA et le remplacement dans le cas de ZFC — a été limité aux formules Σr pour un certain r explicite et fixé. La précision que r est fixé est essentielle : parce que si PA (resp. ZFC) démontre, pour chaque r donné, la consistance et même la correction du système PAr (resp. ZFCr) ainsi défini, il ne démontre pas l'affirmation obtenue en mettant ∀r devant. Bref, pour chaque r donné je peux produire une démonstration de l'énoncé en question, mais je ne peux pas en produire pour la quantification universelle sur r (et si on joue au formaliste, on est obligé de reconnaître chacun de ces énoncés mais, bien que le parallélisme des démonstrations soit évident, ne pas pouvoir généraliser). [Cf. aussi cette entrée ultérieure.]

↑Entry #2093 [older|※ permalink|newer] / ↑Entrée #2093 [précédente|※ permalien|suivante] ↑

[Index of all entries / Index de toutes les entrées • Latest entries / Dernières entrées • XML (RSS 1.0) • Recent comments / Commentaires récents]