David Madore's WebLog: Que signifie : P=NP indépendant de ZFC ?

Index of all entries / Index de toutes les entréesXML (RSS 1.0) • Recent comments / Commentaires récents

Entry #1881 [older|newer] / Entrée #1881 [précédente|suivante]:

(vendredi)

Que signifie : P=NP indépendant de ZFC ?

Je vais répondre ici à une question de David Monniaux sur son blog parce que ce n'est pas la première fois que j'entends quelqu'un la poser, ça me fera un lien à fournir pour la prochaine fois :

Qu'est-ce que cela voudrait dire que PNP indépendant des axiomes de la théorie des ensembles ?

(Attention, je vais m'adresser aux gens connaissant un peu de maths. Si vous ne savez pas ce qu'est le problème P=NP, commencez par lire Wikipédia.)

La remarque cruciale à faire, c'est que l'énoncé P=NP est un énoncé Σ2 de l'arithmétique. C'est-à-dire qu'il peut se réécrire sous la forme il existe n [en l'occurrence, codant un algorithme + une borne polynomiale explicite dessus] tel que pour tout k [codant une entrée du problème SAT, disons], <énoncé à quantificateurs bornés dont algorithmiquement testable en temps borné a priori> [en l'occurrence, que le problème codé par k est résolu dans le temps annoncé par l'algorithme n]. (Je discutais de ces choses-là ici par exemple.)

Mais commençons par un cas plus simple, celui d'un énoncé Σ1. Par exemple, la négation de l'hypothèse de Riemann. L'hypothèse de Riemann (HR) peut se mettre sous la forme Π1, en disant que pour tout n, <une certaine inégalité facilement testable sur des fonctions arithmétiques est vérifiée> (du genre σ(n) < exp(γ)·n·log(log(n)) pour tout n≥5041, avec σ la fonction somme des diviseurs et γ la constante d'Euler-Mascheroni ; mais peu importe le détail de l'inégalité n'est vraiment pas passionnant, et d'ailleurs il y en a plein). La négation ¬HR de l'hypothèse de Riemann est, dualement, Σ1 : elle dit qu'il existe n telle que <telle inégalité>.

Si on dit que HR (ou ¬HR, c'est pareil) est indécidable dans ZFC, cela signifie donc deux choses : (1) HR n'est pas réfutable dans ZFC, et (2) HR n'est pas démontrable dans ZFC (i.e., ¬HR n'est pas réfutable). Or la partie (1) implique[#] que HR est vraie. Pourquoi ? Parce que si HR est fausse, il existe un n qui viole l'inégalité, et donc qui la réfute (l'inégalité est quelque chose de trivialement testable). En fait, réciproquement, comme on croit à la véracité de ZFC (ou du moins de ses conséquences arithmétiques), si HR est vraie, elle ne peut pas être réfutable dans ZFC.

Autrement dit, si on prouve l'indécidabilité (1&2) de HR dans ZFC, on prouve au moins sa vérité (l'item (1)), et on prouve des choses en plus (à savoir l'item (2)). Du coup, évidemment, ce n'est pas dans ZFC qu'on a des chances de prouver (1&2) (puisque le (2) contredit précisément le fait qu'on puisse prouver (1), i.e. HR, dans ZFC). C'est donc dans un système plus fort, typiquement quelque chose comme ZFC+<un axiome de grand cardinal> qu'on peut arriver à prouver (1&2). Prouver (1&2) dans le système ZFC+<grand cardinal> revient exactement à (1) prouver HR dans ZFC+<grand cardinal> et (2) prouver qu'on ne pouvait pas se passer d'au moins une forme d'axiome supplémentaire (à tout le moins la consistance de ZFC !).

Généralement, quand j'explique ce genre de choses, les gens prennent un air gêné et demandent ce que vrai veut dire. Je pense que quelqu'un qui commence à demander qu'est-ce que vrai veut dire a un sérieux problème et ferait mieux de faire de la peinture que des mathématiques. La seule chose que je peux faire pour dissiper une source de confusion possible, c'est de souligner que quand on dit un truc comme ¬HR n'est pas démontrable dans ZFC, on est en train de faire un énoncé arithmétique (par ailleurs Π1 : pour tout n, le nombre n ne code pas une démonstration de ¬HR dans ZFC) exactement comme quand on dit HR pour commencer (lui aussi Π1). Donc si on sait ce que vrai veut dire dans un cas, ou qu'on est prêt à l'admettre, on sait ce que ça veut dire dans l'autre cas aussi !

Maintenant, prenons P=NP et l'affirmation qu'il n'est pas décidable dans ZFC. Cela signifie de nouveau (1) qu'il n'est pas réfutable (PNP n'est pas démontrable), et (2) que P=NP n'est pas démontrable. Mais cette fois, les choses ont plus subtiles. On peut distinguer deux cas :

On peut donc imaginer que dans ZFC+<un grand cardinal> quelqu'un arrive à prouver l'indécidabilité (dans ZFC) de P=NP en montrant qu'on est dans le cas (a) (il prouve PNP et il prouve que ZFC ne suffisait pas), ou en montrant qu'on est dans le cas (b) (il prouve P=NP, peut-être en donnant explicitement un algorithme et une borne dessus et en prouvant leur correction dans le système ZFC+<grand cardinal>, puis il prouve que ZFC ne suffisait pas ; mais il pourrait aussi y arriver de façon moins constructive), ou même sans distinguer entre les deux cas (cela paraît hautement invraisemblable, mais ce n'est pas inimaginable).

[#] Pour être parfaitement précis, je devrais dire que je peux prouver dans des systèmes arithmétiques faibles que [l'énoncé arithmétique] HR n'est pas réfutable dans ZFC implique [l'énoncé arithmétique] HR. (Par systèmes arithmétiques faibles, je veux dire que l'arithmétique de Peano est bien plus qu'il n'en faut : l'induction sur les formules Σ1 suffit au moins (cf. Hájek & Pudlák, Metamathematics of First-Order Arithmetic, chapitre I, théorème 4.33), et je suppose que dans ce contexte, il faut beaucoup moins que ça. De même, on peut remplacer ZFC dans ce qui précède par des choses très très très faibles, comme l'arithmétique de Robinson, mais pour le coup c'est assez évident.) En revanche, l'implication dans l'autre sens, HR implique que HR n'est pas réfutable dans ZFC, lui, est un principe de réflexion (fût-il Σ1 et arithmétique) de ZFC, et c'est quelque chose de fort (mais cela découle trivialement de théories comme ZFC+<cardinal inaccessible>). Bref, ce genre d'énoncés qui parlent d'énoncés qui parlent d'énoncés sont souvent assez embrouillés parce qu'il faut bien préciser quelles sont les théories en jeu à chaque niveau (pis que ça : pour une théorie imbriquée, ce qui compte n'est pas seulement quelle théorie est imbriquée mais aussi comment elle est formalisée pour le niveau d'au-dessus).

↑Entry #1881 [older|newer] / ↑Entrée #1881 [précédente|suivante]

Recent entries / Entrées récentesIndex of all entries / Index de toutes les entrées