Comments on Merci de ne pas faire dire n'importe quoi à Gödel !

Alfred (2020-01-08T04:43:26Z)

Pardon, la ligne de vous que je cite
"(mais dans ce cas, il faudra la supposer cohérente, ce que ZFC lui-même ne peut pas prouver,…)"
n’est pas dans ce post mais dans un autre post de votre blog
http://www.madore.org/~david/weblog/d.2016-11-29.2410.html#d.2016-11-29.2410

auquel vous faites référence dans celui-ci, à propos de la version de Turing que vous jugez moins dangereuse. C’est sur cet autre post plus ancien que j’aurais dû poser ma question, et non ici, mais ici ou là-bas, votre réponse m’intéresse.

Alfred (2020-01-07T18:31:16Z)

Je remarque un détail. Concernant ZFC, vous dites : "(mais dans ce cas, il faudra la supposer cohérente, ce que ZFC lui-même ne peut pas prouver,…)" Certes, après tout ce temps, si ZFC n'était pas cohérent, on aurait dû s'en rendre compte. Cependant, par principe, il faut admettre la possibilité, fût-elle infime, que ZFC ne soit pas cohérent. Mais vous ne dites PAS la même chose de PA, alors qu'en principe, la situation est exactement la même.
Est-ce significatif ?

Ryusenshi (2019-09-21T16:35:52Z)

> - Cet énoncé est nécessairement vrai (car s’il était faux,
> il serait démontrable, ce qui est absurde).
> - Il est donc vrai et non démontrable.
> - Est-ce qu’on ne vient pas pourtant d’en fournir une démonstration (par l’absurde) ?

Un peu tardivement, mais j'aimerais être sûr d'avoir compris. C'est plus ou moins ce raisonnement qui sert à démontrer le second théorème d'incomplétude, non?

Soit un système logique S, vérifiant les trois conditions déjà vues (S est un système de la logique du premier ordre, récursivement axiomatisé, contenant l'arithmétique). Ajoutons une hypothèse supplémentaire: S contient l'affirmation « le système S ne démontre aucune contradiction », que j'appellerai affirmation C (c'est peut-être un axiome, ou le résultat d'une démonstration, peu importe). Alors S est inconsistant. Esquisse de démonstration:
- D'après les trois conditions, on peut appliquer le premier théorème d'incomplétude: il existe dans le système S une affirmation G qui dit « il n'existe pas de démonstration de G dans le système S ».
- Moyennant quelques détails techniques, le raisonnement de C.D. peut être alors formalisé dans le système S:
* Supposons non-G;
* ça veut dire qu'il existerait une démonstration de G dans S;
* c'est justement le contraire de ce que dit G:
donc on aurait montré non-G dans S;
* or, selon l'affirmation C, S ne peut pas démontrer à la fois G et non-G;
* c'est absurde.
* Donc G.
- Mais alors, ça veut dire que S démontre G. Donc S affirme à la fois qu'il existe une démonstration de G (on vient de le voir), et qu'il n'en existe pas (puisque c'est ce que G affirme). Donc S n'est pas consistant.

Mais sans l'affirmation C, on ne peut pas tenir ce raisonnement dans S lui-même! Si S ne "sait pas" lui-même qu'il est consistant, alors « S démontre G » et « S démontre non-G » ne sont pas pour lui des contradictions, donc il ne peut pas finir le raisonnement par l'absurde, et donc il n'arrive pas à démontrer G.

