Décidabilité en géométrie et algèbre
[ancien titre: Messages effacés]
Je recopie ici un message effacé par deux fois du fil "Droites concourantes 5". Il visait à commenter le PS de ce message de Pappus.
Pour qui ne comprend pas le PS de Pappus, il fait allusion à un message de Christophe (effacé par la modération) mentionnant la décidabilité de la géométrie et de l'algèbre élémentaire (la théorie du premier ordre du corps ordonné $\R$), résultat bien connu depuis Alfred Tarski : il y a un algorithme pour décider la vérité de tout énoncé de cette théorie (l'énoncé de Bouzar par exemple). L'hypothèse de Riemann n'est pas un énoncé de cette théorie.
Je recopie ici un message effacé par deux fois du fil "Droites concourantes 5". Il visait à commenter le PS de ce message de Pappus.
Pour qui ne comprend pas le PS de Pappus, il fait allusion à un message de Christophe (effacé par la modération) mentionnant la décidabilité de la géométrie et de l'algèbre élémentaire (la théorie du premier ordre du corps ordonné $\R$), résultat bien connu depuis Alfred Tarski : il y a un algorithme pour décider la vérité de tout énoncé de cette théorie (l'énoncé de Bouzar par exemple). L'hypothèse de Riemann n'est pas un énoncé de cette théorie.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
ceci dans le fil en question... d'où tes messages effacés.
Ouvrir une autre discussion s'imposait, ce que tu viens de faire.
Je me permet d'en changer le titre.
Eric
Je n'aurais pas dû répondre à Christophe mais je voulais savoir s'il était aussi fort en décidabilité qu'il le laissait paraître!
Ce n'était pas bien méchant!
On peut en tout cas décider qu'il l'est plus que moi!
Amicalement
Constatons les faits : de l'intervention de Christophe dans le fil en question il ne reste comme trace, grâce à la modération d'Eric, que ce petit PS de ta part qui vise à la ridiculiser (pas très méchamment, d'accord). Alors qu'objectivement, du point de vue mathématique, Christophe avait parfaitement raison sur cette histoire de décidabilité algorithmique, et faire intervenir comme tu l'as fait l'hypothèse de Riemann dans l'histoire ne prouve que ta méconnaissance de la question, sauf le respect que je te dois.
C'est la raison pour laquelle je voulais, sans polémiquer et dans un message très court (les 3-4 lignes du 1er message du présent fil), rétablir les faits mathématiques à la suite de ton PS,. Eric ne m'en a pas laissé la possibilité, et j'ai dû me résoudre à ouvrir un nouveau fil dont il a d'ailleurs changé le titre, alors qu'il n'était aucunement dans mon intention de lancer un fil sur la décidabilité.
Maintenant, je me permets un brin de polémique.
Cher Pappus, tu te lamentes à longueur de message sur le manque de culture géométrique de nos élèves et étudiants. Mais alors que penser de ce manque de culture logique que tu manifestes, toi un professionnel des mathématiques et de la géométrie, sur un résultat aussi important théoriquement et aussi parlant concernant la géométrie élémentaire ?
Bien sincèrement.
Je croyais que supprimer mon PS était une bonne idée mais je viens de rétablir cette preuve manifeste de mon inculture, ce qui devrait te rendre joyeux.
Mais comme le dit la célèbre chanson:
Moins je s'rai calé, plus je s'rai le meilleur!
Je devrais donc être en bonne compagnie.
Je ne suis donc ni un professionnel des mathématiques ni a fortiori un professionnel de la géométrie, cela doit-il te rassurer ou t'inquiéter?
En tout cas, je dois être un peu maso car j'adore que tu me tapes sur les doigts, en toute logique évidemment!
Amicalement
Pappus
soit une famille de polynomes $P_1,...,P_n, Q_1,...Q_p$.
Il suffit d'exprimer $Z:=\exists x: P_1(x)=0\wedge ...\wedge P_n(x)=0\wedge Q_1(x)>0\wedge ...\wedge Q_p(x)>0$ sous forme d'un énoncé E sans quantificateurs, avec des "ou" et des "et" des $=$, des $>$, des polynomes en les coefficients des $P_i,Q_j$. Sachant "qu"on ne sait rien" des paramètres (ie des coefficients des $P_i,Q_j$) et donc rigoureusement ce qui doit être obtenu est $(\forall a\forall b...: Z)\iff (\forall a\forall b...: E)$ où $a,b,..$ sont les paramètres.
Ca c'est pour $(\R,+,\times)$ et c'est rendu possible par la technique des "tableaux de variations" (mais je sais pu comment, si je l'ai jamais su un jour d'ailleurs en gros on sait qu'un "x" existe quand des conditions beaucoup plus laches existent par le TVI)
Lorsque vous avez affaire à $(\C,+\times)$ c'est un peu plus simple (dans mon souvenir) car il n'y a que $=$ et $\neq $ à gérer et j'ai vaguement l'impression qu'on peut même se passer de $\neq$, ie ramener
$\exists x: P_1(x)=0\wedge ...\wedge P_n(x)=0$ (probablement qu'un histoire de résultant suffit???)
à un énoncé avec des $=$ et des polynomes des "et" et des "ou".
Celles et ceux qui voudraient plus de détails, Ga? connait probablement parfaitement cet aspect.
Pour la partie logique:
1) tout énoncé est équivalent à un énoncé sous forme prénexe
2) la partie ouverte (celle qui suite les quantificateurs) peut être mise sous forme d'une disjonction de conjonctions
3) un $\exists $ devant des "ou" se distribue, ie $(\exists x: A\vee B\vee C... )\iff [(\exists x A)\vee (\exists x \vee ...$. On n'a donc qu'à traiter le cas $\exists x: A\wedge B\wedge C... $
Le pire c'est que par deux fois j'ai eu "le sentiment" que $\neq$ n'était pas nécessaire exactement pour la raison que $x\neq y\iff \exists t: tx=ty+1$ autrement dit, presque au sens propre j'ai marché sur la tête (j'ai renversé l'argument invalidement)
1) On n'a qu'à traiter la situation: $\forall x: [ P_1(x)\neq 0\vee ...\vee P_n(x)\neq 0 \vee Q_1(x)=0\vee ...\vee Q_p(x)=0 ]$
2) Ce qui se ramène à traiter une situation $\forall x: [ P_1(x)\neq 0\vee ...\vee P_n(x)\neq 0 \vee Q(x)=0 ]$
3) qui s'écrit aussi: $\forall x: [ (P_1(x)= 0\wedge ...\wedge P_n(x)= 0 ) \to Q(x)=0 ]$
4) Avec le degrés, on peut de manière effective ***** borner les degrés et trouver effectivement un nombre entier $k$ et donc traiter cette situation en se demandant si :
5) le PGCD des $P_i$ divise $Q^k$
6) ce qui nous ramène à une (grosse, certes) dijonctions de conjonctions d'égalités et inégalités polynomiales** en les coefficients des $Q_j$ et $P$
je peux me tromper, en particulier sur la facilité de calculer le PGCD par disjonction de cas (ou ailleurs, je suis vraiment béotien pour ces trucs-là)
***** par exemple la phrase $\forall x: P(x)=0\to Q(x)=0$ équivaut à $P$ divise $Q^{deg(P)}$ (je pense) car "en imaginant" que le scindage des deux fera apparaitre les mêmes (enfin une inclusion de ceci dans cela entre ensembles finis) racines (mais avec des multiplicités différentes) et on court-circuite la difficulté en mettant Q à une puissance suffisamment grande)
** le PGCD dépend seulement de la nullité ou non de certains polynomes en les coefficients ce qui amène une disjonction de cas
1) On n'a qu'à traiter la situation: $\forall x: [ P_1(x)> 0\vee ...\vee P_n(x)> 0 \vee Q_1(x)=0\vee ...\vee Q_p(x)=0 ]$
2) Ce qui se ramène à traiter une situation $\forall x: [ P_1(x)> 0\vee ...\vee P_n(x)> 0 \vee Q(x)=0 ]$
3) qui s'écrit aussi: $\forall x: [ (P_1(x)\leq 0\wedge ...\wedge P_n(x)\leq 0 ) \to Q(x)=0 ]$
4) qui s'écrit aussi: $\forall x: [ f(x)\leq 0 \to Q(x)=0 ]$
où $f:=(x\mapsto max_i P_i(x))$
Mais $a=0$ peut s'écrire $a\leq 0$ et $-a\leq 0$
donc on peut traiter seulement les situations
5) $\forall x: [ f(x)\leq 0 \to Q(x)\geq 0 ]$
6) qui revient à $\forall x: g(x)\geq 0$
car il y a équivalence entre:
6.1) $a\leq 0$=> $b\geq 0$
6.2) $max(a,b)\geq 0$
où $g$ continue est écrite avec des opérations polynomiales et le signe $\sigma$ qui désigne $x\mapsto max(0,x)$ qui est dérivable partout sauf en $0$ et dont en plus la dérivée est très simple.
7) On n'a plus alors qu'à étudier les antécédents par $g'$ la dérivée de $g$ de $0$, ainsi que les éléments qui ne sont pas dans le domaine de $g'$, et pour chacun $x$ d'eux, se demander si $g(x)\geq 0$.
8) Pourra-t-on exprimer l'énoncé $\forall x: g(x)\geq 0$ comme un énoncé qui est une combinaison booléenne de propriétés polynomiales et "u>v", "u=v" concernant les paramètres apparaissant dans $g$? That is the question... (Peut-être bien que non)
$\forall coefficients [(\forall x: (min_i (P_i(x))\leq 0))\iff (E)]$
Si on veut voir des choses comme ça racontées sérieusement, on peut se référer à la littérature, et il y en a disponible sur le web : ici un livre qui contient tout ça et beaucoup d'autres choses, avec analyse de la complexité etc.
Avant de cliquer sur "envoyer", quand-même, je défends mon oeuvre (:D en ce qui concerne le cas des corps algébriquement clos de caractéristique zéro.
A moins que je me sois trompé sur le fait ***** sinon, passé la routine logique vraiment élémentaire, j'étais assez content de ce que j'avais raconté, et il ne me semblait pas qu'un lecteur studieux aurait rencontré des obstructions essentielles
En tout cas, moi, je serais prêt à parier que si on me donne une famille finie de polynomes $P_1,..,P_n, Q$ (dont on privilégie la variable $x$ mais qui contient tout plein de coefficients (formant la liste L=$a_1;...;a_k$) qui sont aussi des "lettres") je peux trouver une combinaison booléenne $E$ de formules de la forme $u=0, u\neq 0$ où chaque $u$ est un polynôme écrit uniquement avec les lettres figurant dans $L$, de sorte que:
$\forall a_1,...,a_k [(\forall x: [(P_1(x)=0\wedge ... \wedge P_n(x)=0)\to Q(x)=0])\iff E]$ sera un théorème
Et pour ça, je me dis: "ça revient à ce que le PGCD des $P_i$ soit un diviseur de $Q^{max_i(deg(P_i))}$ en visant large"
Of course, "le PGCD" des $P_i$ n'est pas "un seul" polynome car il y a de nombreuses possibilités selon que certains trucs soient nuls ou non, mais tout ça, ça me semble me faire une zolie combinaisons booléenne après application de l'algorithme d'Euclide -D
Par contre, pour le cas "réel clos", je pense que tu as totalement raison sur le fait que je me suis retrouvé bloqué sans même avoir la moindre idée sur la question de savoir "est-ce que j'avais au moins simplifié comme il fallait la question pour entrer dans la dernière ligne droite calculatoire"
Bon, je dois faire une course, mais après, je vais confronter toutes ces idées avec ton lien
J'ai l'impression que le livre (du moins ces pages) travaille dur à "formaliser" un argument qui permet de raisonner par récurrence sur un algorithme de "tableaux de variation" et c'est effectivement ce qui me pose problème (bon d'un autre côté, j'ai fait tellement de tableaux de variation dans ma vie )
Bon bin, ça m'a tellement épuisé que je n'ai pas regardé le cas $\C$ encore merci pour ce joli livre (qui fait 700 pages!!!!!)
En ce qui concerne la complexité, il faut se référer au livre mis en lien plus haut : c'est essentiellement doublement exponentiel en le nombre d'alternances de quantificateurs (moche, mais tout de même nettement moins affreux qu'une tour d'exponentielles de hauteur le nombre de variables !).
** pourtant j'ai traficoté dans tous les sens en imagination
Oui, la borne de complexité, j'avais entendu dire qu'il existe un preuve*** qu'elle ne peut être moindre que celle que tu dis et j'ai dû me tromper en évoquant la tour d'exponentielle. Je regarderai dans l'autre document
*** (et pas seulement un résultat du genre: "la meilleure efficacité connue est..." mais je peux me tromper)
***** Quelle patience tu as même mis un exemple détaillé page 14 à ce que j'ai vu!
En gros, ce qui m'intéresse en premier chef, c'est l'élimination de $\exists x$ dans $\exists x: P_1(x)>0\wedge...\wedge P_n(x)>0\wedge Q(x)=0$
ou la pseudo-élimination de derniers ${\red } \exists x_1\exists x_2....\exists x_n}$ dans $....\forall\forall...\forall {\red \exists x_1\exists x_2....\exists x_n}: P(parametres, x_1,...,x_n)=0$
en appelant "pseudo-élimination" le fait de parvenir à les remplacer par des $\forall y_1...\forall y_p$ de façon à faire disparaitre une alternance de quantificateurs. (Tu m'as fait penser à ça en parlant d'alternances*****)
***** On pourrait alors avoir une stratégie (j'ignore si elle est possible):
$..\exists...\exists \forall ...\forall {\red \exists ...\exists }$
$..\exists...\exists {\green \forall ...\forall} {\red \forall ...\forall ...\forall }$
$..\exists...\exists {\green \forall ...\forall \forall ...\forall ...\forall }$
$..\forall...\forall {\red \exists ...\exists \exists ...\exists ...\exists }$
et recommencer
en notant que $\exists x: P_1(x)>0\wedge...\wedgeP_n(x)>0\wedge Q(x)=0$ se met aisément sous la forme $\exists ...\exists : R=0$
je n'arrive pas vraiment à suivre la discussion, mais voici une question concrète qui est peut-être une reformulation de ce qui précède mais comme je ne comprends pas...
Dans beaucoup de problèmes de géométrie, on sait que le truc de Morley permet de conclure à coup sûr. Par exemple, prenons le fil "Point de Nagel et droites sécantes".
Je n'ai pas de solution synthétique à ce problème, mais je sais qu'on pourrait procéder ainsi : on considère les points de contact $A',B',C'$ du cercle inscrit avec les côtés. On se place dans un repère tel que le cercle inscrit est centré en l'origine et de rayon 1. Appelons $z_1,z_2,z_3$ les affixes de $A',B',C'$. Il est facile de calculer les affixes de $A,B,C$ en fonction de $z_1,z_2,z_3$. On calcule ensuite facilement les équations des bissectrices intérieures et extérieures, puis du point de Nagel, puis de $D,E,M,T$. Une résolution d'un système linéaire permet de trouver les équations des cercles circonscrits de la figure, puis en faisant la différence de deux équations on trouve l'équation de l'axe radical, ce qui permet d'obtenir l'affixe de $P$. On calcule alors les équations de $\Delta_1$ et $\Delta_2$, on trouve l'affixe du point d'intersection et on vérifie qu'il se trouve sur le cercle circonscrit.
Ici, on voit donc que c'est facile parce qu'on peut partir d'un nombre fini de points "libres" $z_1,\ldots,z_n$, et on peut calculer simplement un polynôme $P(z_1,\bar{z_1},\ldots,z_n,\bar{z}_n)$ et l'exercice consiste à montrer qu'il est nul, ce qui peut se faire de manière automatique.
D'ailleurs, Rescassol muni de Matlab parvient à résoudre la plupart des exercices de géométrie postés sur le forum. Pldx1 lorsqu'il travaille en complexes fait de même avec des notations un peu différentes afin d'utiliser les outils du calcul matriciel.
Certains exercices peuvent s'avérer plus compliqués. Ils peuvent se présenter sous la forme de $n$ points $z_1,\ldots,z_n$ donnés, vérifiant un ensemble de contraintes que l'on peut coder sous la forme d'un polynôme $P(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)=0$ (en fait il pourrait y avoir plusieurs polynômes $P_1,\ldots,P_k$ mais on peut les remplacer par un polynôme unique $|P_1|^2+\cdots+|P_k|^2$). La plupart des problèmes de géométrie peuvent donc s'écrire sous la forme : montrer que
$$P(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)=0 \implies Q(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)=0.$$
La première question serait donc : y a-t-il un algorithme efficace permettant de démontrer une implication telle que la précédente ? Si oui, a-t-il déjà été programmé dans un logiciel de géométrie ? J'imaginerais une extension de Geogebra, où on ferait une figure avec un certain nombre de points libres et de points liés, et où on demanderait à l'ordinateur de démontrer par exemple que deux points sont égaux, ou que deux droites sont parallèles,...
Autre question : y a-t-il un théorème du genre "si ça se voit sur la figure alors c'est vrai" ? Plus précisément, est-ce que étant donnés $P$ et $Q$ comme ci-dessus on peut trouver de manière effective $\eta>0$, $\epsilon>0$ et $R>0$ tel que si $\forall z_1,\ldots,z_n$ de module $\le R$ on a $|P(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)|<\eta\implies |Q(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)|<\epsilon$, alors on peut en déduire que $\forall z_1,\ldots,z_n$, $P(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)=0 \implies Q(z_1,\bar{z}_1,\ldots,z_n,\bar{z}_n)=0$ ?
$\forall x_1,...,x_n: P(x_1,...,x_n)\neq 0$ ***
doit pouvoir "se calculer" honorablement rapidement
Je viens d'imprimer (et en couleurs STP!!) le chapitre1 de Ga? Je te ferai une fiche de lecture soignée dès que j'aurai compris le truc qui me manque
*** P1 non nul ou P2 non nul ou .. Pn non nul ou Q nul se dit:
P1 non nul ou ... ou Pn non nul ou 1-tQ non nul (en rajoutant un "quelque soit t")
qui se dit: pour tous .....: [ P1² + ... + Pn² + (1-tQ)² ] non nul
ie qui se dit "il n'existe pas de x1,x2... tels que R(x1,..)=0"
pour dire $x\in \{0,1\}$ on peut écrire $x^2=x$
pour dire "truc=0 ou machin=0" on peut écrire $truc.machin=0$
pour dire "truc=0 et machin=0" on peut écrire truc²+machin²=0
pour dire non(truc), on peut écrire 1-truc
On peut ainsi réduire toute question de savoir si une formule du calcul propositionnel est satisfaisable à une question de savoir si un polynôme réel à plusieurs variables a un uplet solution à peu de frais.
1) Dans le cas des nombres complexes (ou des corps algébriquement clos de caractéristique 0), si on note $Z(P)$ l'ensemble des racines du polynome $P$ alors la question de savoir si $Z(P_1)\cap ...\cap Z(P_n) \subseteq Z(Q)$ est "facile" dans le sens où elle s'exprime en une question équivalente qui s'écrit avec des "et" , des "ou", des $=$ des $\neq$ , des expressions algébriques avec $+, \times, 0,1$ et des coefficients des $P_i, Q$.
2) Autrement dit on peut, sans rien connaitre des coefficients des $P_i, Q$ trouver un énoncé sans quantificateurs $E$ tel que: $\forall a_1,...,a_k [(\forall x: P_1(x)=0\ et ... \ et P_n(x)=0 \ implique Q(x)=0)\iff E]$ où les $a_i$ sont les variables libres apparaissant dans les $P_i,Q$ (ce qu'on appelle généralement les paramètres)
3) Pour prouver (1) et (2), pense à la forme scindée des polynomes. Dire que tous les zéros communs aux $P_i$ sont des zéros de $Q$ revient à demander que $Q$ mis à une puissance assez grande mais effectivement exprimable uniformément soit un multiple du PGCD des $P_i$, or le PGCD des $R_i$ se calcule facilement, même s'il ya plusieurs cas (ce "plusieurs cas" se traduira par des "et" des "ou" rajoutés)
4) Dans le cas de $\R$ c'est nettement plus difficile, mais j'y viens dans la suite (j'ai identifié les passages du doc mis en lien par Ga? )
5) Pourquoi faire tout ça?
5.1) Soit $K$ un corps (un des deux corps $\R,\C$)
5.2) Un énoncé écrit avec les signes $\forall, \exists , et, ou, =,\neq, 0,1,+,\times, variables,>$ (le strictement supérieur ne concerne que $\R$) peut être vrai ou faux (comme tu sais ) et s'il contient des variables libres il détermine une application qui envoie chaque uplet de valeurs sur $\{vrai, faux\}$
5.3) Tu sais que chaque énoncé (dans toute théorie) écrite avec des "et","ou" peut s'écrire sous la forme d'une conjonction de disjonctions tout aussi bien que sous la forme d'une disjonction de conjonctions
5.4) Maintenant imagine que tu as un $\exists x$ devant une disjonction: $\exists x: D_1\ ou ... \ ou \ D_n$. Et bien c'est équivalent à $(\exists xD_1)\ ou ... \ ou \ (\exists xD_n)$
5.5) De même en ce qui concerne $\forall$ avec les conjonctions
5.6) Par ailleurs, quand tu mets un "non" devant un énoncé, tu peux le distribuer jusqu'à plus possible via:
5.6.1) $non(\forall xP)$ qui devient $\exists x(nonP)$
5.6.2) $non(A\ et\ $ qui devient $(nonA)\ ou\ (nonB)$
5.6.3) $non(A\ ou\ $ qui devient $(nonA)\ et\ (nonB)$
5.6.4) $non(a=b)$ qui devient $a\neq b$
5.6.5) $non(a\neq b)$ qui devient $a=b$
5.6.6) $non(a>b)$ qui devient $a=b$ ou $b>a$
5.7) Dans le cas précis de $\R$: $P=0\ et\ Q=0$ peut devenir $P^2+Q^2=0$
5.8) Dans tous les corps $P=0\ ou\ Q=0$ peut devenir $PQ=0$
5.9) En 5.7,5.8 j'ai mis des majuscules mais elle désignent n'importe quoi
5.10) Le bilan de 5.2-5.9 est la chose suivante:
5.10.1) (Cas $\C$): [size=x-large]SI[/size] on peut éliminer la quantification $\exists x$ dans n'importe quel énoncé $\exists x: P_1(x)=0\ et\ P_2(x)=0\ et\ ...\ et\ P_n(x)=0\ et\ Q(x)\neq 0$ [size=x-large]ALORS[/size] n'importe quel énoncé de la théorie de $(\C, +, \times)$ (avec ou sans paramètres, ie variables libres) peut de manière effective être démontré équivalent à un énoncé (contenant les mêmes variables libres) et qui est sans quantificateur
5.10.2) (Cas $\R$): [size=x-large]SI[/size] on peut éliminer la quantification $\exists x$ dans n'importe quel énoncé $\exists x: P_1(x)>0\ et\ P_2(x)>0\ et\ ...\ et\ P_n(x)>0\ et\ Q(x) = 0$ [size=x-large]ALORS[/size] n'importe quel énoncé de la théorie de $(\R, +, \times)$ (avec ou sans paramètres, ie variables libres) peut de manière effective être démontré équivalent à un énoncé (contenant les mêmes variables libres) et qui est sans quantificateur
5.10.3) Remarque: une fois ça fait, les théories $(K,+,\times)$ sont du coup récursives pour ces corps-là, ie il y a un algorithme qui dit si un énon cé clos (sans variable libre) est vrai ou faux
5.11) Il reste donc les cas techniques 5.10.i à traiter.
5.11.1) Le cas 5.10.1) est facile et (sauf erreur) traité en (3) ou à un de mes posts précédents
5.11.2) Le cas 5.10.2) est traité dans le DEUXIEME lien (pdf d'une soixantaine de pages) mis par Ga? entre les pages 1 et 10 environ. Je ne peux pas te résumer car, comme c'est un mécanisme calculatoire, je l'ai un peu lu, mais ne l'ai pas encore "intégré". Mais pour toi, ça devrait nromalement être du gateau. Je crois que les pages 1-10 en question font plus que dire si "oui ou non" $\exists x: P_1(x)>0\ et\ P_2(x)>0\ et\ ...\ et\ P_n(x)>0\ et\ Q(x) = 0$: elles associent de manière effective le nombre de réels différents $x$ qui marchent à une formule sans quantificateur dont les variables libres sont les paramètres
6) Dans un post ultérieur j'essairai de connecter ça avec ta question.
Voilà, il ne reste plus qu'à cliquer sur son lien et à lire les premières pages.
$\forall a,b,c: ([a\neq 0] \to [(\exists x: ax^2+bx+c = 0)\iff (b^2-4ac\geq 0)])$
(Bon, ça me saoulait de réfléchir au cas $a=0$ mais ce qui est à droite de $\iff$ est sans quantificateur mais ce qui est important est qu'on puisse mettre un $\forall parametres$ devant l'équivalence (ici "$\forall a,b,c$") .
Je tente de répondre à JLT. D'abord, la formulation avec des complexes ne sert pas à grand chose (du point de vue théorique, parce que du point de vue pratique ça peut être commode d'utiliser des calculs sur les complexes pour certains problèmes). On considère donc un problème géométrique qui se traduit en coordonnées par
$$P_1(x_1,\ldots,x_n)=\ldots=P_k(x_1,\ldots,x_n)=0 \Rightarrow Q(x_1,\ldots,x_n)=0\;.\eqno(*)$$
Le résultat théorique fondamental est: il y a un algorithme qui décide la vérité de tout énoncé de ce type (sur $\R$ ou sur $\C$), et aussi de tout énoncé du premier ordre du langage des corps (des corps ordonnés si on est sur $\R$). Il y a des logiciels où cet algorithme d'élimination des quantificateurs est implémenté. Mais ces logiciels "à tout faire" restent très limités pratiquement, du fait de la complexité de l'algorithme.
Il y a par ailleurs des logiciels de démonstration automatique en géométrie. En très gros, un moyen de faire pour le type de problèmes $(*)$ ci-dessus est de diviser la conclusion $Q$ par les hypothèses $P_i$ et de vérifier si on trouve $0$. Ca a bien un sens, on peut vérifier algorithmiquement et assez efficacement l'appartenance à un idéal (en utilisant les bases de Gröbner par exemple). Il y a pas mal de travaux dans ce domaine, avec un pionnier chinois qui s'appelle Wu, si je me souviens bien. Je connais Tomas Recio, très actif dans le sujet (on peut googler)
Pour ta deuxième question, toujours à cause du résultat général d'élimination des quantificateurs, on peut donner une réponse comme suit. Avec la formulation du problème comme ci-dessus, en fixant le nombre $n$ de variables, le nombre $k$ d'hypothèses $P_i$ et le degré maximum $d$ des polyn\^omes $P_i$ et $Q$ (de sorte que seuls les coefficients varient), on peut produire algorithmiquement des fonctions strictement positives calculables $R$, $\eta$, $\epsilon$ des coefficients telles que $(*)$ pour les coefficients $\mathbf{a}$ est vrai ssi pour tout $\mathbf{x}$ avec $\Vert \mathbf{x}\Vert \leq R(\mathbf{a})$ vérifiant $|P_i(\mathbf{x})|<\eta(\mathbf{a})$ pour $i=1,\ldots,k$, on a $|Q(\mathbf{x})|<\epsilon(a)$. Mais produire $R$, $\eta$ et $\epsilon$me semble inatteignable pratiquement.
Tu parlais dans $\C$ pour ce cas précis ou dans $\R$? (Parce que si on divise $X+5$ par $X^2+1$ on obtient $X+5=0.(X^2+1) + X+5$ (enfin je crois ) ou peut-être ce genre d'exception est plus ou moins "le seul genre")
@JLT et Ga?
Une des raisons qui me semble assez violente de cette difficulté est qu'on peut ramener la question de savoir si une formule propositionnelle est une tautologie à une question du genre:
Autrement dit, on peut ramener un problème co-NPcomplet à une question d'existence de points vérifiant des conditions simples de géométrie planaire (car quitte à rajouter des $\exists y_i$ on peut même faire que tous les polynomes sont des degré au plus 2 en toutes les variables, et même que ce soient des polynomes très simple, ie soit de degré au plus 1, soit de la forme $x^2=y$, puisque:
$a=bc$ s'écrit $\exists : x=b+c, x^2 = y, y=u+v+a+a, u=a^2, v=b^2$
et je crois qu'il y a sur le forum un post de Bruno qui explique comment représenter la condition $y=x^2$ avec des mots très simples "règle, équerre"
je n'ai pas oublié, j'ai même passé probablement 1H ce matin à lire les pages 1-16 (et surtout 1-10 et 14-16). Hélas, mes handicaps calculatoires + ma non maitrise de l'anglais m'empèchent de "capter" le truc***. De toute façon ça a tjs été comme ça (je me demande s'il m'est déjà arrivé de lire quelque chose où finalement, je ne vois pas un peu d'avance l'idée des auteurs et où après coup je comprends, voire je me demande s'il m'est déjà VRAIMENT déjà arrivé de lire "quelque chose" :X :X au cours de ces 50 dernières années).
*** le théorème de Sturm, etc, avec les tableaux de signes-variations
Bon, j'abandonne pas, je m'y remettrai, mais, à JLT, la fiche de lecture promise n'est pas pour ce WE (enfin ça m'étonnerait)
Pour moi je crois surtout que le plus torturant pour moi c est ce qui se passe page 9-10 y a des matrices et puis apres des histoires de "leading coefficients" et la mon pauvre anglais . . .
poste de mon tel sorry pour la frappe
Les références en rouge renvoient au document que Ga? mentionne dans le lien nommé "ici" du post http://www.les-mathematiques.net/phorum/read.php?8,773709,774408#msg-774408
Attention: ce qui suit est la suite de http://www.les-mathematiques.net/phorum/read.php?8,773709,775552#msg-775552
On en était à:
il suffit d'écrire (j'appelle cette conrtainte "faire une phrase pauvre") avec des "ou", des "et" des "+" des "×", des "=", des ">" et des coefficients "lettres" des $P_1,..,P_n, Q$ mais pas de quantificateur un énoncé qui exprime $\exists x: P_1(x)>0$ et $P_2(x)>0$ et ... et $P_n(x)>0$ et $Q(x)=0$
20) Il y a deux théorèmes de Sturm détaillés dans le document mis en lien par Ga?
20.1) pour chaque $n\in \N$ une phrase pauvre qui exprime le nombre de racines de $P$ comprises entre $a$ et $b$ est $n$ (theos 1.1 et 1.2 pages 5-6)
20.2) pour chaque $n\in \Z$ une phrase pauvre qui exprime le nombre de racines $x$ comprises entre $a$ et $b$ de $P$ telles que $Q(x)>0$ moins le le nombre de racines $x$ de $P$ telles que $0>Q(x)$ est $n$ (avec une petite précaution que ni a ni b ne doivent être des racines de $P$) (theos 1.5 debut page8)
21) Apparemment leurs démonstrations semblent digérables
22) Partant de là, en faisant une assez grosse comptabilité, on peut parvenir à exprimer sous forme d'une phrase pauvre il y a au moins une racine $x$ de $P$ comprise entre a et b telle que $Q_1>0$ et ... et $Q_n(x)>0$
23) Pour s'en apercevoir, on étudie toutes les phrases pauvres qui expriment le nombre de racines $x$ comprises entre $a$ et $b$ de $P$ telles que $R(x)>0$ moins le le nombre de racines $x$ de $P$ telles que $0>R(x)$ est $n$ où $R$ varie sur l'ensemble fini des polynomes de la forme $(-1) ^{s(1)}Q_1....(-1) ^{s(n)}Q_n$ quand $s$ est une application de $\{1;...;n\}$ dans $\{1;2\}$ (stratégie expliquée et contenue dans lemme 1.8 page 9)
24) Puis on peut conclure, vu qu'il suffit de prendre (de manière effective) un $a$ assez proche de $-\infty$ et un $b$ assez proche de $+\infty$ (le "assez proche" étant facile à deviner à partir des coefficients dominants)
J'avais retenu que le fait que $\mathbb{C}$ soit algébriquement clos, reposait sur des keutrus, oulala, de l'analyse, un autre keutru quoi. Genre un polynôme du troisième degré admet au moins une racine réelle.
On en est où maintenant ?
je précise qu'avant d'écrire ce post, j'ai relu le livre "Comment parler d'un livre que l'on a pas lu ?".
S
Oui: Hourya Sinaceur - Corps et Modèles - Collection Mathesis chez Vrin - Janvier 1991 (il valait quand même 198 F à l'époque !).
C'est là aussi que j'ai vu pour la première fois ce théorème.
Cordialement,
Rescassol
0) Connaissez-vous les mots "récursives", "décidables"?
1) Avez-vous bien compris pourquoi (dans le contexte présent), parvenir à "éliminer les quantificateurs" rend la théorie récursive (on dit aussi décidable, mais c'est un abus de langage)?
2) Avez-vous bien compris pourquoi il suffit d'éliminer $\exists x$ des $\exists x: (A_1$ et $A_2$ et ... $A_n)$ et les $\forall x$ des $\forall x: (A_1$ ou $A_2$ ou ... $A_n)$
3) Avez-vous bien compris la délicate (triviale mais délicate) rédaction pour dire que ça doit se faire "uniformément en les paramètres"?
4) Avez-vous bien compris la quasi absence de "non" dans cette histoire, ie la présence de prédicats (par exemple comme $=; >; etc$) atomiques qui permettent de se passer de "non"?
5) Avez-vous bien compris comment c'est assez "routinier" pour $\C$? (J'ai eu la flemme d'écrire why les zéros communs aux $P_i$ sont tous des zéros de $Q$ ssi $Q$ mis à une puissance suffisamment grande est un multiple du PGCD des $P_i$?
5.1) En particulier avez-vous bien compris comment on remplace sans insister des A=>B par des "nonA" ou B, etc?
6) Avez-vous bien compris que le cas $\R$ est nettement plus difficile et semble nécessiter le théorème de Sturm (qui n'est pas une mince affaire) et est traité soigneusement en 20 pages dans le lien mis par Ga? ?
7) Avez-vous bien compris pourquoi quitte à rajouter des "et" et des "ou", on peut écrire uniformément en les paramètres un énoncé $E$ sans quantificateurs a par exemple la propriété que: $\forall a_1,...,a_n [($ les zéros communs aux $X\mapsto P_i(a_1,..,a_n, X)$ sont tous des zéros de $X\mapsto Q(a_1,..,a_n,X))\iff E(a_1,..,a_n)]$
8) Avez-vous bien compris pourquoi ça implique que la géométrie est "décidable"?
J'avais posé la question parce que ça me turlupinait un peu l'idée d'éliminer non pas UN "il existe x", mais d'un coup tous les " $\exists x_1,\exists x_2..,\exists x_n$" à la file dans une succession de quanteurs
Ca semble peu probable qu'il y ait quelque chose de ce genre qui soit possible pour donner une sorte de "toute autre" preuve du même résultat (récursivité de la théorie de $\R$ )
En fait, je pensais aux points $(x,y)$ qui minimisent $|P(x,y)|$[/size]
En fait, tu veux dire qu'on "joue sur l'ensemble vide"? ie qu'on remplace "$ \{(x,y) | P(x,y)=0\}\neq \emptyset$ par "tel calcul différentiel qui cherche un minimum dans cet ensemble dont on ignore s'il est vide le trouve?" (c'est rigolo ça, je comprends mieux tes rappels sur l'ensemble vide maintenant -D )
10 paressent 10 contre 1
S
De quel énoncé de Bouzar s'agit-il ?
Merci
je reviens à deux questions de la FAQ de Christophe, que je vous demande de bien vouloir l'expliquer car pour l'instant je ne comprends pas :
1) Avez-vous bien compris pourquoi (dans le contexte présent), parvenir à "éliminer les quantificateurs" rend la théorie récursive (on dit aussi décidable, mais c'est un abus de langage)?
2) Avez-vous bien compris pourquoi il suffit d'éliminer $\exists x$ des $\exists x: (A_1$ et $A_2$ et ... $A_n)$ et les $\forall x$ des $\forall x: (A_1$ ou $A_2$ ou ... $A_n)$
merci