coopération pour prouver Hadwiger

christophe c
christophe c
dans Fondements et Logique
bon il est tard, mais j'y avais pas pensé avant. Je propose une coopération pour prouver la conjecture d'Hadwiger à plusiseurs, ça peut êre sympa.

En fait je "sais" pourquoi elle est vraie, mais c'est hyperultrapénible à formaliser.

Voilà pourquoi, en gros, elle l'est:

Soit G un graphe. En fait on ne le regarde pas comme un graphe, mais comme un énoncé logique "déjà prouvé" (je propose, pour fixer les idées, que G est supposé ne pas êre coloriable avec 8 couleurs (ça permet de rester dans les chiffres, plutôt que des lettres, le reste étant déjà pas mal assez abstrait)

But du jeu montrer qu'il contient un "mineur" isomorphe à $K_9$

Si la logique classique était égale à la logique intuitionniste, ce serait trivial, en effet, on dispose déjà d'un tautologie (un théorème déjà prouvé, c'est ça le kiff) qui dit "G n'est pas 8 coloriable" et formellement, ça s'énonce:

"axiomes$\to$ disjonction des énoncés "$x_1\neq s_2$ et .... et $x_3\neq x_7$ et ...$x_8\neq x_9$" où la disjonction porte sur tous les ensembles de sommets $(x_1,...,x_9)$ du graphe $G$

Les axiomes du graphes sont $x_i\neq x_j$ pour chaque arête $(i,j)$ et les axiomes $a=b\ et \ b=c\to a=c$ pour tous les triplets de sommets

En logique intuitionniste, si des axiomes ne contenant pas "ou" entrainent une disjonction, alors en fait l'un des items est entrainé prouvablement. Dans ce cas particulier, si l'impossibilité de colorier $G$ avec 9 couleurs était intuitioniste, ça entrainerait (exercice) que $G$ contient carrément une 9-clique (ie il aurait $K_9$ comme sous-graphe et pas seulement comme mineur).

Hélas, nous vivons dans un monde classique. Hadwiger exprime que la conclusion ci-dessus est presque vrai à condition de remplacer "sous-graphe" par "mineur"

Vous me dires, ça change tout, mais vous allez voir que non... Je continue au prochain post, mais je pars à la rechercge de quelques fils que j'avais posté sur ce thème sans suite, pour ne pas tout réécrire....
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi

