Linéarisation de la logique

Le problème aussi en montant (sans procès d'intention) c'est que tu vérifies ça sur ordi pour des config qui ne peuvent plus servir de contre-exemple car trop petites et, idem sur le forum, on "subit" tes conjectures, tout en sachant que tout contre-exemple sera "gros".

Evidemment, je me doute que tu ne montes pas pour ça, mais ça a cette conséquence. Tu disais que tu avais longtemps cherché à prouver $P\neq NP$ et que la volte-face est récente, mais te rappelles-tu de la littérature que tu as lue dessus? Il y a pas mal d'articles (je ne les ai que survolés) qui "racontent" la difficulté de trouver un algo attestant de $P=NP$ sans pour autant arriver à prouver son inexistence. De plus la calculabilité souffre de pas mal de "mal-formalisations", ie les gens se contentent de "se comprendre". Sauf que c'est assez piégeux.

Par exemple, on réduit facilement SAT à 3SAT et facilement 3SAT à 3colorgraf et 3 colorgraf à ton profi du présent fil via les ensembles :

$\{(s,1); (s,2); (s,3)\}$ pour chaque sommet $s$ et $\{\infty; (s,i), (u,i)\}$ pour chaque arête $(s,u)$.

Mais tu as des tas d'autres NP-complets qui sont "exotiques". L'un des meilleurs est l'ensemble des théorèmes linéaires écrits avec une seule lettre $X$ et le signe $\to$ (ou plus traditionnellement $\multimap$).

Il est aussi facile de voir (pas avec une seule lettre bien entendu, du coup) que l'ensemble des théorèmes affines est NP-complet.

Si tes méthodes marchaient, en les traduisant sur "ces deux problèmes positifs (où on ne cherche pas un "satisfaire", mais à "prouver") tu aurais probablement un contre-exemple immédiats, dans la mesure où on se rend "mieux" compte, à partir d'un algo simple et polynomial qui prétend dire si un énoncé est un théorème linéaire (ou affine avec plusieurs lettres) pourquoi il va échouer.

Je ne sais même pas (en tout cas, il n'en existe aucune de célèbre) s'il existe une logique propositionnelle $L$ qui est polynomiale (ie l'ensemble de ses théorèmes) avec $Lineaire\subset L\subset Classique$, alors que c'est un problème BIEN PLUS LIBRE ET FACILE à regarder et en cas de réponse non, tu as évidemment une preuve de $P\neq NP$, or ça correspond à un théorème que j'ai prouvé que quand on cherche à prouver un truc, il faut chercher à prouver une "version débile" beaucoup plus forte.

Là on a tout un espace entre la logique la plus faible connue qui est NP-complète et celle la plus forte qui est coNP. Peut-on passer par $P$ où le fait d'être une logique est-il rédhibitoire?

Etre une logique veut juste dire: être stable par modus ponens et permutation de variables, avec de plus que les théorèmes passent au cas particulier, ie un théorème en reste un quand on remplace $x$ par $z$ et $y$ par $z$ (qui sont des variables).

Ola non non non ne t'inquiète pas ce n'est pas du tout péjoratif d'ailleurs j'ai mis les guillemets. Je cherchais un mot court et ne l'ai pas trouvé mais je voulais juste exprimer ta vitesse de production de documents très spécialisés comparée aux temps de réaction du forum pourtant habituellement réactif mais sur des sujets plus généralistes.

Hier j'ai googlé un article (vulgarisant) où il était stipulé (je ne sais pas si c'est vrai) que la majorité de la communauté scientifique parie que:

1/ $P\neq NP$

2/ Aucun algorithme quantique ne pourra jamais résoudre un problème NP-complet en temps polynomial

3/ En mettant des garde-fou assez violents exploitant les remontées dans le temps via des trous relativistes pour ne pas obtenir un système de calcul contradictoire, il a pu être prouvé que la puissance quantique ne permet pas de dépasser $PSPACE$ en temps polynomial

Ce que je parie: 1 est probable ; 2 me parait faux (j'ai ma petite idée sur comment résoudre SAT quantiquement) et pour ce qui concerne (3), j'avoue que j'aimerais bien mettre la main sur la liste formelle des gardes-fous en question. Ca sent l'approximation physique à plein nez. A priori, je dirais que ces garde-fous consistent à tout simplement NE PAS permettre le voyage temporel, et donc j'ai des doutes sur le fait qu'ils ne soient que partiels.

De manière générale, sans parler d'algorithmique, on dispose d'un ensemble fini $E$ et d'une partie $A$ de $P(E)$ telle que $\forall X\in A\forall Y\supset X: Y\in A$. Autrement dit d'une notion de "gros ensembles". Et une instance de SAT demande s'il en existe un qui ne contient aucune paire contenue dans un AUTRE ensemble donné $B$ de paires d'éléments de $B$.

Chaque fois qu'on fait des réductions, on retombe là dessus, et c'est assez facile de voir que c'est dû à la polarité logique**.

Et typiquement, "être gros" est défini par "intersecter tous les machins de $C$" la plupart du temps

De la (petite) expérience que j'ai ignorer la polarité logique est PERDRE énormément d'avantages dans l'étude de ce truc.

** La polarité logique est le phénomène qui dit que la seule chose qui compte est la place positive ou négative des occurrences de variables. En effet, l'application $\to$ (l'implication) est une fonction $\phi$ comme une autre vérifiant:


$ \forall x: (y\mapsto \phi(x,y))$ est croissante et $ \forall x: (y\mapsto \phi(y,x))$ est décroissante

et c'est LA SEULE CHOSE QUI COMPTE!!!

C'est d'ailleurs une des raisons qui fait que passer par les anneaux de Boole est "une mauvaise idée", puisque $+$ n'est pas monotone.

Autrement dit, un théorème de la forme $R(x,y,y,t,...)$ où la place de $y$ dans $R(x,y,z,t,...)$ par exemple est décroissante et celle de $z$ est croissante autorise AUTOMATIQUEMENT l'affirmation plus générale que :

$$(y\to z)\to R(x,y,z,t,...)$$

est un théorème, sans aucun besoin de réfléchir.

Il suit que si on regroupe d'un côté les occurrences négatives et de l'autre les positives (chaque lettre n'apparait qu'une fois), pas besoin de rajouter des axiomes de la forme $x=y$ pour deux lettres qui, initialement, étaient égales, il suffit de rajouter $x\leq y$. En dualisant et (ie en ajoutant le mot "non" et en remplaçant $u\to v$ par $u\vee v$, on obtient un ensemble de conditions où toutes les occurrences sont croissantes et où les $x\leq y$ deviennent des empêchements de mettre tout à $1$, puisque ça exprime en fait des $non(u\wedge v)$, autrement dit des exigences que l'ensemble solution cherché ne doit pas contenir $\{u;v\}$

C'est juste ça qui fait qu'on étudie les $A$ ayant la propriété bleue.

Et pour l'anecdote, c'est aussi ça qui fait que certains discours politiques ou polémiques autres sont ridicules (quand on voit des gens s'inquiéter dans le mauvais sens polaire d'un occurrence du discours.

Les tentatives de "linéariser" (au sens des systèmes affines d'équations en tout genre) se heurte aussi à ce mur. Par exemple, en demandant que $a+b+c\leq 0$, on se donne vaguement l'impression de s'assurer une disjonction que l'un des trois est négatif, mais hélas, on s'assure beaucoup beaucoup beaucoup beaucoup plusssss. Par exemple tout graphe où on remplace les ou de cette manière est DEUX COLORIABLE quand la traduction a une solution (et ça écarte donc les graphes 54 coloriables en particulier)