Gödel, ta démo ne me convainc pas.

[Argyre]

Un peu de sarcasme dans le titre de ce fil !

Je voudrais soulever ici la question de la pertinence de la démonstration de Gödel pour aboutir à son théorème concernant l'incomplétude.

Il y a notamment un point que j'ai du mal à comprendre. A un moment de sa démonstration (je ne connais en vérité qu'une version simplifiée, donc je dois être un peu naïf, pardonnez moi), il est admis qu'il a construit une nouvelle formule qui est "évidemment vraie", alors qu'il est impossible de le démontrer.

Voir par exemple http://membres.lycos.fr/godel/theoreme_plus_pres.html
J'espère que cette présentation reproduit "honnêtement" la démonstration de Gödel. Si c'est le cas, il est écrit à un moment donné :

"La formule de nombre de Gödel g1 est démontrable par la suite de formules de nombre de Gödel g2."
Dans la suite, nous appellerons cette formule G.
...

"n : Il n'existe aucun nombre de Gödel qui représente une suite de formule qui soit la démonstration de la formule portant le nombre de Gödel n ."
Cette affirmation métamathématique (disant que G est indémontrable) est manifestement vraie, comme nous venons de le voir. Et elle est representée par une formule arithmétique, selon la methode de Gödel, qui est donc vraie elle aussi...
Gödel a donc au final construit une fomule arithmétique qui est vraie, et qu'on ne peut pas démontrer en utilisant un système formel de l'arithmétique si celui-ci est consistant.

En fait, il y a une autoréférence gênante, qui pourrait laisser penser que la démonstration d'incomplétude n'est valable que si on autorise cette autoréférence dans les formules. Si on ne l'autorise pas, est-ce que le théorème ne tient plus ? Et donc, dans ce contexte sans autoréférence possible, le système formel de l'arithmétique pourrait être consistant et complet ?

Autre chose, si en autorisant l'autoréférence on obtient quelque chose d'inconsistant, on peut parfois démontrer une formule et son contraire. Mais du coup, que devient le théorème sur l'incomplétude ?

Enfin, si on modifie le système formel de l'arithmétique de la façon suivante : on introduit un nombre entier théorique gamma et la formule suivante : quel que soit x appartient à N, x < gamma
(en gros, on empêche l'accès à l'infini, tout en autorisant les grandes valeurs)
Est-ce que le théorème de Gödel est invalidé ?
(il me semble que oui, car tout peut être démontré par induction, non ?)

[robert et ses amis]

je ne me souviens pas d'énoncés "manifestement" vrais dans la démo de Gödel.

Le résultat d'incomplétude se formule plutôt ainsi : "ou l'arithmétique est inconsistante, ou il y a des énoncés indémontrables dans l'axiomatique considérée".

