la machine à démontrer (science-fiction)

Bonjour, cher Stramoine et cher Bruno.

Sauf erreur de ma part, il semble que l'on a enfin prouvé que toute démonstration mthématique est "programmable" dans un langage informatique suffisamment complexe.

J'écoutais cela il y a quelques années sur France Culture.
Le conférencier s'empressa d'ajouter que, par contre, on ne savait toujours pas ce qu'était une démonstration.

Cherchez l'erreur.

Cordialement.

Bruno a écrit:

Par contre, le calcul propositionnel est décidable.

... en temps exponentiel 8-)

Je crois que par "démonstration programmable" il faut comprendre que l'on donne la démonstration au logiciel, par exemple coq, et qu'il vérifie qu'elle est correcte. C'est particulièrement intéressant pour des preuves de programmes "critiques".

Ce genre de logiciel permet aussi de construire automatiquement des programmes satisfaisant certaines conditions. Typiquement, si on part d'une propriété mathématique de la forme :
$$\forall x,\exists y,P(x,y)$$
et qu'on en donne une preuve constructive au logiciel (c'est à dire sans utiliser le tiers exclu, il y a peut-être d'autres conditions à satisfaire, je ne me rappelle plus très bien), il peut extraire de la preuve un programme qui prend en entrée x et qui calcule le y qui convient. Cette correspondance entre preuves constructives et programmes s'appelle l'isomorphisme de Curry-Howard.

Non, par exemple il suffit de prendre une proposition P indécidable dans ZFC (au sens : ni P ni son contraire ne sont démontrables) et considérer Q=(P ou (non P)). Q est démontrable (tiers exclu) mais si on savait démontrer P sans le tiers exclu on obtiendrait soit une démonstration de P, soit une démonstration de (non P).

D'ailleurs ces logiciels ne travaillent pas avec ZFC il me semble, mais je ne saurais plus dire quel est le formalisme utilisé par coq.

Bonne question, cher Bruno, à laquelle a répondu AlexB, que je salue.

La vérité est que je suis un béotien en logique et en informatique.

J'ai voulu jouer les petits malins en me contentant de répéter vaguement un extrait d'une émission de France Culture.

Et pan sur mon bec !

GERARD à la maison a écrit:

il reste un problème : Comment va-t-on savoir que la dernière démonstration donnée par la machine est celle du théorème de Fermat (On ne sait pas la lire dans le formalisme machine

Déjà en français ça doit être chaud...

Oui, moi je répondais simplement au message de Bruno en fait, car je pensais qu'il pouvait y avoir confusion entre vérifier et générer justement !

Effectivement, il y a un lien entre la conviction de Hilbert et le théorème de Godel. En effet, si l'on suppose que pour tout énoncé P, soit P est démontrable, soit non P l'est, alors il suffit d'énumérer toutes les démonstrations possibles (après tout ce ne sont que des textes de longueur finie vérifiant certaines conditions syntaxiques) et de s'arrêter dès que l'on en trouve un dont la conclusion est soit P soit non P.

Le théorème d'incomplétude de Godel met un terme à cet espoir puisqu'il existe, dans tout système mathématique suffisamment puissant, des énoncés P qui ne sont ni démontrables, ni réfutables.

Merci ! Mais je ne me qualifirai pas de logicien. C'est juste que le DEA d'info que j'ai fait touchait un peu à la logique et ces question m'intéressaient...

(hors-sujet pour Christophe Chalons : je n'ai pas eu le temps de le dire, mais je trouve que tu as eu tout à fait raison dans ta dernière intervention sur le fil de GF et ses "cardinaux".
Seule une verbalisation orale pourrait faire évoluer cette situation.
Tu vois que, des fois, je ne suis pas sans coeur..;))

ooooh merci Aleg (j'ai cherché un coeur géant dans les smileys, mais ya pas... Manque de smileys ce forum)

à mt-i tu dis on imagine généralement qu'ils sont décidables dans les formalisations courantes des mathématiques

Je changerai qu'un mot:

on espère généralement qu'ils sont décidables dans les formalisations courantes des mathématiques

On ne dispose pas spécialement de raisons d'y croire

On a sans doute rarement des raisons très fortes, mais enfin expérimentalement, on a plus ou moins une idée de ce à quoi ressemblent en général les énoncés qui nécessitent l'axiome du choix, tel axiome de grands cardinaux ou encore l'hypothèse du continu. Ils ont tendance à avoir une certaine tête. Alors on peut avoir des surprises bien sûr, et la famille des exemples qui façonnent l'idée qu'on se fait de l'intervention de tel ou tel type d'axiome évolue au fil de ces surprises. Mais quand même, si RH est indécidable dans ZFC, je veux bien te payer un verre :-).

mais enfin expérimentalement, on a plus ou moins une idée de ce à quoi ressemblent en général les énoncés qui nécessitent l'axiome du choix, tel axiome de grands cardinaux ou encore l'hypothèse du continu. Ils ont tendance à avoir une certaine tête. Alors on peut avoir des surprises bien sûr, et la famille des exemples qui façonnent l'idée qu'on se fait de l'intervention de tel ou tel type d'axiome évolue au fil de ces surprises. Mais quand même, si RH est indécidable dans ZFC, je veux bien te payer un verre :-).

