Projet $P\not=NP$
Je vous ai proposé ici quelques approches vers $P=NP$.
Cependant, j'ai toujours continué à aussi travailler pour le contraire.
Avec ce genre de problème, il s'agit de rester bien ouvert sans être borné.
Peut-être que mon style a pu faire croire le contraire mais ce n'est que de la forme.
Sur le fond, j'ai continué à chercher plus ou moins assidument une preuve de $P\not=NP$.
Voici par exemple une approche que j'avais envoyée à une revue l'année dernière (voir le pdf).
Ces derniers temps, je suis revenu à cette approche et j'ai fait un profond nettoyage dans ces idées.
Je vais vous exposer le résultat dans ce fil...avec mon style "minimaliste" et "constructiviste" et surtout "fainéant".
Pour le moment je laisse regarder celles et ceux qui veulent cette première approche et vous donne la suite un peu plus tard.
Cependant, j'ai toujours continué à aussi travailler pour le contraire.
Avec ce genre de problème, il s'agit de rester bien ouvert sans être borné.
Peut-être que mon style a pu faire croire le contraire mais ce n'est que de la forme.
Sur le fond, j'ai continué à chercher plus ou moins assidument une preuve de $P\not=NP$.
Voici par exemple une approche que j'avais envoyée à une revue l'année dernière (voir le pdf).
Ces derniers temps, je suis revenu à cette approche et j'ai fait un profond nettoyage dans ces idées.
Je vais vous exposer le résultat dans ce fil...avec mon style "minimaliste" et "constructiviste" et surtout "fainéant".
Pour le moment je laisse regarder celles et ceux qui veulent cette première approche et vous donne la suite un peu plus tard.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
d'expliquer, de détailler et de répondre aux questions. J'ai bien dit que je vais "essayer".
Cette "preuve" de $P\not=NP$ se fera :
1. Par l'absurde : Supposons $P=NP$ et on en déduit une contradiction et ceci grâce à....
2. Un argument diagonal "à la manière de Gödel". Une remarque : cet argument diagonal va pouvoir s'appliquer dans le cas de complexité polynomiale mais pas dans le cas de complexité exponentielle. C'est attendu puisque $EXP=NEXP$.
Bon, je me lance :
1. Supposons $P=NP$ alors il existe une constance $c$ et une MTD (Machine de Turing Déterministe) $M$ qui décide l'ensemble des FCP (Formules du Calcul Propositionnel) qui sont satisfiables (ensemble ou problème de décision SAT) en temps $c+n^c$ pour toute formule d'entrée codée par un mot $w$ de taille $n$.
Remarque : l'addition dans $c+n^c$ est un détail pour gérer les mots de petites tailles. On peut l'oublier car la question de départ porte sur la limite. On peut reformuler en supposant que les codes des formules considérées ont une taille $n>n_0$ pour un $n_0$ fixé.
2. On va construire une FCP $F$ qui dit d'elle-même dans son interprétation quelque chose du genre :
"je suis consistante si et seulement si la machine $M$ ne m'accepte pas"
Ainsi :
a) si $F$ est SAT (consistante) alors $M$ ne l'accepte pas alors qu'elle devrait le faire.
b) si $F$ est non SAT (inconsistante, contradictoire) alors $M$ l'accepte alors qu'elle ne devrait pas.
la suite plus tard...en attendant d'éventuelles questions.
J'ai du mal à voir comment ça peut entrer en jeu, et naturellement c'est essentiel (puisque SAT est décidable)
Cette question est pertinente et arrive à propos car elle introduit l'étape suivante qui fera le lien entre les FCP et les MTD.
Je vais le détailler demain. Pour patienter, vous pouvez regarder la construction de S.Cook dans sa preuve que SAT est NP-Complet.
Merci, qu'est-ce que je me suis marré en lisant cette phrase, aah vraiment merci, c'était trop drôle!!!!! Tu nous occuperais bien notre soirée, toi, des fois qu'on s'ennuierait, hein.
Petit rappel.
Supposons que $P=NP$.
Alors il existe deux constantes entières positives $C,N_0$ et une MTD $M$ qui à partir de tout mot $w$ de longueur $n>N_0$ se retrouve dans son état acceptant en au plus $n^C$ étapes de calcul si et seulement si le mot $w$ représente (est le codage d') une FCP consistante (satisfiable).
Sans perte de généralité, on peut supposer que le codage se fait sur un alphabet à deux lettres $0,1$. La machine $M$ est effective. Elle possède $K+1$ états $e_0,e_1,e_2,\dots,e_K$. On peut fixer que $e_0$ est son état initial et $e_1$ son état acceptant. Cette machine travaille sur un "ruban" indexé par les entiers positifs sur lequel est écrit initialement le mot d'entrée $w=w_1w_2\dots w_n$ avec une lettre par case suivi d'une suite infinie de lettres $0$. Notez que cet "infini" n'est pas nécessaire car le calcul est fini et déterminé par $n^C$. La MTD $M$ possède une tête de lecture/écriture qui se déplace d'au plus une case après chaque étape de calcul qui est positionnée initialement sur la case $1$ du ruban. Donc vous voyez bien que la machine va pouvoir aller au maximum en position $n^C$.
Le calcul suit pas à pas les instructions données dans une table qui définit son programme.
Ces instructions sont de ce type : si $M$ est dans l'état $e_i$ et la tête est en position $p$ et la case $p$ contient la lettre $a$ alors y écrire la lettre $b$ et déplacer la tête en $p+d$ avec $d\in\{-1,0,+1\}$ et tel que $p+d\ge 1$ et se mettre dans l'état $e_j$. On fait une table de ces instructions du type $(e_i,a\rightarrow b,d,e_j)$. Notez que ces instructions sont indépendantes de la position de la tête (si ce n'est pour la condition $p+d\ge 1$), bien que l'on aurait pu le faire dans une certaine limite finie. Si une configuration ne se trouve pas dans la table d'instructions alors $M$ se bloque. On peut aussi supposer que si l'état acceptant $e_1$ est atteint alors $M$ rentre dans un état stationnaire $(e_1,a\rightarrow a,0,e_1)$. Si bien que si $w$ est accepté en moins de $n^C$ étapes alors $M$ sera toujours dans l'état $e_1$ à l'étape $n^C$.
Soit $t$ le temps maximal de calcul. Ainsi $t=n^C$. Pour chaque étape $k$ de $0$ à $t$, on décrit complètement la situation de la machine :
$e_i^k\equiv$ la machine est dans l'état $e_i$
$p_h^k\equiv$ la tête de la machine est en position $h$
$z_h^k\equiv$ la case $h$ contient la lettre $0$
ainsi la FCP $M(011)$ exprime les conditions initiales
$$(e_0^0)\wedge(p_1^0)\wedge(z_1^0)\wedge(\lnot z_2^0)\wedge(\lnot z_3^0)\wedge(z_4^0)\dots\wedge(z_t^0)$$
ainsi que toutes les autres conditions sur le calcul.
Par exemple, pour une instruction du type $(e_2,0\rightarrow1,-1,e_3)$ on ajoute toutes les implications suivantes pour $1<h\le t$ et $0\le k\le t$ :
$$(e_2^k\wedge p_h^k\wedge z_h^k)\implies(\lnot z_h^{k+1}\wedge e_3^{k+1}\wedge p_{h-1}^{k+1})$$
ainsi que toutes les conditions d'invariance des autres cases comme
$$(p_7^5\wedge\lnot z_3^5)\implies\lnot z_3^6$$
et celles qui indiquent qu'il y a un seul état actif et une seule position lue comme :
$$\lnot (e_3^5\wedge e_7^5)$$
$$\lnot (p_8^5\wedge p_9^5)$$
Il reste à dire que la machine se trouve à la fin dans son état acceptant avec :
$$(e_1^t)$$
La formule $M(w)$ est la conjonction (ET) de toutes ces conditions.
C'est une formule assez "indigeste" mais sa construction et sa taille restent (par composition) polynomiales en la taille $n$ de $w$ puisque $t=n^C$ l'était.
Petite pause "digestive"...(et ça c'est drôle...non ?)
Il suffit pour cela de remplacer la condition $(e_1^t)$ par $(\lnot e_1^t)$ dans la formule $M(w)$.
On souhaite donc obtenir une FCP $F$ dont la consistance est équivalente à celle de $R(f)$ où $f$ est un codage de $F$.
Avant de voir cela, j'aborde la question de la complexité.
Tous les indices dans ces formules sont représentés en base $2$ dans le codage de la formule.
Ainsi, si $f$ est de taille $N$, le temps de calcul $T$ sur $f$ est $N^C$ et la condition $(\lnot e_1^T)$ est codée par un mot binaire de taille $$O(log_2(T))=O(C.log_2(N))=O(log_2(N))$$
ce qui est plus petit que la taille $N$ du mot $f$ pour $N$ assez grand. Heureusement afin que $f$ puisse intégrer cette condition auto-référentielle.
Petit rappel de notation : $O(f(n))$ signifie <<à une forme linéaire près>> comme $a+b.f(n)$ où $a,b$ sont des constantes.
Par contre, si la complexité de $M$ est exponentielle comme en $2^N$, la taille du codage de la condition $(\lnot e_1^T)$ serait de l'ordre de $N$ voire plus.
Donc, cette condition auto-référentielle ne serait pas exprimable par ce principe.
Du moins, cette condition prendrait plus de place que la formule elle-même.
(***) On voit ainsi que la complexité polynomiale <<n'empêche pas>> l'auto-référence alors que la complexité exponentielle l'empêche.
Ce principe de preuve ne s'étend donc pas à une preuve de $EXP\not=NEXP$. Heureusement puisque c'est faux.
Pour compléter la "preuve", il reste (au moins) à convertir le <<n'empêche pas>> du cas polynomial en <<permet>>.
J'ai lu la phrase peu de temps d'aller au dodo, et ça donnait l'effet d'un devoir du soir à faire. C'est un ressenti immédiat. Attention, trouver drôle ne veut pas dire qu'on se moque, j'ai parfois l'impression que les gens peuvent se vexer, ce n'était nullement mon but.
C'est un détail insignifiant...tout comme la réaction de fatigue de CC. Pas de soucis.
"Je vous ai proposé ici quelques approches vers P=NP.
Cependant, j'ai toujours continué à aussi travailler pour le contraire."
ça me rappelle la manière dont on décrit de manière informelle un algorithme de décidabilité pour les théories complètes : le jour on cherche une preuve de $\varphi$, la nuit une de $\neg\varphi$. Si l'une des deux est démontrable, on est sûr de s'arrêter un jour.
En fait, c'est intéressant dans des cadres où on a des critères "calculatoires" différents pour $\varphi$ et $\neg\varphi$, car dans ce cas-là on peut faire le calcul "qui cherche $\varphi$" le jour, et celui pour $\neg\varphi$ la nuit (j'avais vu quelqu'un décrire cette stratégie algorithmique pour la question de la décidabilité de l'existence d'une solution aux équations diophantiennes dans $\Q$, modulo une conjecture de Grothendieck)
C'est très pertinent au contraire...autant utiliser le tiers exclus quand on en dispose. De plus, dans la démarche de recherche, une voie peut donner du relief à l'autre ou même l'éclairer. Et si elle conduit à une impasse avérée, cela prouve aussi l'autre.
C'est un peu l'histoire d'une grenouille qui veut avaler un bœuf. Une histoire de taille et de volume.
On va plutôt faire avaler à la grenouille l'ADN du bœuf qui est un codage suffisant pour dire qu'elle a avalé l'équivalent de ce bœuf.
Ce sera plutôt un nombre suffisant de cellules du bœuf pour garantir qu'il s'agit bien de ce bœuf.
De plus, pour compliquer l'histoire, ce bœuf est en fait le résultat de la transformation d'un clone de cette grenouille par une sorcière.
La grenouille c'est la formule $F$, le bœuf c'est le codage de $F$, la sorcière c'est l'hypothétique machine de Turing $M$.
Et on veut montrer que cette sorcière n'existe pas....pour une <<happy end>>.
On procède par complétion.
On va intégrer à la formule $F$ des bribes du calcul de $M$ sur son codage $f$.
Pour une FCP $P$ on notera $<P>$ son codage pour fonctionner sur $M$. On aura donc $f=<F>$.
On part du mot $f$ qui code la FCP $(\lnot e_1^T)$ avec un $T$ grand, disons suffisamment grand. Avec la notation on a $f=<\lnot e_1^T>$.
Cela code une formule qui est pour l'instant "insignifiante", dénuée de sémantique. On va lui donner du sens par complétion.
On va rajouter ce qui est suffisant pour qu'elle signifie que l'état n'est pas acceptant à la fin du calcul sur le code de cette formule.
Le mot $f$ est une suite finie $f_1....f_k$ de lettres $0,1$ avec $k$ grosso modo de l'ordre de $22+log_2(T)$ (ça devrait suffire largement).
On effectue le calcul de $M$ sur $f$ et on ajoutera (à la fin du mot $f$) et de "temps en temps" des éléments concernant la configuration de $M$.
On peut commencer par rajouter $<e_0^0>$ et quelques autres éléments à propos du mot initial $f$.
On continue le calcul est on rajoute encore des éléments de la configuration comme par exemple l'état actif à un instant $k$ comme $<e_i^k>$.
Au lieu que ce soit des hypothèses comme dans les règles de transition du calcul, elles deviennent des faits avérés puisqu'on le constate en effectuant le calcul sur ce mot. Cette méthode de complétion n'est pas rigide mais elle a des contraintes (###).
Le but est de donner du sens à la formule et surtout au mot initial $<\lnot e_1^T>$.
Il faut cependant faire attention lorsque l'on rajoute des éléments (des mots à la fin du mot $f$) que la MTD $M$ n'a pas encore été "voir" ces positions de lettres dans le mot initial afin que la situation que l'on décrit soit bien indépendante de ce que l'on va rajouter à la fin du code $f$.
Je détaillerai ces points (###) par la suite.
Au final, on obtient un codage d'une FCP qui dit qu'au bout d'un certain temps le calcul sur le mot qui code <<au bout d'un temps certain $T$ le calcul est achevé>> est terminé. Puisque la formule de départ dit que l'état final n'est pas acceptant, nous avons obtenu notre formule $F$ qui mène à la contradiction voulue. Précisons cela :
a) Si au final la MTD $M$ arrive dans son état acceptant $e_1$ alors on devrait aussi avoir par "stabilité" de cet état le fait que $e_1^T$ est vrai. Puisque la formule contient aussi la condition que $\lnot e_1^T$ doit être vrai, alors $F$ est inconsistante mais pourtant $M$ arrive sur son état acceptant et l'accepte. Contradiction : la machine $M$ n'est pas correcte.
b) Si par contre, la MTD $M$ termine son calcul dans un état différent de $e_1$ cela signifie que $\lnot e_1^T$ est vrai et la formule $F$ est consistante puisqu'elle décrit des bribes de ce qu'il se passe effectivement et sans contradiction. Mais $F$ n'est pas acceptée. Contradiction par incomplétude.
Voilà l'idée. C'est aussi "tordu" que la construction de Gödel, mais pas beaucoup plus et peut-être moins. Il s'agit de se débrouiller sans les entiers et l'axiomatique de Peano mais simplement avec des $0,1$ et des FCP, ce qui est à peu de choses près pareil.
C'est clair que tout ceci doit être détaillé...c'est la base du projet. Mais cela semble réaliste et réalisable.
Nous avons vu que pour distinguer la classe $EXP$ de la classe $NEXP$ cela n'était en revanche pas possible.
Et cette impossibilité est plutôt un bon signe puisque, je le répète, $EXP=NEXP$.
Là on a essayé de donner des éléments afin de prouver $P\not=NP$
Il y a peut-être moyen de le faire autrement, plus directement, plus logiquement avec des substitutions à la Gödel et une FCP $S(F,G)$ qui dit que
soit $F$ est ce que l'on cherche
soit $G$ est ce que l'on cherche
soit $S(F,G)$ est ce que l'on cherche
J'y pense mais ce n'est pas évident conceptuellement et je ne suis pour l'instant pas trop à l'aise pour le formaliser.
J'attends vos questions et vos remarques. Merci à celles et ceux qui ont eu le courage de lire tout ça.
Pour montrer $P\not=NP$, on va exhiber un langage qui est dans $NP$ mais qui n'est pas dans $P$.
Ce langage $L$ est une extension des FCP satisfiables. On ajoute de nouvelles sortes de conditions qui portent sur le fonctionnement même de la Machine de Turing qui est supposée décider $L$. En particulier on peut demander si à un instant $t$, la machine est dans un état acceptant ou non.
Une formule est dans $L$ si et seulement si il existe un calcul de la machine qui prouve sa non contradiction et son adéquation avec les conditions de calcul (au bout de $N^C$ étapes). Une sorte de certification qui se fait par une Machine Universelle qui simule la machine $M$ donnée et vérifie que les conditions portant sur le calcul sont vérifiées.
Maintenant, on peut ajouter à une FCP la condition $<\lnot accepte(N^C)>$ qui dit qu'il existe un calcul de la machine qui n'accepte pas la formule à la fin du calcul.
Pour une Machine de Turing Déterministe et une formule non contradictoire,
si la formule est acceptée, c'est qu'elle ne l'est pas
si formule n'est pas acceptée, elle devrait l'être pourtant.
Mais on peut très bien imaginer une Machine de Turing non Déterministe,
qui aura les deux types de calculs : un acceptant et un autre non acceptant.
Ainsi il existe bien un calcul non acceptant et la formule est acceptée.
Encore une fois, cela marche pour du temps polynomial puisque $N^C$ se code par un mot de taille $C.log_2(N)<N$ pour $N$ assez grand.
Je n'ai pas suivi ce fil, mais il semblerait que Rupert McCallum t'ait devancé :-D
(bon, ce n'est qu'un preprint sur arXiv, donc ce n'est pas la fin de l'histoire - il avait déjà fait une annonce grandiloquente il y a quelques années)
(mais c'est amusant)
Merci pour cette information...je n'étais pas au courant. Vais voir cela….(je cherche)….et trouve cela <<Proving $P\not=NP$ in first-order PA>>
C'est de ce preprint dont tu parles ?
C'est une approche pour le moins différente de la tienne, donc ne te décourage pas pour autant !
(d'autant plus qu'apparemment, quelqu'un a déjà repéré un point d'ombre)
Mais si c'est convainquant, tant mieux. Peut-être est-ce "simple" et "limpide" pour des théoriciens des ensembles.
Rien que l'abstract est un modèle du genre pour faire une sélection parmi les lecteurs.
Par ailleurs, j'ai en général toujours des méfiances sur les preuves "à texte".
En 10 lignes de texte on peut convaincre quelqu'un de tout.
Alors, il va falloir attendre le chant du "Coq".
Mais pourquoi pas...ce serait bien.
Passer à autre chose.
Enfin !
En ce qui concerne $P = NP$ je ne suis pas qualifié pour commenter ces tentatives de preuves (ou de réfutations).
C'est d'ailleurs un peu bizarre, parce qu'on a tous plus ou moins (chez les logiciens épris de procédés diagonaux) fait le projet un jour de rédiger l'argument*** et procrastiné, donc si un quidam débarque et rafle le million de dollar parce qu'il a juste rédigé le truc, ça donnera une bonne leçon aux matheux faignants.
*** avec la conviction qu'à un moment dnné "quelque chose" ne marcherait pas, donc pas la peine de le faire et de bousiller 100H, je précise quand-même :-D parce que si on nous accuse de "pure flemme" ce serait injuste
** et, déjà riche et protégé le laisse à un jeune.
On suppose $P=NP$. Donc, qu'une machine déterministe $M$ décide le problème SAT en temps $N^C$ pour $N$ assez grand.
Il s'agit de trouver une instance $F$ de taille $N$ du problème SAT qui dit : <<je ne suis pas acceptée par $M$>>
Cela veut dire : $F$ est consistante (dans SAT) si et seulement si $M$ n'accepte pas $F$.
Il s'agit alors d'exprimer dans $F$ la non acceptation de $F$ par $M$
Une version totalement syntaxique coderait dans $F$ le calcul complet (et non acceptant) de $M$ sur $F$.
Les étapes de calcul sont exprimables mais il y a le problème de la taille de ce codage complet qui serait à priori plus grand que la formule $F$.
On peut toutefois coder le fait que le temps de calcul est d'au plus $N^C$ et que l'état final n'est pas acceptant :
c'est grosso modo codable en $C.log_2(N)$ qui est plus petit que $N$ pour $N$ assez grand.
On peut coder encore d'autres éléments de ce calcul mais pas la totalité.
Cependant, le calcul est déterministe et donc unique et uniquement et invariablement déterminé par $F$.
Ce qui n'est pas le cas pour les calculs non déterministes.
On peut donc penser à introduire de la sémantique et à la limite ne coder que le fait que l'état final n'est pas acceptant.
La sémantique portant sur la nature et l'interprétation des calculs sera alors définie par une variante de la machine $M$, une machine qui simule le fonctionnement de $M$ et qui vérifie que les éventuelles configurations de calcul exprimées dans $F$ sont valides, c'est à dire consistantes avec la réalité du calcul effectué. Du coup, il ne faut plus grand chose pour obtenir un argument diagonal et la taille $N$ de $F$ est suffisante.
Les ingrédients sont les suivants :
a) coder le temps de calcul : c'est possible pour du polynomial...mais pas pour du temps exponentiel.
b) dire que l'état final n'est pas acceptant : c'est par la négation logique qui est à priori dans le langage.
c) simuler une machine de Turing donnée : c'est la machine universelle $U$ qui simule la machine $M$
d) écrire sur un autre ruban le codage de chaque étape de calcul de $M$ et vérifier que $F$ n'est pas en contradiction avec l'une d'elles.
e) cette simulation donne une variante étendue $M^+$ de $M$ qui décide (toujours en temps polynomial) une extension $SAT^+$ de $SAT$ qui intègre de nouvelles formes sémantiques de clauses portant sur le calcul lui-même. Ce problème $SAT^+$ reste dans $NP$ mais n'est pas dans $P$.
voilà le résumé.
Je ne vois pas à quel moment ce qu'il fait ne pourrait pas être transposé en une preuve de $EXP\not=NEXP$
Il me semble que tout ce qu'il fait est transposable de son $p(n)=C.n^{\alpha}$ à du $p(n)=\alpha^n$.
Mais dans ce cas, il y a comme un hic puisque $EXP=NEXP$.
C'est un "filtre" que j'applique à mes réflexions quand je suis dans le mode <$P\not=NP$>.
Quand je suis dans le mode <$P=NP$>, c'est plutôt un booster.
Il utilise explicitement une fonction polynomiale inventée par Woodin dans "les tours de Hanoi" et ses récent travaux sur $V=L_{Ultimate}$ qui entre en conflit explicite avec P=NP.
Ca ne veut pas dire qu'il ne s'est pas trompé (son argumentation fait à peine 3-4 pages si on enlève ses efforts didactiques, et mon anglais m'empêche d'évaluer), mais il ne s'est en tout cas certainement pas trompé à ce niveau-là. D'ailleurs, son argument ne marche pour aucune partie non précisée $A$ telle que $P(A)=NP(A)$. Les fonctions de croissance rapide de Woodin ne semblent absolument pas avoir leur équivalent avec des $A$-oracles.
L'outil est surprenant parce que Woodin a le "chic" pour produire des énoncés $\exists \forall$ qu'on n'envisage pas (on n'envisage même pas qu'ils sont faux, on ne les envisage pas du tout), comme par exemple le fait que si $HC$ est vraie alors la théorie de $\R$ jusqu'au niveau de $HC$ incluse est figée, autrement dit la valeur de vérité de n'importe quel énoncé de complexité égale à inférieure à l'énoncé $HC$ est constante (dans tout modèle bien fondé de ZF, ou en tout cas, dans toute extension générique). Bon bin personne ne le nie, mais qui aurait eu envie de "croire" à ce genre de chose saugrenue?
Idem: un problème ouvert important est de savoir si $ZF+CD+j:V\to V$ est contradictoire, même sans l'axiome du choix?
Et bien selon Woodin, oui elle l'est contradictoire, et il laisse un jeunot se faire un nom en le prouvant, et il dit qu'il veut bien "donner des conseils" que la preuve est très longue (même si elle ne fait que retirer petit à petit la "graisse-choix"). Il bénéficie d'une telle crédibilité que c'est, il me semble "à peu près" tenu pour "acquis" (alors que si un jeunot ne sort pas le papier explicite, il n'y aura jamais de preuve publiée).
De même son revirement et son délire avec son $L_{ultimate}$ (qui, je crois), entraine HC, ne doit pas leurrer. Il y a bien longtemps que Woodin ne "travaille pas" avec l'idée simpliste d'être platonicien. Il dit que "c'est bien de faire comme si on l'était" et en ce sens, je ne sais pourquoi, il défend HC depuis récemment, mais il faut garder à l'esprit qu'on dispose de plein de modèles où non(HC) et qu'on ne vit plus dans "un seul modèle". Pour le dire autrement, ce "HC" du $L_{ultimate}$ n'est pas un rejet du café philo des gens contre HC.
En résumé, si ce McCallum que je ne connais pas du tout (j'ignore totalement son pedigree) prétend aller sur ce terrain et s'il n'a pas le gout de se ridiculiser pour le plaisir, c'est qu'il doit être relatviement sérieux. Sinon, il aurait évité de parler de Woodin, il se serait attribué la trouvaille, et aurait maquillé son texte en 40 pages imbitables.
Là, au contraire, il "signale" un argument diagonal dont les experts ne vont faire qu'une bouchée en quelques jours et sait qu'il aura une réponse rapide (peut-être ralentie par confinement et diversions actuelles mais bon). Et crois-moi, je ne sais s'il est jeune ou vieux (son type d'idée fait assez jeune), mais il vaudrait meieux que son erreur soit subtil, sinon, il perdra assez nettement en crédibilité scientifique.
voilà des raisons d'espérer, après je ne peux pas en dire plus, de moins point de vue personnel, à moi seul, sans engager presonne, je pense effectivement que ce genre d'argument peut marcher, que c'est pénible à rédiger et qu'on remet au lendemain, ce qui ne garantit en rien qu'il marche.
Tes arguments à toi me paraissent au contraire trop concrets pour pouvoir marcher. C'est un peu comme si tu essayais de prouver la consistance de Peano dans Peano. Pour prouver $P\neq NP$, il faut "rendre" les grands nombres infinis et gérer ça, c'est chiant et platonicien, c'est à dire qu'il "faudra croire" même une fois prouvé à la fixité ABSOLUE d'énoncé arithmétique de complexité $\forall \exists \forall \exists$, puisque $P=NP$ est de complexité $\exists \forall$.
Comme je l'ai souvent dit, on a déjà une preuve de $P\neq NP$ puisque l'énoncé "il existe une formule qui casse l'algo" NE PEUT PAS être prouvé faux dans une théorie faible (qui ne peut pas deviner par elle-même que $2^{BigNombre}$ est fini, donc ne peut se permettre, sous peine de contradiction de prétendre "tout y voir".
Mais ça, ça relève de la production d'axiomes, ce n'est pas une preuve. Les preuves admises dans la communauté sont celles où cet (ce genre) argument sera transformé en preuve formelle dans ZF ou autre. Autrement dit, c'est un "concours d'expressivité" que se livrent les jeunes qui s'attaquent à ce problème. Aucune astuce calculatoire ne peut marcher (je saurais comment la transformer en une preuve de $P=NP$ si on m'en présentait une).
Il a été posté le 19 mai. Il a l'air un peu précipité (normal s'il veut prendre date). La bibliographie "Hanoi" ne marche pas (enfin je n'ai pas cherché longtemps non plus). Quand je googleise le gars, je n'obtiens rien (à part une vague annonce de recherche de post-doc).
Ca ne signifie rien, j'ai connu des jeunes démarrer comme ça (en TDE,même la plupart, vu l'osrtacisme des crédits), mais l'anglais "littéraire" du début à la fin de l'article me rend vraiment impossible de vérifier grand chose.
Certes, il n'y aura pas de "références bétons" au génial Woodin mais du constructif basique.
L'objectif : exhiber un langage $L$ qui est dans $NP$ mais pas dans $P$.
Pour cela, je pense pouvoir formaliser l'avantage d'une machine non déterministe sur une autre déterministe afin de contrer un paradoxe.
Avec le non déterminisme, on peut avoir un calcul qui est acceptant et un autre calcul qui est réfutant.
Et la question de départ est bien existentielle et non universelle :
étant donnée $F$, $\exists$ calcul tel que $Prop(F)$ ?
Ainsi, si $F\in L$ si et seulement si la machine $M$ qui décide $L$ peut la rejeter (càd : il existe un calcul non acceptant) alors
a) une machine déterministe tombe dans un paradoxe car elle n'a qu'un seul calcul possible.
b) mais une machine non déterministe peut accepter la formule si elle possède aussi un calcul qui la rejette.
C'est une réponse du genre : <<$F$ est dans le langage $L$ puisque j'ai aussi un moyen de dire qu'elle n'y est pas>>
Le paradoxe est résolu
Voici le truc rédigé ce matin.
Ce n'est vraiment pas mon style de mettre des hiérarchies ou de construire des idoles, n'importe qui peut en témoigner sur le forum. La partie Woodinienne, je l'évoque car c'est un mathématicien assumant un platonisme extrême jusqu'au bout des ongles et qui a mis les mains "dans le cambouis" en construisant des choses auxquelles on ne pense pas.
Je n'ai aucun idée de la valeur de l'argument de Mc Callum (bien trop informel et anglais littéraire pour moi qui ne parle pas anglais), mais je peux témoigner ces échanges que j'ai ai hier soir tard avec Anatole: il pensait que cet argument ne marche pas parce qu'il y voyait des erreurs que font habituellement les débutants. Par exemple, il a cru que MC affirmant que $n,p \mapsto \phi_n(p)$ est récursivement énumérable et tout un tas de choses comme ça, qui illustrnent que quand tu reprends une suite construite "essentiellement" par Woodin, si tu t'attends à des choses habituelles, tu fais vite des procès d'intention.
Le génie n'est pas u nsujet ici, il s'agit de spécialités à l'intérieur de spécialités. Tout monde "sent bien" qu'il peut exister des preuves où on construit des suites bizarres d'énoncé de ZF (sans en préciser aucun explicitement puisqu'on ne peut pas) à partir de l'ensemble vérité de l'univers, etc, en itérant, mais peu de gens à part Woodin "ont eu la patience dans leur vie de le faire réellement"
C'est une spécialité, comme celle de Harvey Friedman, resté seul, s'est spécialisé dans le fait de construire des équivalences entre énoncé infinitistes profonds et phénomènes combinatoires dans IN. Il y a passé sa vie, ce sont des choses, quand on commence on les emmène dans la tombe, on ne peut pas "en même temps" faire du ski ou de la politique par exemple.
J'ai principalement défendu l'idée d'une potentielle crédibilité de MCallum à cause de ces phénomènes. Il aurait pu ne pas en parler et s'attribuer le truc (en même temps, s'il y a une erreur, il se cherche peut-être une excuse :-D ) L'avenir dira.
J'ai adoré le papier de Harvey Friedman sur les "long finite sequences"....une petite définition toute simple et anodine qui aboutit à des nombres finis et assez gigantesques (pour les petits comme moi).
Sa preuve d'incomplétude avec sa formule qui dit qu'elle n'est pas prouvable dans une théorie donnée suffisamment riche est un modèle du genre que j'admire et qui m'inspire depuis l'adolescence. C'est très constructif sa fonction $\beta$...et c'est pas béta du tout là.
Tu trouves que c'est non constructif ? Je n'ai pas le bon vocabulaire alors.
C'est pas pour être publié mais pour être présenté.
Laisser la place à la discussion.
Sans aucune prétention.
Merci bien.
Article sur Brouwer via pt fixe LC
on a l'impression qu'il est venu sur le forum (c'est un canadien parlant français) et a décidé de répondre à certaines des questions posées. Tant mieux pour moi, mais la barrière de l'anglais...
Il va peut-être même finir par aussi regarder ce que je fais.
Mais va-t-il comprendre mon anglais élaboré ?
Fichue barrière du langage !
;-)
On sait juste que $P=NP\implies EXP=NEXP$.
Dans ce que je propose là, on se place juste en dessous de la classe $EXP$.
Mais c'est aussi plus intéressant de travailler sur des questions formelles ouvertes.
Voici la version du jour soumise à arXiv.
Bon, je lirai, mais le choix anglais je trouve ça triste pour un français.
Ma thèse faisait au départ 2 pages avec aucun mot de français...que des notations.
Dehornoy a galéré pour me pousser à développer et à <<faire des maths pour les gens>> et en faire plus de 100 pages.
Sinon, j'ai pensé à ta remarque sur $PSPACE=NPSPACE$.
Je devrais en effet le dire dans la note (en espérant ne pas devoir dépasser ma limite d'une page...lol)
C'est implicite mais pas clair. Je vais clarifier ainsi :
a) on montre pour une classe $C$ de fonctions de temps que $DETC\not=NDETC$
b) cette classe $C$ est en dessous de $EXP$
c) cette classe $C$ contient les polynomiales de $P$
d) juste en dessous de $EXP$ il y a $PSPACE$ mais elle ne vérifie pas le point a) puisque $PSPACE=NPSPACE$.
e) et juste en dessous de $PSPACE$ il y a $P$
C'est donc que $C=P$.
C'est quand même dans un format plus standard et peut-être plus lisible...je n'arrive pas à juger...alors jugez-moi.
Merci et bonne nuit.
@Christophe : et non, ce n'est pas une injonction pour que tu lises cela avant de te coucher ;-)
Quelques corrections effectuées.
Ma première réaction, à chaud, a été d'ordre psychologique : penser que je suis "black-listé" ou peut-être le site sigle (www.sigle.space)
Ma deuxième réaction, à froid, a été plus raisonnable : penser que le papier est mauvais, incomplet, mal formulé et mal expliqué.
Je me suis donc posé des questions et elles me semblent aujourd'hui pertinentes. Je vous les présente avant de reformuler le papier.
La problématique est conceptuelle. J'ai une vision des Machines de Turing conventionnelle, terre à terre et plus proche des ordinateurs.
C'était implicite dans mes travaux sur ce sujet car je n'arrivais pas à le rendre explicite.
Désormais, c'est plus clair et je pense être en mesure de le formaliser.
Une Machine de Turing (MT) $M$ travaillant sur un mot $w$ est un programme défini. Ce programme est effectué par quoi ?
Par la définition ? Par nous ? Par les mathématiques ? Par Platon dans le monde des mathématiques ?
C'est une question qui semble bête mais qui peut devenir essentielle et Turing devait y penser.
Il en est alors venu à la notion de Machine Universelle.
Comme dans nos ordinateurs, il y a un processeur qui exécute les programmes écrits dans sa mémoire sur des données elles aussi écrites dans sa mémoire. Cette notion conceptuelle me semble essentielle pour appréhender des questions de complexité comme $P\not=NP$.
Alors voici, je formalise.
Etant donné le code $<M>$ d'une MT travaillant sur un mot $w$ et le code $<C>$ d'une autre MT calculant une fonction de complexité en temps comme par exemple $n^k$ ou $2^n$ ou $log(n)$ ou $2^{n^k}$....la bonne façon de poser le problème est de considérer comme entrée un triplet $<M,w,C>$ et cette entrée sera fournie au processeur, à Platon, à nous, à la définition...bref, à une Machine de Turing Universelle.
Avec ceci, tout devient plus clair, universel et uniforme et on peut sortir de fichues boucles conceptuelles assez perturbantes et même chiantes quand on aborde des questions comme celle de comparer $P$ à $NP$.
Dans ce que j'ai écrit (et qui a été rejeté), le problème c'est que la Machine Universelle, utilisée pour montrer que $L\in NP$, tourne sur une donnée paramétrée par une fonction de temps polynomiale $n^k$ pour la machine simulée $M$. Mais la variable $k$ n'est pas une constante pour la Machine Universelle mais seulement une constante pour la MT $M$ qu'elle simule. Ainsi, bien que la simulation puisse se faire en $n^{k}$ étapes de simulation, cette fonction n'est pas une "vraie" fonction polynomiale. Je me suis heurté à cela pendant longtemps et ma définition de la classe $Q$ devait y remédier. Ce n'était pas assez clair. Je vais donc tout reformuler dans un cadre plus général en parlant de "complexité effective", celle des calculs effectués par "quelque chose" : la définition, Platon, nous, un ordinateur...bref, une Machine de Turing Universelle.
Est-ce que cette clarification est claire ? Pas sûr...des idées rédigées au réveil à 5h du matin ont encore la diffuse empreinte de l'inconscient.
C'était pour mettre une touche "romanesque" à ma nouvelle approche qui me semble plus sémantique, conceptuelle, voire complète.
Cependant, il est factuel et vérifiable que mon site www.sigle.space a reçu des visites depuis arXiv Cornell University New York.
Je vais rédiger ces idées (peut-être même en français pour te faire plaisir, mais je ne sais plus faire les accents en Tex)
(oui je fais du Tex pas du LaTex)
\catcode`^^a9=13 \def ^^a9{\'e}
\catcode`^^a8=13 \def ^^a8{\`e}
\catcode`^^a7=13 \def ^^a7{\c{c}}
\catcode`^^a0=13 \def ^^a0{\`a}
\catcode`^^aa=13 \def ^^aa{\^e}
\catcode`^^ab=13 \def ^^ab{\e}
\catcode`^^ae=13 \def ^^ae{\^ \i}
\catcode`^^af=13 \def ^^af{\ \i}
\catcode`^^a2=13 \def ^^a2{\^a}
\catcode`^^a4=13 \def ^^a4{\a}
\catcode`^^b4=13 \def ^^b4{\^o}
\catcode`^^b6=13 \def ^^b6{\o}
\catcode`^^bb=13 \def ^^bb{\^u}
\catcode`^^bc=13 \def ^^bc{\u}
\catcode`^^b9=13 \def ^^b9{\`u}
j'y pige rien mais ça marche.
Voici le début rédigé hier soir.
voici la refonte du début et la suite...il faut encore travailler sur la preuve car j'ai changé des définitions en cours de route...mais le principe est là.
Il faut sortir des Machines de Turing et des classes de complexité pour pouvoir en "parler".
Je vais méditer là dessus et peut-être trouver que c'est foireux ou alors trouver comment rendre cela plus clair.
Merci de me donner vos avis...même si ce sont des critiques cinglantes.
Bonne soirée
Comme en communication politique voici les "éléments de langage" pour expliquer la "preuve".
Pas comme en politique, on peut en discuter et modifier.
Est-ce que cela peut inspirer les logiciens puristes ?