Conclusion: si un système (du premier ordre, récursif, contenant l'arithmétique) est consistant, il ne peut pas lui-même affirmer sa consistance.

> À un certain niveau, la question devient « l'intuition est-elle plus puissante
> que la rigueur si l'intuition ne se plante pas ? », et la réponse est
> « certes, si on ne se plante pas, mais la seule façon fiable de ne pas
> se planter, c'est, justement, la rigueur ».

Ça me fait penser à un kôan: "It can't be found by seeking, but only seekers will find it". (Recherche faite, ça vient d'un philosophe perse, Bayazid Bastami, et pas du zen.)

C.D. (2019-09-16T19:55:31Z)

Réponse tout en finesse.

Primat de l’intuition dans l’absolu (mais pas toujours fiable dans la pratique), rôle indispensable du formalisme dans la pratique (mais second dans l’absolu) pour étayer et confirmer l’intuition.

Reste une porte ouverte pour la possibilité théorique d’une éventuelle intuition parfaitement rigoureuse.

Comme ça, ça me va. C’est raccord avec ma petite philosophie des maths…

Merci infiniment.

Ruxor (2019-09-16T16:50:12Z)

@C.D.: Le problème est que la seule façon qu'on sache éviter « soigneusement » l'auto-référence (et encore, certains types d'auto-réference, puisque le théorème de Gödel est justement construit sur une auto-référence licite, et toute la subtilité est de voir qu'elle est licite !) est de formaliser le raisonnement. À un certain niveau, la question devient « l'intuition est-elle plus puissante que la rigueur si l'intuition ne se plante pas ? », et la réponse est « certes, si on ne se plante pas, mais la seule façon fiable de ne pas se planter, c'est, justement, la rigueur ».

C.D. (2019-09-16T13:16:16Z)

Merci à nouveau pour vos réponses.

Permettez-moi de décortiquer encore un peu la question car ça fait pas mal d’années qu’elle me travaille (pas tous les jours, heureusement…).

Les paradoxes que vous évoquez ont pour point commun de s’appuyer sur une auto-référence :

- Dans le paradoxe de Berry, la définition de l’entier fait référence à la définition de ce même entier.

- Dans le paradoxe du menteur, l’affirmation du menteur fait référence à cette même affirmation.

- Dans le paradoxe de Russell, un ensemble est susceptible d’appartenir (ou non) à lui-même, donc la relation d’appartenance est conçue au départ comme étant auto-référente. Les éléments constitutifs (ou non) d’un ensemble font référence à l’ensemble lui-même. Je veux dire par là que même lorsque l’on écrit que x n’appartient pas à x, il y a quand même auto-référence. L’auto-référence vient en fait de la nature même de la relation binaire qui pioche ses deux arguments dans le même sac.

D’où la conclusion suivante :

Le raisonnement informel, lorsqu’il est « bien fondé » (c’est-à-dire lorsqu’il évite soigneusement l’auto-référence) est plus puissant que le raisonnement formel.

Comme ça, ça fonctionne ?

Ruxor (2019-09-13T17:42:15Z)

@Vicnent: 😭

Vicnent (2019-09-13T14:19:23Z)

<URL: https://towardsdatascience.com/an-obscure-mathematical-theory-and-the-consciousness-debate-in-ai-424f5f95ada />

Ruxor (2019-09-02T12:25:13Z)

@C.D.: Ah oui, j'oubliais de répondre, mais je vais faire la même réponse que f3et : le problème avec le raisonnement « informel », c'est qu'il tombe très rapidement sur plein de paradoxes (du menteur, de Russell, etc.) et que la seule façon de les exorciser est de passer à un raisonnement formel… du coup, savoir si on y perd en puissance n'est pas une question bien définie : on n'a juste pas le choix. Évidemment, une baguette magique qui permettrait de raisonner informellement sans paradoxes serait plus puissante, mais à ce compte-là autant souhaiter une baguette magique qui permet directement de savoir ce qui est vrai ou faux !

f3et (2019-09-02T08:55:33Z)

C.D. : En fait, le raisonnement informel est plutôt un bon moyen de créer des paradoxes insolubles, comme l'entier défini par Berry (ou peut-être Russel) comme "le plus petit entier non définissable par une phrase de moins de cinquante mots" (cela dit, étrangement, tout paradoxe de ce type peut être converti en un théorème parfaitement rigoureux, et souvent important)

C.D. (2019-08-29T05:51:47Z)

Merci pour ta réponse.

La conclusion suivante te semble-t-elle pertinente :

Le théorème de Gödel illustre le fait que le raisonnement informel est par nature plus puissant que le raisonnement formel (au sein d’une théorie vérifiant les trois hypothèses indispensables au théorème de Gödel).

En effet, on pourra toujours démontrer de façon informelle un énoncé de Gödel d’une théorie T, alors qu’on ne peut pas le faire formellement à l’intérieur de la théorie T.

Si d’aventure on trouve une théorie T’ extérieure à T et plus puissante qu’elle, qui permette de conclure que les théorèmes de T sont vrais, on recommence avec T’ : on construit un énoncé de Gödel dans T’, non démontrable formellement dans T’, et on prouve de façon informelle qu’il est vrai. Etc.

Autrement dit, on ne pourra jamais formaliser totalement le raisonnement informel. Il a toujours un coup d’avance.

Ruxor (2019-08-28T11:47:56Z)

@Vicnent: Tu rigoles, mais la question a vaguement un sens (au moins si on la comprend comme : y a-t-il un analogue du théorème de Gödel pour des logiques qui ne vérifient pas le théorème de compacité ?).

@C.D.: On peut tout à fait démontrer le théorème de Gödel dans le cadre formel rigoureux dont il énonce lui-même l'incomplétude (notamment, l'article de Gödel de 1931 se place dans le cadre des Principia Mathematica pour démontrer le fait que si les Principia Mathematica sont cohérents alors ils sont incomplets). Il faut évidemment faire attention à ce qu'on dit, et être bien précis. Le raisonnement informel est essentiellement celui que tu énonces (la difficulté est de le formaliser avec précision, de se convaincre qu'il se passe bien et qu'on ne dit pas de bêtise) : la subtilité dans le raisonnement c'est que, même si ça peut sembler évident, la théorie T ne peut pas conclure que les théorèmes de la théorie T sont vrais (essentiellement parce que la logique du premier ordre ne permet de manipuler la notion de vérité que de façon très limitée, ce qui est nécessaire pour éviter des paradoxes comme celui du menteur/crétois), donc vu d'une théorie extérieure qui peut conclure que les théorèmes de T sont vrais, le raisonnement que tu tiens est correct et permet de démontrer (dans cette théorie extérieure plus puissante) l'énoncé indémontrable (dans la théorie T considérée), mais on ne peut pas le tenir dans T, et c'est bien le genre de subtilités qui rendent le théorème intéressant.

C.D. (2019-08-28T05:34:51Z)

Dans le même ordre d’idée, lorsque tu évoques l’énoncé : « Cet énoncé n’est pas démontrable » :

- Cet énoncé est nécessairement vrai (car s’il était faux, il serait démontrable, ce qui est absurde).

- Il est donc vrai et non démontrable.

- Est-ce qu’on ne vient pas pourtant d’en fournir une démonstration (par l’absurde) ?

C.D. (2019-08-28T03:37:05Z)

Question(s) d’un éternel néophyte sur ce sujet : lorsque tu dis que la « preuve » du théorème de Gödel est quasiment triviale, ou encore que sa « démonstration » est très simple, les mots « preuve » et « démonstration » ont-ils un sens rigoureux dans ce cas-là, sont-ils utilisés là aussi dans un cadre formel ? Et si oui, y a-t-il complétude ou incomplétude à l’intérieur de ce cadre ? Les notions de complétude et d’incomplétude ont-elles d’ailleurs un sens à ce niveau de langage là ?

Vicnent (2019-08-28T01:30:52Z)

Est ce que Gödel peut fonctionner dans le cas non compact ?

Ruxor (2019-08-27T22:46:20Z)

@Ilia:

Sans l'hypothèse de contenir l'arithmétique, effectivement, on peut donner des systèmes assez triviaux (même si la notion de complétude n'est pas forcément bien définie dans le système pq- de Hofstadter tel que je me le rappelle vu que je crois me souvenir qu'il n'y a même pas de négation dans l'histoire, et je n'ai pas le livre sous la main pour vérifier). Mais on peut faire un chouïa moins trivial : un exemple assez standard est la théorie des corps réel-clos (les axiomes sont ceux d'un corps totalement ordonné + le fait que tout élément positif a une racine carrée + le schéma d'axiomes évident qui dit que tout polynôme de degré impair a une racine ; les théorèmes sont les énoncés vrais dans un, et automatiquement dans tout, corps réel-clos, et tout énoncé ou sa négation est un théorème).

Sans l'hypothèse d'axiomatisation calculable, on peut effectivement prendre tous les énoncés vrais de l'arithmétique comme axiomes.

Sans l'hypothèse du premier ordre, c'est surtout que la question n'a plus vraiment de sens, parce qu'on ne sait pas exactement de quoi on parle. Si on considère la logique du second ordre (où on peut quantifier sur les prédicats et pas juste sur les objets), il n'y a plus de théorie de la démonstration évidente… mais si on comprend « découle des axiomes » comme « vrai dans tout modèle [modèle “plein”] où les axiomes sont vérifiés » (conséquence sémantique — par opposition à « syntaxique » ce qui sous-entend une notion de démonstration), alors les axiomes de Peano du second ordre (c'est-à-dire que l'axiome de récurrence est formulé pour tous les prédicats) ont pour seul modèle le modèle naturel ℕ, et leurs conséquences (sémantiques) sont donc exactement les énoncés vrais de ℕ, donc ils sont complets. Mais on pourrait aussi parler d'autres logiques (par exemple des logiques infinitaires ; il me semble que le théorème de complétude de Barwise doit permettre de fabriquer assez facilement des systèmes d'axiomes qui définissent exactement les énoncés vrais dans ℕ, et pour le coup, il y a une notion de démontration, fût-elle infinitaire). Bref, si j'ai souligné l'hypothèse du premier ordre, c'est surtout que si on la retire, on ne sait plus bien dans quel cadre se placer.

@jonas: Maybe Hofstadter got it from Smullyan (directly or indirectly)! All I'm saying is, I learned it from Hofstadter. But the sentence also appears in Franzén (who is, indeed, more likely to have taken it from Smullyan than from Hofstadter; but it could be older, I have no idea).

jonas (2019-08-27T20:12:11Z)

> > Douglas Hofstadter ne peut pas se convaincre de la vérité de cette phrase.
> Hofstadter est l'auteur d'un célèbre livre de vulgarisation … dans lequel j'ai d'ailleurs piqué l'idée de la phrase ci-dessus !

This surprised me. I assumed that it was Smullyan who inspires such statements.

Ilia (2019-08-27T17:53:04Z)

Peux-tu donner des contre-exemples au théorème si on enlève les trois hypothèses ?

Si on enlève la troisième, je comprends assez bien ce qui se passe : en gros, ce n'est qu'à partir du moment où le système est suffisamment complexe que son comportement devient imprévisible. Si je comprends bien, le système "pq-" dans Gödel, Escher, Bach fournit un contre-exemple au théorème sans la troisième hypothèse - mais reprends-moi si j'ai tort.

La deuxième hypothèse, si je comprends bien, sert à éliminer des trucs du genre "le système où on définit P comme étant un théorème lorsque P est vrai". Mais peut-être est-ce une vision trop naïve ?

Quant à la première hypothèse - que le système soit du premier ordre - là, j'avoue que j'ai du mal à en comprendre l'importance…

ooten (2019-08-27T14:58:26Z)

Et si vous voulez de la très bonne vulgarisation et pas seulement (enfin personnellement je ne me suis intéressé qu’aux tout premiers paragraphes des ses articles), allez sur : <URL: http://girard.perso.math.cnrs.fr/Accueil.html >