oups, désolé de décevoir quelque chose peut-être sur quoi tu t'appuies, mais là, tu viens de "commettre" un archétype d'erreur (les suites du théorème de Godel n'ont pas été assez "médiatisées"): l'indécidabilité des énoncés n'est pas relié à leur place dans l'échelle de complexité

Pour parler moins crument: ça commence au niveau des équations diophantiennes. Il y en a plein qui sont indécidables. RH peut se traduire, je crois, en un énoncé arithmétique équivalent à une équation diophantienne (si RH est faux, elle aura des solutions, si RH est vrai, elle n'en aura pas), et de ce fait appartient à la famille d'énoncés le moins complexes.

L'indécidabilité n'est pas en rapport avec la puissance de la théorie: ZFC, et même ZFC avec plein de grand cardinaux laisse irrésolu la plupart des équations diophantiennes!!!!!

La "consistance de ZFC" par exemple se traduit en une équation diphantienne (elle a des solutions si et seulement si ZFC est contradictoire).

Cela dit, je ne pourrai jamais vous prouver l'indécidabilité de RH car elle est équivalente à sa vérité (si je me trompe pas en ce qui concerne son équivalence avec une equa dioph)

{\it

ça ça nécessite l'axiome du choix, ça ça nécessite un axiome de grand cardinal, et ainsi de suite.

}

L'argumentation de Godel est dynamique et s'applique {\bf à tous les énoncés} (dans une certaine mesure). C'est d'ailleurs une erreur "honorable" de ne pas en avoir conscience à temps plein puisqu'elle est "commise" par le "maitre" (H.Woodin) de la théorie des ensembles dans plusieurs conférences (dans lesquelles ils déclarent "telle théorie T doit résoudre tous les problèmes de tel type, {\bf aux énoncés godéliens près}".

C'est une image intuitive, bien sûr que tu fais, que Woodin fait...

{\it Soit $e$ l'ensemble des $x$ tels que l'énoncé $x\notin x$ est prouvé à l'aide d'axiomes non godéliens.

Manifestement, les raisons qui font de $e\notin e$ un énoncé "godélien" ne sont pas godéliennes. Il suffit juste de remarquer qu'on est en plein délire godélien. Dès lors, il semble assuré sans godélite que $e\notin e$. Ce qui atteste que $e\in e$. }

En fait, pour éviter toute confusion dans ce domaine, voilà comment il faut voir les choses:

Il faut se dire que la logique a découvert que rien n'est absolu-absolu. Il y a des degrés. Les "godélites" donnent des indications, partielles seulement, sur le niveau de certitude qu'un raisonnement procure. Aucune preuve de A dans aucune théorie T ne décide vraiment A tout seul, mais plutot un certain énoncé "Ceci entraine A" où, généralement le "ceci" est une conjonction de choses décrétées vraies (le plus souvent parce qu'elle sont toutes dans un même système d'axiomes officiel).

Dès lors, le fait même de dire que RH est décidable dans ZFC n'avance à rien et n'a pas beaucoup de sens: car il faut voir la preuve "d" de RH dans ZFC qui sera proposée. Il faut "juger sur pièce" en quelque sorte. Si quelqu'un t'amène une preuve "d" de RH dans ZFC et que quand tu la lis, tu te rends compte que cette preuve "d" peut se trafiquer en une preuve "d'" du faux qui attestera que ZFC est contradictoire tu ne seras guère avancé. Une croyance de la forme "il existe une preuve "d" dans ZFC de RH" est très claire et n'exclut pas cette éventualité. Et je suppose que tu te doutes de ce que je te répondrais si tu disais "oui, mais on suppose que ZFC n'est pas contradictoire"

La seule question qui vaille d'être posée est "existe-t-il une preuve convaincante de RH?" (dans quelque système que ce soit, peu importe), et celle-ci, elle n'a pas de traduction suffisamment formelle pour qu'on puisse dire qu'on "devine" la réponse, et en fait elle n'a pas de valeur de vérité absolue.

Un exemple de ce petit jeu t'est donné par ce qui suit:

on dit que des axiomes vérifient $A<B$ quand il est prouvable que $A$ entraine l'existence d'un monde vérifiant $B$ (on ne se préoccupe même pas de ce que ça veut dire), c'est un énoncé du genre $A\to \exists x B^x$ dont les logiciens sont familiers.

Placons-nous dans une théorie (c'est un argument très général, une théorie donnée par un axiome G) capable de distinguer des "étages" bien ordonnés (qu'elle veut être bien ordonnés), et qui décrète que seuls les axiomes possédant des mondes à un de ces étages existent.

(C'est le genre de critère incontournable dans toutes les maths)

Si $G<G$ alors dans un modele de $G$ il y aura un "premier" étage qui contient des modeles de $G$ (mondes vérifiant G pouir parler plus volontairement vaguement). Par "definition" (que je n'ai pas donnée) d'un étage, si un étage $e$ est le premier à contenir un modele (disons $m$) de $G$ alors, comme $G$ implique qu'il existe des $x$ tels que $G^x$, il y a dans $m$ des $x$ qui sont des modeles de $G$ et qui devraient, si les choses étaient bien faites se trouver dans des étages inferieurs à $e$.


Je vais être plus concis. Si tu connais les ordinaux ça va aller très vite, il semble impossible de concilier plusieurs désirs, pourtant légitimes:

Soit $\alpha$ le premier ordinal à partir duquel, pour tout $A$ {\bf acceptable}
s'il existe un modele $m$ (ou n'importe quoi qui ait une hauteur) de l'énoncé $A$ alors il en existe un de hauteur inférieure à $\alpha$.

Si tu considères n'importe quelle traduction $B(\alpha)$ de l'énoncé que je viens d'écrire, et si tu considères comme "acceptable" (qu'il soit vrai ou non) l'énoncé $\exists \alpha B(\alpha)$ alors tu auras des soucis. Formaliser n'y changera rien.

Autre exemple: soit $E$ une équation diophantienne.

1) si une théorie trop forte $T$ prouve "$E$ n'a pas de solution" ça ne te garantit pas du tout que c'est vrai car peut-être cette preuve n'est pas "assez courte" pour être "réelle".

2) si une théorie trop forte $T$ prouve "$E$ a des solutions" ça ne te garantit pas du tout que c'est vrai car peut-être cette preuve n'est pas "assez courte" pour être "réelle", et si elle est courte, peut-être n'est-elle pas assez "constructive" pour te donner des solutions, en le sens très précis suivant qu'on n'a aucune garantie "interne" à T qu'il existe des modeles de T dans lesquels l'ensemble des entiers est le "vrai".


Voilà pourquoi je te disais qu'on {\bf espère} sans avoir aucun arguments, que les énoncés un peu classiques sont abordables (résolubles) par les axiomes classiques

Non, on rencontre une sorte de malentendu (mais enfin, en me relisant j'avoue ne pas avoir été clair)...

J'en reviens à ma remarque de départ: aucun argument ne semble autre chose que qualifiable par le mot "espoir", "espérer": tu {\it espères} que RH est démontrable.

C'est tout ce que je disais... Après, en fait je disais, en quelque sorte {\it et en plus, ça a été prouvé (Godel) qu'on ne peut avoir plus}. Mais enfait peu importe: faibles ou fort l'apport de Godel est en plus, {\bf c'est tout}. Il ne peut quand-même pas être mis à décharge de l'idée que l'existence d'une preuve dans ZFC ou ailleurs n'est pas garanti, en général...

