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 P≠NP 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
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 vrai
veut dire¬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 !
Ajout : Voir cette
longue entrée ultérieure pour toutes sortes de développements sur
la notion de vrai
.
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 (P≠NP 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 :
- (a) Soit P≠NP (i.e., P=NP est faux) : il n'existe pas d'algorithme qui résolve SAT en temps polynomial, mais ce fait-là n'est pas prouvable dans ZFC (sur chaque algorithme putatif donné, il serait toujours possible de trouver une instance du problème qui le met en défaut, mais c'est tout). Rien de plus à dire dans ce cas.
- (b) Soit P=NP est vrai : il existe donc bien un algorithme et qui résout SAT en temps polynomial. On peut expliciter cet algorithme et cette borne (je ne dis pas que la démonstration sera forcément constructive, mais un algorithme est un truc fini, il est en principe possible de l'écrire). Les choses se comprennent alors comme : l'algorithme existe, mais même si un messager des dieux nous le donne (avec sa borne) sur un plateau d'argent, il n'est pas possible de prouver dans ZFC que cet algorithme résoudra toujours le problème dans le temps imparti (on ne peut que constater que sur chaque instance donnée il tourne effectivement en temps imparti et résout le problème). (Il est bien sûr concevable que dans ZFC+<tel grand cardinal> on puisse prouver ce qu'on veut sur l'algorithme.)
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 P≠NP 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]
. (Par HR n'est pas réfutable
dans ZFC
implique [l'énoncé
arithmétique] HRsystè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
, 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).HR n'est pas réfutable
dans ZFC