Réponses

  • christophe c
    christophe c
    Je continue.

    Qu'est-ce qui ajouté à la logique intuitionniste donne la logique classiques?

    Réponse les axiomes de la forme $A\to B\to A\to A$ (priorité à gauche pour les parenthèses)

    Ca s'appelle "axiome de Pearce"

    Quel rapport, me direz-vous avec Hadwiger?

    Et bien la réponse n'est pas tout à fait courte. En fait, histoire d'y aller avec une affectueuse douceur, il faut d'abord voir la "bonne façon" d'énoncer le théorème de Brouwer, qui en fait à à voir avec la connexité (bien que sa formulation "point fixe" ne le manifeste pas spécialement (sauf en dimension 1, TVI)

    Si 2 ouverts recouvent le carré [0,1]×[0,1], alors il existe un chemin continu allant de haut en bas entièrement inclus dans le premier ouvert, ou il existe un chemin allant de gauche à droite, entièrement contenu ds le 2ieme

    Comment ça s'exprime?

    Et bien en notations symboliques, par:

    Pour tout élément $L$ de $(A\to B)\to A$ il existe un élément $a\in A$ ET un connexe $C$ inclus dans $A\to B$ tels que

    1) pour tout $f\in C$, $L(f)=a$

    2) pour tout $b\in B$ il existe $f\in C$ tel que $f(a)=b$

    autrement dit par une formule dont le profil abstrait est la formule de Pearce. En prenant $A=2$ et $B=[0,1]$ c'est le Brouwer bien connu de la dimension1 et en fait Brouwer est vrai en "toute dimension" via Schauder, Ascoli etc.

    Voici 2 liens:


    http://www.les-mathematiques.net/phorum/read.php?14,394898,395026#msg-395026


    http://www.les-mathematiques.net/phorum/read.php?2,358795,359489#msg-359489
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    En fait, Brouwer est un théorème qui concerne le monde des objets finis, caché dans l'analyse. Il est très robuste.

    Revenons à Hadwiger: actuellement, en logique, la réalisation de l'axiome de Pearce (qui est, c'est marrant une découverte récente) ne se fait pas en tenant compte du C connexe du théorème précédent.

    Quand on a une preuve de $(A\to B)\to A$, donc par la correspondance de Curry HOward, un "robot qui réussit à attérir dans $A$ quand on lui fait cadeau d'un objet quelconque dans $A\to B$, L'informaticien Griffith a découvert que pour "réaliser" A, il suffit de "piéger" le robot. Ca correspond à la procédure "Call CC" ou "exit.

    Précisément, on donne au robot une "fausse" fonction qui va de $A$ dans $B$ et il s'exécute. Quand il sonne parce qu'il s'aperçoit qu'on l'a arnaqué et que la $f\in A\to B$ est un téléphone en plastique pour enfant, on l'assome à coups de massue parce qu'on sait que pour se rendre compte qu'il a été arnaqué, ça veut dire qu'il EST DEJA arrivé dans A. Donc pas besoin de lui donner le $f(a)$
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Un point du coup qui n'a pas été creusé est la partie $\forall b\in B$ du théorème précédent. En effet, plutôt si elle a été creusé en disant qu'au fond c'est trivial, et bien connu car c'est la classique argument diagonal de Cantor:

    si $L\in (A\to B)\to A$ alors si pour tout $a\in A$ ilexiste un $b_a\in B$ tel que $\forall f\in A\to B$ on a que:$L(f)=a\to f(a)\neq b_a$ on arrive à la contradiction avec $f:a\to b_a$

    Dans l'idée Griffthienne, ça correspond au fait qu'on peut tranquillement assomer le robot au moment où arrivé dans $A$ ilmet sa "fausse" clé dans la serrure qui va de $A$ à $B$ et se plaint, car nous ce qu'on cherchait c'est ..$A$ et le robot nous y a conduit.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Donc ce n'est pas tellement "Cantor" qui est oublié dans ce profil symbolique, mais c'est la connexité de l'ensemble C du théorème du deuxième post.

    Il est temps que je dise ce qu'est un mineur dans un graphe: c'est un ensemble d'ensembles connexes 2 à 2 disjoints de sommets et on considère que 2 d'entre eux sont reliés quand il y a une arête au moins qui va d'un sommet de l'un à un sommet de l'autre.

    Le théorème de Bouwer quant à lui exprime que quand un graphe connexe a une "dimension" n alors pour tout application de $G$ dans $n$, ie toute coloration de $G$ avec n couleurs, il existe un chemin (donc connexe) qui va d'un bord à l'autre en restant dans la même couleur
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    A propos de dimension, d'ailleurs, ces phénomènes donnent une définition alternative de dimension de $\R ^n$ (ou d'un espace topologique générale) qui marche aussi bien que les autres.

    Ca fait appel à la notion de "grahes infinitésimal", je vois pas trop comment l'appeler autrement. N'ayez pas peur, ça fait "grands mots", mais c'est assez "naif" en fait.

    De manière imagée, on peut colorier $\R$ avec 2 couleurs de manière que chaque ouvert inclus dans une seule couleur soit de tout petit diamètre. Mais on ne peut pas le faire pour la plan à cause du cas particulier du théorème rappelé au 2ième post et suggéré dans le lien

    http://www.les-mathematiques.net/phorum/read.php?2,358795,359489#msg-359489

    Par contre, on peut colorier le plan avec 3 couleurs de sorte que chaque ouvert inclus dans une seule couleur soit de tout petit diamètre, mais on ne peut pas le faire pour l'espace à cause.. du même théorème

    Et ainsi de suite....
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    La dimension "graphique" d'un esp top est par définition $n-1$ où $n$ est le plus petit entier tel que:

    pour $e>0$ quelconque, on peut colorier (avec des exigences honnêtes) l'espace avec $n$ couleurs tel que tout ouvert inclus dans une seule couleur a forcément un diamètre $<e$.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    La "bonne façon" d'énoncer Brouwer que j'ai proposée au 2ième post dit que la dimension de $\R ^n$ est $n$
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Of course, cette notion de dimension est une notion locale, mais ça n'a rien d'étonnant...

    En quoi Hadwiger peut être attaqué par ces papotages?

    Revenons à la formule de Pearce. En fait le "A", en pratique est un énoncé souvent trs compliqué (ie voir toutes les preuves par l'absurde en maths) et précisément dans le cas qui nous occupe, notre graphe $G$ non coloriable avec 8 couleurs, c'est la disjonction des $D$ où chaque $D$ est de la forme

    "$x_1\neq s_2$ et .... et $x_3\neq x_7$ et ...$x_8\neq x_9$"

    Au passage, je rappelle la preuve du point classique "si on peut prouver une disjonction en logique intuitionniste, on peut prouver un de ses items":

    Rajoutons une constante $Z$ et les axiomes $D\to Z$ à nos axiomes (déjà dits au premier post) du graphe.

    Il n'y a plus de "ou". En $G$ est tel qu'on peut maintenant prouver $Z$.

    Le théorème d'élimination des coupures indique que la dernière étape de la preuve de $Z$ est de la forme:

    "... donc D... donc Z"


    ce qui atteste qu'en fait pour prouver Z on est passé par prouver l'une des D (items de la disjonction).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Voici à quel endroit intervient la formule de Pearce, Brouwer et Hadwiger:

    appelons "tout" la conjonction de toutes les variables propositionnelles utilisées dans les axiomes du graphes (en comptant aussi, Z).

    J'appelle $Axi$ la conjonction de ces axiomes.

    Le 1er post suppose qu'il existe une preuve en logique classique de $Axi\to Z$

    Exercice (facile): on peut prouver en logique intuitionniste $axio \to [(Z\to tout)\to Z]$

    Autrement dit, si on interprete les variables propositionnelles comme des ensembles (ou des esp top, ou etc) on a une fonction canonique $L$ qui va de $Axi$ dans $(Z\to tout)\to Z$

    Et par le théorème de Bouwer, on obtient l'existence d'un élément de $z\in Z$ fixe et d'un ensemble connexe $S$ tel que pour toute application $f\in S\subseteq Z\to tout$ on a que $L(f)=z$. DE PLUS, pour tout élément de $y\in tout$ il existe $f\in S$ telle que $L(f)=y$

    Comme la seule manière d'arriver dans $Z$ est de passer par l'une des $D$, il existe donc 9 sommets attachés à la $L$ quiprovient de la preuve de $axio \to [(Z\to tout)\to Z]$

    Bien entendu, $L$ n'est pas trop "linaire" sinon, il existerait pas seulement un mineur, mais carrément un sous-graphe iso à $K_9$.

    Mais ce que les informaticiens qui s'occupent de Curry Howard ne font pas, c'est de s'occuper du $S$ connexe qui résulte et provient de la topologie algébrique et pas la plus facile, celle qui donne Brouwer.

    J'ai essayé sur des petits graphes, et ça marche (mais c'est une galère):

    En fait, quand $f$ parcourt $S$, l'exécution de $L$ dessine un progressivement un mineur de $G$ où chaque pays est pointé par les sommets de l'unique $D$ dont provient $z$ from $L$

    Je pense qu'ici il y en aura qui auront la patience de rédiger ça correctement. Je suis casiment sûr que c'est "sans obstacle" et que ça donne Hadiwiger.

    Si ça n'a pas été testé, c'est parce qu'il n'y a pas beaucoup de gens qui travaillent à la fois en théorie des graphes, en informatique version CUHO et en Brouwereries tordues. Les théoriciens des graphes ont tendance à se shooter à la combinatoire un peu trop exacte, par exemple et multiplient les résultats calculatoires compliqués. Le th de Roberson et Seymour est un peu à part, et, comme par hasard il utilise de la toppo algébrique
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Je reviens au plan précédent. Le côté 9-clique est assuré par le fait que quand on va parcourir le S du théorème de Brouwer, la disjonction D qui fournit son z fixe à Z, via la construction de L ne varie pas non plus.

    La SEULE objection possible (chose à justifier) est que les morceaux (forcément connexes, vu que S est connexe) vont peut-être se recouvrir partiellement ce qui foutrait tout parterre.

    En fait ce n'est pas le cas, mais c'est difficile à rédiger. C'est très exactement la même raison, purement logique, que celle qui apparait dans des raisonnements du genre quand on prouve, par exemple, Cayley Hamilton sans calcul, en le justifiant sur la matrice générique abstraite (où toutes les valeurs propres sont différentes) et où on "peut croire" être génés ensuite à cause des "=" éventuels entre VP.

    Là c'est pareil, ce n'est pas à "nous" de justifier que les morceaux du mineur issu de S ne vont pas s'intersecter, car en fait par définition, c'est donné par la preuve qui a donné la construction de L

    Cependant je ne vois pas du tout comment mettre ça en forme, ça m'a l'air d'une chirie sans nom..
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • FrançoisD
    FrançoisD
    Salut,

    effectivement (je n'ai lu que les 2 premiers messages) Hadwiger est intuitif mais visiblement, plus l'énoncé est intuitif plus c'est... euh... j'ai le droit à "merdique"?

    Ca me fait penser à une autre conjecture du même acabit : "tout groupe non-moyennable contient un sous-groupe isomorphe à L(x,y)" qui (comme chacun sait) est le prototype de groupe non-moyennable ([Pedersen, Invariant means on topological groups]).

    Le problème reste toujours le même : généricité d'un contre-exemple donné dans une théorie.

    Est-ce qu'il possible que ça soit indécidable? il y en a d'autres des problèmes "indécidables" (sens naïf et non Gödelien) sur les graphes, non?
    Si mes souvenirs sont bons:
    $x\mathcal R y$ ssi $x-y\in\Q$ donne une relation d'équivalence sur $\R$ et on ne peut pas savoir combien de couleurs il faut pour colorier $\R/\mathcal R$ car le résultat est différent dans ZF (infiité) et ZFC (2).
    Si quelqu'un a la référence d'un article sérieux sur ce truc, je suis preneur d'ailleurs...

    Amicalement,

    F.D.
  • christophe c
    christophe c
    Concernant ton dernier exemple, tu n'as pas précisé où sont les arêtes.... Si j'ai bien compris les sommets sont les classes d'équivalence, mais les arêtes?

    Certes, Hadwiger pourrait être indécidable, en théorie, mais il a le profil d'une équation diophantienne, donc s'il l'est, on ne le saura jamais.

    La seule chose éventuelle qu'on pourrait prouver pour ce genre de problème est que vrai --->indécidable, autrement dit qu'il n'en existe pas de preuve (à théorie fixée).

    Pour ma part, je pense qu'il est prouvable et que c'est une facette du théorème de Brouwer, qui est hélas encore très mal compris..
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • FrançoisD
    FrançoisD
    Justement, je bugge dans la définition du graphe : sommets = points de $\R$, arêtes relient deux points ssi même classe d'équivalence?

    Je n'ai pas de référence exacte, et ça m'ennuie.

    Au fait, le théorème de Brouwer (de point fixe) n'est-il pas tout sauf intuitionniste?

    (voir [Ageron, Girard] qui ont des points de vues opposés sur Brouwer mais pas sur le susdit th.)

    F.D.
  • christophe c
    christophe c
    Le théorème de Brouwer est un mystère: il n'en existe aucune preuve respectable, et certes, elles sont toutes avec 2 étapes par l'absurde au moins.

    Mais justement, je pense que (j'en fais le pari) le jour où l'humanité sera assez évoluée pour comprendre que la recherche de bonnes preuves est aussi importante (voir plus) que celle de résultats nouveaux, alors Brouwer et Hadwiger seront tous 2 des cas particuliers d'un même théorème important et bien compris.

    (sinon, je n'ai pas lu Ageron, je ne connais pas et Girard: le point aveugle?)

    Prends un hypercarré (un échiquier) $C^n$ et prends une application $f$ de $C^n$ dans $n$. Vois $C$ comme une échiquer de dimension 1 (une suite de cases)

    Autrement dit, tu as alors une application de $(n\to C)\to n$. Le théorème de Brouwer dit (entre autre) qu'il existe un élément privilégié $e$ (au moins1) de $n$ et un chemin $T$ "continu" d'éléments de $C^n$ tel que:

    1) pour tout élément $t\in T$, $f(t)=e$

    2) $T$ va d'un bout à l'autre de l'hyperéchiquier, ie pour tout élément $x\in C$, il existe un $t\in T$ tel que $t(e)=x$ ($t(e)$ n'est rien d'autre que la e ième case de $C$


    Visuellement, avec $C=2$, ça te dit que si tu colories les cases d'un damier en 2 couleurs, tu peux le traverser en restan sur une seule couleur.

    Quand tu regardes le "profil" de ce théorème: $[(n\to C)\to n]\to n$, c'est très exactement le profil suivant:

    $[(A\to B)\to A]\to A$ qui est l'axiome du raisonnement par l'absurde qu'il suffit de rajouter à la logique intuitionniste pour avoir la logique classique.

    La plupart des théorèmes de maths "préservent" les profils (quand ils sont profonds).

    Par conséquent, il y a non seulement peu de chance que Brouwer soit accessbile autrement que par l'absurde, mais je pense même que c'est le raisonnement par l'absurde qui a quelque chose à demander à Brouwer.

    La conjecture d'Hadwiger, à part qu'elle n'est pas prouvée, est dans le même cas.

    Quand on applique un axime de RPA, ce qu'on fait c'est qu'on prouve $(A\to B)\to A$ et on dit à l'assemblée "donc A" d'un revers de la main. On oublie complètement le "résidu", le "joyau" qui est le $T$ ci-dessus obtenu dont Brouwer assure la CONNEXITE.

    La conjecture d'Hadwiger est très exactment un énoncé presque trivial auquel on a rajouté "qui sont connexes"..
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Brouwer moins connexité = l'énoncé suivant:

    Si pour toute famille de uplet $x:=(x_1;...x_n)\in E^n$ il existe l'un des $i$ compris entre $1$ et $n$ tel que le uplet $x$ est dans $W_i$ alors il existe un $j$ et un ensemble de uplets $Z\subseteq W_j$ tel que la jième projection de $Z$ est l'ensemble $E$ entier

    qui est presque trivial, sinon classique.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Pour l'anecdote: on appelle "espace" tout ensemble de graphes stables par mineures. On peut les voir comme des "vrais" espaces (genre le plan) avec leurs éléments qui sont dessinés dans le vrai espace (exercice)

    La CjHad et conséquence de l'énoncé suivant qui je pense est très vox populi:

    "si tous les espaces bords de E ont un nb chromatique qui ne dépasse pas n alors le nb chromatique de E ne dépasse pas n+1" (1)

    Le nombre chromatique d'un espace est le plus grand nombre chromatique possible des graphes de l'espace

    Les espaces bords de E sont fabriqués comme suit: on prend un pays P de E et on regarde l'ensemble des graphes qu'on peut dessiner avec que des pays qui touchent P

    Exemple: les espaces bords des espaces bords du plan sont le suite de sommets $u_1;u_2..u_n$ telles qu'il y a seulement une arête entre $u_i$ et $u_{i+1}$

    Théorème: la Cj d'Hadwiger est en fait équivalente à l'énoncé (1).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    [size=large]Voici un pdf d'une page[/size]

    [small]rien à voir: je suis tellement verbeux que je viens de passer 20mn :-X à modifier tous les Christophe C....... en Christophe C. Je présume qu'il n'y a pas de moyens de le faire pour tous les posts du forum?[/small]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 26

BlueberryChaurienCidrolinCyranoDomMatricule_63Milasabcdbielyjohn_johnzestezygomathique +14 Invités