Tu apportes un "témoignage" perso {\it je n'ai jamais vu d'énoncé de ce genre qui soit indécidable dans ZFC} qui fonde ton "espoir". Aucun désaccord avec toi sur cette démarche personnelle. Mais en platonicien que tu prétends être, tu ne peux par contre pas "décider" (au sens capricieux du terme) si la réponse est oui ou non (que ZFC démontre RH)...

{\bf Par ailleurs, ça c'est très important, il se peut qu'il soit "vrai" que ZFC démontre RH, sans pour autant qu'il existe une démonstration de longueur "acceptable" (finie), en ce sens très vicieux que peut-être que dans la théorie Z (pas de schéma de substitution) on peut prouver (humainement et formellement) que tous les modèles de ZF vérifient RH}

Bref... Le sens de mon post un peu confus était surtout pour tirer la couverture dans un sens pas assez souvent, à mon avis, affiché: il y a une sorte de connexité dans les phénomènes mathématiques. Il semble qu'un jour, en un certain sens, on passera du "vrai" au faux" sans "lever le stylo" (je parle sérieusement: d'ailleurs il y a une vieille tradition qui consistait à prendre $0=1$ comme axiome de grand cardinal se trouvant tout en haut de la hiérarchie). Dès lors, croire ou ne pas croire à l'existence de preuves dans des théories assez fortes n'est pas important. RH étant pi 0-1, c'est peut-être ça le plus crucial, à savoir que {\bf c'est une équation diophantienne, dont on prétend qu'elle n'a pas de solution} et dès lors, les raisons de "croire" ou non à RH sont multiples (pas besoin de se demander si telle ou telle théorie la démontre)

Contrairement à ce qu'une mauvaise littérature a répandu comme idées, le théorème de Godel {\bf n'est pas} crucialement contenu dans le fait d'avoir réussi à construire des codages: ces codages ont juste servi à faire passer le théorème à la postérité (un bon coup de lemme chinois, il fallait ça pour entrer à l'académie), mais le "fond" de l'histoire est que

des phrases comme "je suis indémontrable" etc, {\bf ont une sens mathématique} (comme d'ailleurs chacun le sent, c'est une évidence que le sens de cette phrase ne dépend que du sens du mot "démontrable") et sont {\bf très différentes} de phrases comme "je suis fausse", etc qui {\bf n'ont pas de sens mathématique} car le mot "faux" n'a pas de sens mathématique.