Une référence peut-être plus pertinente (j'ai pas lu le lien) :
"Le théorème de Gödel" Nagel,Newman,Gödel,Girard éd. du seuil
Ce petit bouquin, contient l'article original de Gödel traduit en français, un texte introductif qui permet de bien se mettre dans la problématique et de mieux comprendre l'article, et enfin un texte intéressant sur les intérprétations du théorème.

[invité576543]

je ne me souviens pas d'énoncés "manifestement" vrais dans la démo de Gödel.

Le résultat d'incomplétude se formule plutôt ainsi : "ou l'arithmétique est inconsistante, ou il y a des énoncés indémontrables dans l'axiomatique considérée".

Bonsoir,

Il y a plein de textes abordables sur la toile. A lire. La formulation ci-dessus n'est pas satisfaisante. Pour une formulation simplifiée, par exemple "Pour toute théorie cohérente qui contient l'arithmétique, il existe au moins un énoncé indécidable". Avec "théorie cohérente" = avec laquelle on ne pas démontrer "faux", et "indécidable" = non prouvable, ainsi que son contraire, dans la théorie.

Une référence peut-être plus pertinente (j'ai pas lu le lien) :
"Le théorème de Gödel" Nagel,Newman,Gödel,Girard éd. du seuil
Ce petit bouquin, contient l'article original de Gödel traduit en français, un texte introductif qui permet de bien se mettre dans la problématique et de mieux comprendre l'article, et enfin un texte intéressant sur les intérprétations du théorème.

J'ai "lu" l'article original, enfin je l'ai vu. Bonne chance! Il vaut mieux lire des bonnes vulgarisations par des logiciens!

Cordialement,

[pi-r2]

Je te conseille cette page web:

http://membres.lycos.fr/godel/en_savoir_plus.html

Mais je te rassures tout de suite, tes interprétations sont fausses.
De manière simplifiée, le théorème de Gödel consiste à écrire une phrase auto référente en arithmétique (que l'on peut écrire, puisque on peut l'écrire si je puis dire), en respectant les règles.
Et cette phrase auto référente est l'équivalent de:
cette phrase est non démontrable

Le raisonnement méta mathématique sur une telle phrase (raisonnement fait hors du système formel) permet de dire: soit la phrase est démontrable dans le système formel (donc vraie) et il y a contraction. Soit elle n'est pas démontrable, donc vraie. Elle est donc toujours vraie.

[Photon]

Gödel, ta démo ne me convainc pas.

Ce serait pas plutot : Gödel, ta démo ne me convient pas

J'ai trouvé ce lien à partir des liens donnés plus haut que je trouve intéressant : Le Hasard des Nombres

"Pour Hilbert et pour la plupart des mathématiciens de l'époque, l'idée que tout problème mathématique possède une solution était un principe qui allait de soi [NDLR: Argyre est-il une réincarnation de Hilbert ? ]. Ce n'est que par la suite qu'Hilbert a reconnu qu'il y avait là un thème à explorer. De cette exploration, il s'est avéré qu'une question mathématique simple et claire ne possède pas toujours de réponse tranchée ; de plus, une certaine forme de hasard intervient même en mathématiques pures, et se rencontre au travers des équations diophantiennes, objet du dixième problème de Hilbert. En effet, nous verrons que certaines questions assez simples d'arithmétique, liées aux équations diophantiennes, ont --- dans un sens bien déterminé --- une réponse complètement aléatoire. Et cela, non pas parce que nous ne pourrons y répondre demain, dans cent ou mille ans, mais parce que la réponse est aléatoire quel que soit le raisonnement utilisé.

....

Avec ces découvertes, les mathématiciens sont en train de rejoindre, en un sens, leurs collègues de la physique théorique. Ce n'est pas nécessairement une mauvaise chose. Dans la physique moderne, le hasard et l'imprévisibilité jouent un rôle fondamental ; la reconnaissance et la caractérisation de ce fait, lequel pouvait être perçu a priori comme une limitation, sont un progrès. J'ai la conviction qu'il en sera de même en mathématiques pures."

[spi100]

J'ai travaillé à partir de ce document

http://www.bun.kyoto-u.ac.jp/~suchii/Logic/goedel.html

Ce m'a paru plutot beaucoup plus clair que ce que j'avais déjà vu sur le sujet.

[Argyre]

Je te conseille cette page web:

http://membres.lycos.fr/godel/en_savoir_plus.html

Mais je te rassures tout de suite, tes interprétations sont fausses.

Quelles interprétations ? Je n'ai posé que des questions m'a t-il semblé !
En plus, en suivant ton lien, j'ai fini par tomber sur : http://nl.ijs.si/~damjan/g-m-c.html#impl
et là, je m'y retrouve parfaitement !

"cette phrase est non démontrable "

Le raisonnement méta mathématique sur une telle phrase (raisonnement fait hors du système formel) permet de dire: soit la phrase est démontrable dans le système formel (donc vraie) et il y a contradiction. Soit elle n'est pas démontrable, donc vraie. Elle est donc toujours vraie.

Franchement, je ne vois pas trop où tu veux en venir. On ne peut prouver ni qu'elle est vraie, ni qu'elle est fausse, car dans les 2 cas on aboutit à une contradiction. En revanche, l'objectif de Gödel a été de trouver une formule vraie et indémontrable (sauf à utiliser les métamathématiques). C'est différent, non ?

[pi-r2]

Franchement, je ne vois pas trop où tu veux en venir. On ne peut prouver ni qu'elle est vraie, ni qu'elle est fausse, car dans les 2 cas on aboutit à une contradiction. En revanche, l'objectif de Gödel a été de trouver une formule vraie et indémontrable (sauf à utiliser les métamathématiques). C'est différent, non ?

Non, les 2 cas ne sont pas symétriques. Cette phrase ne peut pas être fausse.
Si j'arrive à démontrer cette phrase dans mon système formel, elle est donc vraie car démontrée. Or elle dit qu'elle est fausse, il y a contradiction.
Le seul cas où il n'y a pas contradiction c'est si je n'arrive pas à la démontrer. Dans ce cas elle est vraie puisqu'elle dit qu'on ne peut pas la démontrer. Il n'y a pas de contradiction.
Mais la "phrase" construite par Gödel est effectivement différente, cet exemple de vulgarisation est très utilisé mais reste un peu caricatural.

La volonté d'éliminer l'auto référence pour ne pas tomber sous le coup du théorème de Gödel est interessante, mais ne conduit qu'à des systèmes moins puissants (comme la logique booléenne seule qui ne tombe pas sous le coup du théorème de Gödel).


PS:J'avais pris tes questions pour une manière d'interpréter.

[spi100]

(comme la logique booléenne seule qui ne tombe pas sous le coup du théorème de Gödel).

Slt,
Peux - tu développer ce point ?

[Gre]

Si je puis me permettre, j'aimerais apporter quelques petites précisions quand à la démonstration.
Gödel était bien conscient du risque d'autoréférence. C'est pour cela qu'il n'a pas créé une phrase qui dit :
cette phrase ne peut être démontré,
mais une phrase qui dit
La phrase portant le numéro de gödel xxxxx ne peut être démontré
Il se trouve qu'il a aussi créé cette phrase de manière à ce que qu'elle porte le numéro xxxxx. C'est donc par un heureux hasard (si j'ose dire ) que cette phrase se méta-référence à elle-même.
Bien sûr de fait on a que la phrase sus-dite ne peut être démontrable car sinon elle démontrerais que la phrase xxxxx n'est pas démontrable. Hors étant elle même il y aurait contradiction.

Ceci m'amène au deuxième point : cette phrase est eminemment vraie. En effet, je ne peux pas démontrer la phrase xxxxx. En conséquence de quoi la phrase est vraie. Cependant ceci n'est pas une démonstration formelle, mais une métadémonstration. C'est-à-dire que cette démonstration n'est pas une suite de théorème qui sont soit des axiomes soit démontree à l'aide des théorèmes précédents de la suite.

Par la même : on vient de (méta)démontrer qu'on ne peut pas démontrer que cette phrase est fausse, puisqu'on sait qu'elle est vraie. On a là une différence significative avec une phrase comme celle du crétois menteur. A priori rien n'empêchait qu'on puisse démontrer que la phrase de Gödel était fausse, mais sachant que c'est vrai, on ne peut donc le faire.

Ainsi une démonstration formelle n'est pas possible bien qu'on sache qu'elle soit vraie ! Cela montre donc une limite du processus de démonstration formel : certaines phrases sont vraies, mais ne peuvent être démontrée formellement. Ceci sous tend donc qu'il existe des choses qu'on ne peut démontrer formellement.

On venait de briser le rêve hilbertien de mécaniser les mathématiques.

Il faut cependant mettre un bémol là-dessus, car la conclusion ne s'énonce pas aussi facilement que ca. Mais globalement, cela s'avère presque impossible.

[Gre]

Slt,
Peux - tu développer ce point ?

Je pense qu'il parlait de la logique propositionnelle qui est décidable «toute phrase écrite comme une proposition peut-être prouvée ou contredite formellement»

[Argyre]

La phrase portant le numéro de gödel xxxxx ne peut être démontré
Bien sûr de fait on a que la phrase sus-dite ne peut être démontrable car sinon elle démontrerais que la phrase xxxxx n'est pas démontrable. Hors étant elle même il y aurait contradiction.

Ok.

Ceci m'amène au deuxième point : cette phrase est eminemment vraie. En effet, je ne peux pas démontrer la phrase xxxxx. En conséquence de quoi la phrase est vraie.

Là-dessus, je voudrais faire la remarque suivante :
<<en posant l'hypothèse que la phrase était démontrable, on a abouti à une contradiction, et on en a DEDUIT que la phrase était donc non démontrable.>> Mais le raisonnement entre crochet EST un raisonnement tout à fait valable qui peut tenir lieu de démonstration. Et donc, on a (méta)démontré qu'elle était non démontrable. Mais si on l'a démontré ou métadémontré, c'est que la phrase est fausse, il y a à nouveau contradiction !!!

Par conséquent, je conteste que la phrase soit "éminemment vraie" !
Elle me parait indécidable.

Cependant ceci n'est pas une démonstration formelle, mais une métadémonstration.

Je ne vois pas pourquoi le raisonnement entre crochets ne peut pas être considéré comme une démonstration formelle. Il faudra m'éclairer là-dessus.

Par la même : on vient de (méta)démontrer qu'on ne peut pas démontrer que cette phrase est fausse, puisqu'on sait qu'elle est vraie.

En fait, on a aussi métadémontré qu'elle était fausse !
Bref, j'y perds mon latin, faites vos jeux, rien ne va plus !

[Gre]

Là-dessus, je voudrais faire la remarque suivante :
<<en posant l'hypothèse que la phrase était démontrable, on a abouti à une contradiction, et on en a DEDUIT que la phrase était donc non démontrable.>> Mais le raisonnement entre crochet EST un raisonnement tout à fait valable qui peut tenir lieu de démonstration. Et donc, on a (méta)démontré qu'elle était non démontrable. Mais si on l'a démontré ou métadémontré, c'est que la phrase est fausse, il y a à nouveau contradiction !!!
[...]
Je ne vois pas pourquoi le raisonnement entre crochets ne peut pas être considéré comme une démonstration formelle. Il faudra m'éclairer là-dessus.

Une démonstration formelle de T est une suite de théorème (T_i)_{1<=i<=n} telle T_n = T et tout T_i est:
soit un axiome de notre théorie ;
soit une proposition démontrée à l'aide des règles de déductions de la logique formelle sur les T_j avec j<i.

Les régles de déductions de la logique sont des schémas de la forme:
A et A->B permettent de démontrer B
A&B permet de démontrer A
A&B permet de démontrer B
A et B permettent de démontrer A&B
etc.

Je te passe toutes les règles.
Grosso modo une démonstration formelle est codifié sur la syntaxe de ton langage. La démonstration que la phrase est indémontrable n'était pas formelle car elle était sémantique (basée sur des éléments ayant du sens si tu veux). Ainsi on peut démontrer que certaines théories sont consistentes de manière non formelles mais trés mathématiques.

Le problème vient du fait que les gens disent que les mathématiques sont formelles, alors que seule une partie l'est vraiment : être formelle c'est ne porter que sur la forme et non sur le fond, i.e. ne porter que sur la syntaxe et non sur le sens (la sémantique).

Ais je été d'un quelconque secours ?

[Gre]

J'ai rajouté des précisions mais ca m'a mis plus de 5 minutes à repenser alors j'ai été N**é pendant la procédure

Revoilà

Être valable ne veut pas dire être formel. C'est justement là toute la nuance.

Une démonstration formelle de T est une suite de théorème (T_i)_{1<=i<=n} telle T_n = T et tout T_i est:
soit un axiome de notre théorie ;
soit une proposition démontrée à l'aide des règles de déductions de la logique formelle sur les T_j avec j<i.

Les régles de déductions de la logique sont des schémas de la forme:
A et A->B permettent de démontrer B
A&B permet de démontrer A
A&B permet de démontrer B
A et B permettent de démontrer A&B
etc.

Je te passe toutes les règles.
Grosso modo une démonstration formelle est codifié sur la syntaxe de ton langage. La démonstration que la phrase est indémontrable n'était pas formelle car elle était sémantique (basée sur des éléments ayant du sens si tu veux). Ainsi on peut démontrer que certaines théories sont cohérentes de manière non formelles mais trés mathématiques. Tu peux par analogie dire que la vérité syntaxique est donc basée sur la forme de la proposition
[i] \forall_i ((A(i)->B(i+1)) & C(i,i+1))
alors que la vérité sémantique est basé par une projection (interprétation) dans un monde «réel» (un modèle mathématique comme l'ensemble des entiers naturels vu comme un groupe additif).

Le problème vient du fait que les gens disent que les mathématiques sont formelles, alors que seule une partie l'est vraiment : être formelle c'est ne porter que sur la forme et non sur le fond, i.e. ne porter que sur la syntaxe et non sur le sens (la sémantique).

Revenons à la décidabilité : si une démonstration formelle de toute véritée sémantique existait dans un modèle en particulier, on pourrait déterminer de manière mécanique si une proposition est vraie ou est fausse dans un modèle juste en analysant la validité syntaxique (la forme). On aurait donc une propriété de décidabilité : toute proposition peut-être analysée formellement (syntaxiquement) pour déterminer si elle est vrai ou fausse.
Conclusion: un ordinateur pourrait un jour découvrir la véritée mathématique par simple énumération de possibilités. Ca peut paraître terrifiant ou au contraire merveilleux. Mais de toute façon, Gödel a mis fin à ca.


Être valable ne veut pas dire être formel. C'est justement là toute la nuance.

Une démonstration formelle de T est une suite de théorème (T_i)_{1<=i<=n} telle T_n = T et tout T_i est:
soit un axiome de notre théorie ;
soit une proposition démontrée à l'aide des règles de déductions de la logique formelle sur les T_j avec j<i.

Les régles de déductions de la logique sont des schémas de la forme:
A et A->B permettent de démontrer B
A&B permet de démontrer A
A&B permet de démontrer B
A et B permettent de démontrer A&B
etc.

Je te passe toutes les règles.
Grosso modo une démonstration formelle est codifié sur la syntaxe de ton langage. La démonstration que la phrase est indémontrable n'était pas formelle car elle était sémantique (basée sur des éléments ayant du sens si tu veux). Ainsi on peut démontrer que certaines théories sont cohérentes de manière non formelles mais trés mathématiques. Tu peux par analogie dire que la vérité syntaxique est donc basée sur la forme de la proposition
[i] \forall_i ((A(i)->B(i+1)) & C(i,i+1))
alors que la vérité sémantique est basé par une projection (interprétation) dans un monde «réel» (un modèle mathématique comme l'ensemble des entiers naturels vu comme un groupe additif).

Le problème vient du fait que les gens disent que les mathématiques sont formelles, alors que seule une partie l'est vraiment : être formelle c'est ne porter que sur la forme et non sur le fond, i.e. ne porter que sur la syntaxe et non sur le sens (la sémantique).

Revenons à la décidabilité : si une démonstration formelle de toute véritée sémantique existait dans un modèle en particulier, on pourrait déterminer de manière mécanique si une proposition est vraie ou est fausse dans un modèle juste en analysant la validité syntaxique (la forme). On aurait donc une propriété de décidabilité : toute proposition peut-être analysée formellement (syntaxiquement) pour déterminer si elle est vrai ou fausse.
Conclusion: un ordinateur pourrait un jour découvrir la véritée mathématique par simple énumération de possibilités. Ca peut paraître terrifiant ou au contraire merveilleux. Mais de toute façon, Gödel a mis fin à ca.

[spi100]

Revenons à la décidabilité : si une démonstration formelle de toute véritée sémantique existait dans un modèle en particulier, on pourrait déterminer de manière mécanique si une proposition est vraie ou est fausse dans un modèle juste en analysant la validité syntaxique (la forme). On aurait donc une propriété de décidabilité : toute proposition peut-être analysée formellement (syntaxiquement) pour déterminer si elle est vrai ou fausse.
Conclusion: un ordinateur pourrait un jour découvrir la véritée mathématique par simple énumération de possibilités. Ca peut paraître terrifiant ou au contraire merveilleux. Mais de toute façon, Gödel a mis fin à ca.

Ca je le comprend bien dans le cadre des machines de Turing. Turing montre qu'il est impossible de trouver une machine capable de décider si un programme s'arrête ou non, simplement en regardant sa syntaxe.

Supposons qu'un tel programme H existe. Je pourrais alors considérer n'importe quelle formule existentielle, la traduire sous forme numérique f(n) = 0 et écrire un programme P de la forme

for (i = 0; ; ++i ) {
if ( f(i) == 0 ) then return;
}

Je demanderais alors à mon halting programme H : "est - ce que la syntaxe de ce programme est celle d'un programme qui s'arrête ?" Si oui, alors la proposition existentielle serait vraie, sinon elle serait fausse.
La conclusion irrémédiable serait que toute la sémantique serait réduite à la syntaxe, puisque la seule considération de la forme du programme permettrait de déterminer la vérité d'une proposition.