Discussion:Théorèmes d'incomplétude de Gödel

Indécidabilité

Note : le texte ci-dessous a été déplacé depuis le Bistro de Wikipédia. Aoineko 18 fév 2004 à 02:50 (CET)

Dans la page Discuter:Athéisme, Stuart évoque le principe d'indécidabilité de Cantor. C'est apparemment un sujet qui touche à la fois les mathématiques (par son origine) et la philosophie (par ses applications). J'aimerais en savoir plus là-dessus, c'est pourquoi j'ai lancé une offre sur Wikipédia:WikiMonnaie. Et à la réflexion, 4 ψ c'est pas assez pour un sujet aussi costaud, je vais remonter ça. Φido 11 fév 2004 à 11:15 (CET)

Je n'y connais pas grand chose (juste quelques mots de la part d'un prof d'algèbre en prépa) mais je donne quand même mon avis. Le principe d'une bonne théorie est d'expliquer le maximum de choses avec le minimum d'hypothèses. Pour réduire le nombre d'hypothèses on essaie de montrer qu'une hypothèse peut se démontrer à partir d'autres qui ont déjà été posées. En revanche il y a des résultats qu'on ne peut absolument pas démontrer à partir d'autres. L'exemple le plus célèbre est constitué par les tentatives de démontrer que l'axiome des parallèles en géométrie euclidienne pourrait se déduire des autres axiomes (je ne me souviens plus lesquels). Or, grâce à ce cher Cantor on sait maintenant que cet axiome n'est pas démontrable. Donc les trois solutions (deux parallèles ne se coupent jamais; se coupent en un point; se coupent en une infinité de points) sont toutes aussi valables et sont chacune à la base d'un type de géométrie. Dans le cas de Dieu, son existance ou sa non existance n'étant pas démontrable, chacune des réponses est valables. S'il y avait un matheux dans la salle pour corriger mes erreurs ce ne serait pas de refus. /me préfère la Physique aux maths ;) Med 11 fév 2004 à 11:30 (CET)

Non, cette théorie là, c'ets le rasoir d'Ockham. Stuart Little 11 fév 2004 à 17:36 (CET)

Pour moi, le principe d'indécidabilité est de Gödel (en s'inspirant de Cantor)), qui a publié le Théorème d'Incomplétude. D'ailleurs, Stuart Little a écrit : "C'est ce qu'explique le principe d'indécidabilité de Goeddel à partir des travaux sur les grands cardinaux de Cantor.". Ceci dit, c'est bien au-dessus de mon niveau, on verra ca dans quelques années. Ceux que ca intéresse peuvent aussi lire les livres de Raymond Smullyan ("Le livre qui rend fou" et "Ca y est, je suis fou"), ca commence par des énigmes et ca finit par ca... je me suis arrêté un peu avant Koxinga 11 fév 2004 à 13:20 (CET)

C'est exactement cela que j'aimerais qu'on expose proprement. Parce que moi, si je l'expose, je sors de mon domaine de compétence et je n'exposerai que des salades.

Je suis pas au courãnt du wikimonnaie. Mais c'est sûr que j'en mettrais bien pour avoir un exposé clair et cohérent. Stuart Little 11 fév 2004 à 17:36 (CET)

J'ai lu un bouquin la dessus il y a quelque temps qui expliquait qu'il fallait faire très attention as l'application de ce théorème hors du champs des mathématiques (il prenait justement le cas de l'existence de Dieu). En effet les indécidables de Goëdel (comme tout résultat mathématique) ne le sont que pour un système formel (une collection d'hypothèse de départs: les axiomes) donné. Il ne prédisent en aucun cas qu'il ne sera pas possible de trouver un système formel ou il ne seront plus indécidable (tout ce que prédit ce théorème c'est que ce nouveau système formel sera toujours incomplet car il contiendra encore d'autre indécidables). Pour reprendre l'axiome de parallèle: il est tout à fait possible de le remplacer par un autre axiome (la somme des angles d'un triangle vaut 180° devrait marcher ???) qui permettra de démontrer l'axiome des parallèles. Par ailleurs il existe des systèmes formels complets (c'est à dire des théories sans indécidables): par exemple la logique du premier ordre (tout est vrai ou faux) est axiomatisable. Donc si quelqu'un qui vous dit "l'existence de Dieu est indécidable" demandez lui "en prenant quelles hypothèses de départ?" ;-) ske 11 fév 2004 à 13:49 (CET)

OK. Mais si tu prends la question de Cantor sur les grands cardinaux (cel de l'aleph 1 et de l'aleph 0) tu comprends parfaitement ce dont on parle à propos de l'indécidabilité de l'existence de Dieu. Laquelle question des grands cardinaux ne dépend que d'un axiome : toute grandeur est mesurable. Stuart Little 11 fév 2004 à 17:36 (CET)

Coucou, coucou ! Voilà un matheux ! Gödel a démontré deux théorèmes sur le sujet de l'indécidabilité : ① tout système formel contenant les nombres entiers (donc pas mal de choses) contient une proposition indécidable (ie qu'on ne peut peut démontrer vraie ou fausse avec les axiomes initiaux) et ② que cette proposition est vraie en ajoutant un axiome. Ensuite il ne faut pas faire sortir ce théorème mathématique des mathématiques sinon on raconte n'importe quoi comme Debray et son principe bidon de Gödel-Debray (cf. la partie là-dessus du livre de Sokal et Bricmont Impostures intellectuelles). ℓisllk 11 fév 2004 à 16:32 (CET)

Bon, c'est incompréhensible. Mais l'interdit de Sokal et Briquement est clairement documenté par des exemples et, dans le cas présent, cela ne s'applique pas.

C'est marrant comme les matheux peuvent être dogmatiques, parfois ? On croirait entendre un croyant démontrer l'existence de Dieu dans le langage qui lui est propre et, quand on veut lui montrer un glissement sémantique qui sert de raisonnement, il répond ah, mais tu peux pas comprendre. :-)))

Stuart Little 11 fév 2004 à 17:36 (CET)

Relis lentement, tu devrais comprendre : ce n'est pas si dur que ça. De plus le problème de א₀ et de א₁ n'est pas indécidable au sens de mon intervention ci-dessus parce que le problème de Cantor (est-ce qu'il existe un cardinal entre א₀ et א₁ ?) est un postulat, c'est-à-dire qu'on peut y répondre « oui » ou « non », cela produira juste des théories différentes, en aucun cas des contradicitons. Notons que mon intervention (comme la précédente) n'est pas dogmatique, ce que je dis sont des théorèmes démontrés (pas par moi bien entendu). ℓisllk 11 fév 2004 à 20:40 (CET)

Création de l'article

J'ai réalisé deux articles sur le Théorème d'incomplétude de Gödel et l'Hypothèse du continu de Cantor. Je pense que c'était le sujet de vos demandes ? Ils sont par contre à completer, notamment pour la demonstration du théorème d'incompletude et le rapport avec la philosophie et dieu. OsMoSe 29 fév 2004 à 19:13 (CET)

Je pense que la page devrait s'appeler Théorèmes d'Incomplétude vu que Gödel en a pondu deux. Sinon je ne vois pas ce que dieu vient faire là dedans. Ces théorèmes existent et sont prouvés mathématiquements. La philosophie qui vient se greffer dessus ce n'est que des discussions. --Tom 15 sep 2004 à 23:15 (CEST)

CD J'ai créé le titre "création de l'article", et ce serait bien que quelqu'un fasse des séparations avec des "modifier" parce que la page commence à être bien longue - c'est hors de ma portée pour le moment. Je viens de faire un peu de "cosmétique" dans le texte et je m'apprétais à pondre mes observations ici, et, oh surprise, ce n'est pas comme pour tous les théorèmes que j'ai visités ces derniers jours, on a déjà beaucoup discuté ! J'allais commencer en disant : bon article, mais cela peut être un article phare pour le projet mathématiques dans la mesure où la population intéressée dépasse largement le cadre des plus ou moins initiés à la logique (sauf erreur, il n'y a aucun article de mathématique non élémentaire parmi la centaine de fleurons de wikipédia) ; de ce point de vue je crois que l'article n'est pas encore à la hauteur, mais je me doute combien la tâche est difficile. Avant d'écrire quelques réflexions sur l'article, je suggérerai une méthode pour apporter des idées : il est clair, si j'ai bien compris la discussion, qu'il y a eu un bon débat sur le sujet avant la création de l'article, mais qu'il s'est éteint après la création ; ne pourrait-on pas relancer le débat sur une arène plus fréquentée (bistro, ?, et pourquoi pas, tâche de la semaine) en demandant aux gens de dire ce qu'ils pensent de la rédaction actuelle ?

Je termine par quelques remarques au fil de la lecture de l'article. Je vais parfois essayer de dire des choses précises du point de vue logique formelle, mais je risque ainsi de sortir de mon domaine de compétence, bref de dire des conneries.
1) Au sujet de « échapper ». Pour bien exposer la problématique il faudrait en dire un peu plus sur les systèmes formels. Goedel (comme Hilbert) s'intéresse à des systèmes où en un certain sens, qui peut être rendu précis, l'ensemble des axiomes est décidable : on a un algorithme qui permet de décider si oui ou non un énoncé est un axiome. Mais on peut très bien définir une théorie fromelle des entiers en prenant un modèle de la théorie précédente et en prenant comme axiomes tous les énoncés vrais dans le modèle ; on n'a là une théorie complète (tout aussi consistante que celle départ), mais à part cela sans grand intérêt pratique.
2) Il faudrait quelques mots ici ou là sur l'ordinal mystérieux de Gentzen.
3) La date 1868 est aussi mystérieuse ; et puis ce n'est pas tout à fait juste pour Bolyai et Lobatchewski.
4) Ici encore il faudrait que le lecteur puisse comprendre qu'un indecidable dans un système à la Peano (et jamais précisé dans l'article) peut ne pas l'être dans les entiers de la théorie des ensembles. De plus on a un exemple amusant d'une telle chose avec Hercule coupant les têtes de l'hydre (je ne sais plus exactement ce que c'est, mais je peux retrouver). Par contre je ne connais pas du tout l'exemple en théorie des matrices, et j'aimerais bien avoir une référence.
5) enfin, le dernier paragraphe n'a à mon avis rien à faire dans un article de mathématique ; par contre il suggère qu'il devrait y avoir un article sur l'exploitation de résultats scientifiques (th. de Goedel, mais aussi principe d'incertitude, etc. ; en fouillant les archives de l'affaire Sokal, on peut trouver beaucoup de sujets) en sciences humaines, avec quelques beaux problèmes de neutralité de point de vue... CD 22 jan 2005 à 19:41 (CET)

Personnellement, je verrai bien l'évolution de l'article vers 2 articles différents :

• Je pense qu'il faudrait crée sur une autre page un article totalement mathématique présentant rigoureusement les théorèmes d'incomplétude de Gödel, avec un modèle de démonstration.
• Quand à cette page, elle pourrait rester dans le même esprit qu'actuellement, une page de vulgarisation qui présenterai également les aspects extra-mathématiques. Qu'en pensez vous ?
  

Concernant les têtes de l'hydre, c'est un très bon exemple en effet, très clair, j'essayerai de le rajouter (à moins que vous préfériez le faire ?). Concernant "l'ordinal mystérieux de Gentzen" par contre, je pense voir grosso-modo de quoi il s'agit, mais je ne pense avoir les connaissances pour en parler, je vous laisse donc faire :).

Concernant la date de 1868, elle correspond à la démonstration due à Eugenio Beltrani.

OsMoSe 23 jan 2005 à 19:27 (CET)

Content de te "rencontrer" (comme je suis sans doute le plus vieux, je me permets de proposer le tutoiement, qui me semble habituel dans ces lieux). Je suis entièrement de ton avis, c'est très bien d'avoir, comme on a maintenant, une bonne base de départ (pas trop formalisée, mais pas trop floue non plus) et de continuer par les aspects extra-mathématiques. Mais il faut alors, comme tu le dis, un article vraiment mathématique et je n'ai pas l'impression qu'on a parmi nous quelqu'un d'apte à le faire ex nihilo ; si le texte anglais est bon (je ne l'ai pas regardé) je peux en faire la traduction (avec les afférents : système formel, etc. ; dans quoi je me lance !). Pour l'hydre, c'est un souvenir, je ne sais plus où j'ai lu (ou entendu) cela, et je te la laisse bien volontiers. Je me doutais que 1868 était l'apparition d'un modèle intérieur à la géométrie euclidienne ; il faut ajouter Beltrami etc. ou dans l'article ou dans 1868. Je m'occupe du epsilonn de Gentzen (je ne sais pas bien ce que c'est, mais j'ai de la documentation - de manière générale j'ai à ma disposition beaucoup de documentation, ne pas hésiter à me demander). CD 23 jan 2005 à 21:58 (CET)

Modification de l'article

• Quelques modifs mineures :
  • remplacer consistant par cohérent. C'est tout aussi précis (aucune contradiction prouvable) et c'est plus parlant.
  • date de communication de la preuve (1930), publication écrite 1931.
  • mentionner que la terminologie n'est pas très bien fixée, ni ici, ni par les logiciens. Le théorème d'incomplétude de Gödel est appelé parfois le premier théorème d'incomplétude pour le distinguer du second (l'énoncé qui affirme la cohérence d'une théorie T est un indécidable de T). Comme les deux vont ensemble, que la preuve du second suit directement celle du premier, qu'ils ont été exposés par Gödel dans le même article fondateur de 1931, il me semble qu'ils doivent être présentés dans un même article de l'encyclopédie.
• modifs plus importantes
  • mentionner l'existence d'une preuve naturelle de la Cohérence des axiomes de l'arithmétique formelle, dont la validité n'est pas contestable, mais qui est difficile à formaliser et qui présuppose notre capacité à connaître les ensembles infinis.
  • Introduire les notions de représentation d'une formule par un nombre (arithmétisation de Gödel) et par un objet quelconque de la théorie, et de prédicat de prouvabilité.
  • Prouver le théorème de Gödel sous l'hypothèse de l'existence d'un prédicat de prouvabilité et d'un prédicat de substitution. La preuve est facile et peut être exposée même dans un article destiné à tout public. La construction de l'énoncé indécidable de Gödel est identique à la construction du nombre AT dans le théorème d'incomplétude de Tarski. Il suffit de remplacer le prédicat de vérité par un prédicat de prouvabilité. C'est une application directe du paradoxe du menteur, comme tous (?, je crois que oui, mais c'est peut-être un peu tiré par les cheveux. Peut-on voir les théorèmes de Cantor comme une application directe du paradoxe du menteur ?) les théorèmes sur l'incomplétude mathématique. On peut aussi déduire le théorème de Gödel du théorème de Tarski.
  • La partie difficile de la preuve de Gödel consiste bien sûr à prouver l'existence des prédicats de prouvabilité et de substitution. Je ne sais pas si CD a avancé sur cette partie très mathématique. De mon côté je laisse cela pour l'instant. Je prépare une révision de l'article système formel qui donnera quelques préliminaires.
  • Donner l'argument de la preuve du second théorème d'incomplétude. Insister, comme cela a déjà été dit sur le caractère relatif de ce théorème : T ne permet pas de prouver la cohérence de T, mais cela ne veut pas dire que la cohérence de T n'est pas prouvable.
  • Je trouve que la discussion sur formalisme et logicisme est trop courte.
    • Pour que les conclusions soient recevables il faudrait qu'elles soient précisées. Il y a des façons d'interpréter le formalisme et le logicisme tout à fait respectables, même aujourd'hui. Ce sont des tentatives de réponse à la question de la nature de la vérité mathématique. C'est toujours une question d'actualité pour laquelle les propos de Frege, Hilbert, Whitehead, Russell et beaucoup d'autres sont toujours pertinents, même s'ils doivent être révisés à la lumière des résultats obtenus par Gödel.
    • mentionner que la terminologie sur la différence entre principes logiques et principes mathématiques n'est pas très bien fixée, ni ici, ni par les logiciens. Frege considérait les principes de sa théorie (contradictoire) des ensembles comme des principes logiques. Il me semble qu'aujourd'hui, le mieux est de considérer les principes de la logique du premier ordre (sans théorie des ensembles donc, ni explicitement, ni implicitement) comme le noyau dur de la logique.
  • la partie philosophie pourrait être mieux exploitée.
    • Dire que l'existence de Dieu est un indécidable, c'est dire qu'on n'a pas choisi d'axiomes pour répondre à cette question. De ce point de vue, on peut rappeler que chacun est libre de choisir les axiomes qu'il veut, et que c'est à lui de montrer alors leur valeur.
    • Discuter les notions de puissance et d'impuissance de la raison. Montrer que le théorème d'incomplétude est lié à la puissance de l'imagination mais qu'il ne met pas en doute notre capacité à donner des preuves et à connaître, en un sens, tous les principes logiques.(voir théorème de complétude de Gödel.
• Tout ceci est en préparation. J'en mettrai en ligne une partie dès que ce sera prêt (quelques jours), en tenant compte de vos objections.--Thierry Dugnolle 19 fev 2005 à 11:08 (CET)

J'ai lu, apprécié, mais je n'ai pas le temps d'écrire ma réponse aujourd'hui. J'écris aujourd'hui surtout pour te signaler ce qui me semble une coquille dans tes premières lignes. Tu as écrit "théorème de complétude" pour "théorème d'incomplétude" me semble-t-il. Trois théorèmes de Goedel : l'un, de complétude, le suivant d'incomplétude (1er) et le dernier d'inconsistance si je puis dire (incomplétude 2ème). CD 19 fev 2005 à 12:11 (CET)

Désolé pour la coquille. J'avais pourtant relu deux ou trois fois.--Thierry Dugnolle 19 fev 2005 à 14:30 (CET)

Maturité de l'article

Très bel article, maintenant ! Encore un peu de wikification et de corrections typographiques (pour les formules mathématiques) et je serais pour en faire un "article de qualité" ! --Aldoo / ✉ 25 fev 2005 à 10:12 (CET)

J'avais aussi fait des éloges et quelques remarques, mais tout a disparu à la sauvegarde ! Avant d'avoir le courage de recommencer, deux petites choses que je pourrais faire moi-même un peu plus tard : sauf erreur, on n'écrit pas "Türing" mais "Turing", et il faut un lien diophantien quelque part. CD 25 fev 2005 à 11:17 (CET)

Reprises de quelques remarques.

• Il manque un pont entre "incomplétude" qui paraît dans le titre mais peu ailleurs (sf reprise du titre) et "indécidabilité" et autres utilisés abondamment.
• Je suis d'accord que "cohérent" est meilleur que "consistant", mais il est tellement fait usage de "consistant" ou "inconsistant" qu'il faut à mon avis que le mot paraisse dans le début de l'article (je ne sais si Dugnolle voit ici une différence "technique" entre "cohérent" et "consistant", aussi je m'abstiens de corriger moi-même).

Est-ce que "consistant", bien que fréquemment utilisé dans ce contexte-là, ne serait pas un anglicisme, au fait ? --Aldoo / ✉ 1 mar 2005 à 09:17 (CET)

Oh là bonne question, moi qui défends "récurrence" contre "induction"... C'est sans doute un anglicisme (et j'ai appris la logique dans des livres en anglais). J'ai été voir dans mes références en français. Dans "théorie des ensembles", Krivine donne "non contradictoire", "cohérent" et "consistant" comme synonymes [il serait bon aussi de citer "non contradictoire"] ; dans "Logique mathématique", Cori et Lascar prenne "cohérent" dans le sens syntaxique (on ne peut démontrer formellement un énoncé et son contraire) et "consistant" dans le sens sémantique (théorie ayant au moins un modèle). CD 1 mar 2005 à 10:46 (CET)

• Le paragraphe "Relativité de l'indécidabilité..." et plus précisément dans l'alinéa "On pourrait penser "s'échapper" du théorème...", qui date d'avant Dugnolle, ne me satisfait pas. Il manque une référence à quelque chose comme "théorie finiment axiomatisée", introduit bien plus tard.
• Toujours dans ce paragraphe, pourrait-on rendre moins mystérieux l'ordinal de Gentzen ?
• Le paragraphe "Des exemples... d'indécidables", qui date aussi d'avant Dugnolle, contient une distorsion historique : l'exploration de la géométrie hyperbolique par Lobatschevski ou Bolyai date de bien avant le modèle de Beltrami auquel la date 1868 fait sans doute référence.
• Dans le même paragraphe, je suis toujours preneur de l'exemple d'indécidable concernant les produits de matrices (je ne vois pas du tout à quoi cela fait allusion). Je me souviens (imprécisément) d'autre part d'un exemple où Hercule a à couper des tetes de l'hydre selon certaines règles : on ob tient un indécidable de la théorie de Peano mais un théorème pour les entiers en théorie des ensembles.
• Au début de "Argument de la preuve et...", le paragraphe "On sait aujourd'hui... temps de calcul". Cela donne l'impression qu'une théorie décidable n'a pas grand intérêt, et c'est faux : par exemple, d'après Tarski, la géométrie d'Euclide est décidable, etc. D'autre part, le temps de calcul, pour un énoncé de taille raisonnable, peut être plus long que ce que permet l'univers (voir travaux de Stockmeyer et Meyer). CD 28 fev 2005 à 17:41 (CET)

---

Il y a beaucoup à répondre.

• Sur Gentzen je suis un peu embêté. Je n'ai pas lu ses travaux sur la cohérence, ou consistance, ou non-contradiction, de l'arithmétique, je ne connais que le chapitre donné par Lorenzen (Métamathématique) sur ce sujet, et je ne connais pas les développements de la théorie de la preuve. J'aimerais bien aller plus loin mais je manque de temps et de documentation.
• On a parfois besoin de distinguer plusieurs notions de consistance (syntaxique ou sémantique, oméga-consistance,...) mais je ne crois pas qu'il faille introduire ici ces distinctions. Le même flou terminologique existe aussi en anglais.
• Oui pour changer le ton du paragraphe sur les théories décidables. Il serait même souhaitable de répertorier les théories décidables "intéressantes" et de donner (dans d'autres articles) des algorithmes de décision.

Sur les autres points, j'y réfléchis.--Thierry Dugnolle 1 mar 2005 à 15:00 (CET)

Petite réponse. Je suis (et serai) beaucoup en voyage ces temps-ci. Sur Gentzen, tu n'as pas à te sentir embêté ; je ne pense pas qu'il faille en dire beaucoup ssur son ordinal, juste une petite chose pour qu'il soit moins mystérieux (c'est sans doute un "petit" ordinal dénombrable, je n'ose pas le mettre parce que je n'ai pas retrouvé de référence, sinon je pense que c'est la seule chose à mettre). Je suis tout à fait d'accord pour ne pas chercher à distinguer dans l'article les différents sens donnés à consistance, cohérence, etc. Mais je réitère ma remarque : il faut que le mot "consistance" (ou "consistant") apparaisse au moins une fois pour que le lecteur qui a lu quelque part "consistance" n'ait pas de doute qu'on parle de la même chose. Enfin, il y a un article décidable qui a été créé, et aussi une discusssion de savoir si on le garde (dans PàS). J'ai proposé de garder, et de mettre là des exemples intéressants de théories décidables. CD 4 mar 2005 à 10:02 (CET)

J'ai supprimé les deux phrases suivantes. Je suis pour les réintégrer mais comme je ne sais pas de quoi il s'agit j'aimerais des précisions

• Mais depuis l'arrivée de la théorie du calcul, on a pu créer de nouveaux indécidables, touchant par exemple des propriétés élémentaires concernant des produits de matrices.

• En 1973, Saharon Shelah montra que le problème de Whitehead était un indécidable de la théorie des ensembles.

--Thierry Dugnolle 4 mar 2005 à 22:08 (CET)

Pour ce qui est des "...produit de matrices...", c'est un mystère pour moi. Peut-être que "Osmose", qui s'est beaucoup occupé de la première rédaction, sait. Pour le problème de Whitehead je crois que j'ai lu un article dessus dans la version anglaise de Wikipédia et j'y ai compris un petit quelque chose. Cependant, il s'agit d'un problème sur les groupes abéliens, la théorie des groupes abéliens est décidable... et là je flotte. CD 4 mar 2005 à 23:23 (CET)

Dieu ?

La partie Le théorème d'incomplétude en philosophie est assez surprenante. Il est dit que le théorème est souvent cité en philosophie. On aimerait bien des exemples. Quant à Dieu, on se demande bien ce qu'il vient faire dans cet article et quel rapport il peut bien avoir avec un théorème d'ordre mathématique. Mêler Dieu au théorème d'incomplétude de Gödel est aussi absurde que de le lier à la non-existence de solution réelle à l'équation x²+1=0 ou au contraire à l'existence d'une solution complexe. Theon 9 mars 2006 à 18:15 (CET)

Je suis globablement d'accord. L'existence de Dieu n'a rien a faire là. En ce qui concerne les citations en philosophie : ce n'est pas parce que certains "philosophes" ont utilisé le théorème de Gödel de façon extravagante que c'est l'habitude en philosophie. La philosophie peut s'occuper de mathématiques, de la logique et du théorème de Gödel sans sortir ce dernier de son contexte. A ce sujet, quelques lignes plus loin dans l'article, une phrase comme "Ces théorèmes montrent que l'imagination déborde tous les cadres" fait quand même un peu penser aux citations décriés au dessus. Est-il besoin dans un article sur le théorème de Gödel de parler des mauvais usages de celui-ci ? Si oui il faudrait intituler le paragraphe autrement et effectivement donner des exemples. je pense plutôt que l'on peut supprimer cette partie. Proz 7 avril 2006 à 01:30 (CEST)

En fait, je pense que les utilisations plus ou moins délirantes du Théorème de Gödel font partie de la matière encyclopédique concernant ledit théorème. Le but, c'est de rester neutre (donc, je retire plus ou moins délirantes:)), et de garder à cette partie des proportions raisonnables. Pour la neutralité, on peut utiliser cette phrase introductive : Le théorème de Gödel porte sur une propriété des systèmes formels d'axiomes dans la théorie des prédicats. Certains ouvrages ont prétendu lui donner une portée plus étendue que son champ d'application naturel. (peut-être certains trouveront prétendu non neutre, on peut changer). Après, il faudrait faire une vraie recherche pour donner quelques exemples significatifs, n'en développer aucun, et renvoyer sur les pages dédiées aux auteurs ou aux ouvrages en questions pour plus de précision, puis citer au moins l'existence d'une réaction à la Sokal-Bricmont, avec à nouveau lien vers ailleurs. La question existe, on dit ainsi cette existence, sans entrer dans la polémique.Salle 14 août 2006 à 23:20 (CEST)

Je ne suis guère enthousiaste, mais on peut faire quelquechose effectivement. Finalement je ne citerais pas forcément d'exemple précis. On peut se contenter d'une phrase sur la fascination exercée par le th. qui a produit quelques extrapolations contestables. Le livre de Sokal-Bricmont (qui peut être cité) a sa cohérence propre. C'est le fonctionnement d'un milieu qui est dénoncé, à travers ce genre de dérive sur le th. de Gödel (entre autres). Maintenant faire une vraie recherche pour etc. (ne pas se contenter de seconde main), c'est du boulot, et est-ce vraiment intéressant ? Si quelqu'un a envie de le faire, pourquoi pas ? L'écueil c'est un peu ce qui existait encore un avril 2006 (voir l'historique) : un paragraphe qui dénonce de façon vague, et qui fait vite prétentieux. Tout ça peut s'intégrer à un paragraphe d'intro, (dans lequel il y a des choses plus urgentes à dire). Proz 15 août 2006 à 22:57 (CEST)

Moi non plus, ça ne me passionne pas ; disons que l'idée, c'est de ne pas tomber dans un consensus entre matheux pour dire que tout ça n'a pas sa place. Puisque personne n'a envie de faire les recherches nécessaires, il vaut mieux effectivement ne rien faire pour le moment ; mais en se disant que le jour où quelqu'un voudra le faire bien, ça vaudra un petit paragraphe.Salle 18 août 2006 à 10:55 (CEST)

refonte de l'article ?

Après avoir parcouru l'article il me semble que quelques modifications seraient utiles. D'une part il y a des imprécisions, voire erreurs. Par exemple la partie sur la preuve partielle du théorème est vraiment douteuse. Le théorème de Gödel ne se déduit pas du théorème de Tarski (sauf dans une version beaucoup plus faible que celle de Gödel, puiqu'il faut supposer que la théorie à pour modèle les entiers usuels) et de toute façon celui-ci date de 1933 (2 ans après Gödel), l'énoncé dit équivalent au th. de Gödel dans cette partie n'est de toute façon pas clair (que veut dire vrai ?) etc.[corrigé] Il faut de toute façon parler des hypothèses de cohérence pour comprendre le problème [à faire].

Je commence quelques modifications dans ce sens, très graduellement, et en débutant sous wikipedia. Mais une refonte serait peut être utile :

- la partie sur les preuves de cohérence de l'arithmétique devrait être dans un autre article

- les considérations sur les théories complètes devraient faire partie d'un autre article

- l'existence de théories incomplètes est en soit une trivialité, donc je ne suis pas sûr que le passage sur la géométrie, qui est bien-sûr intéressant (preuve de cohérence relative) soit à sa place.

Proz 5 avril 2006 à 22:19 (CEST)

Petit ajout : j'ai commencé quelques modifications. J'en justifie une qui n'était pas annoncée ci-dessus. L'énoncé du second théorème d'incomplétude n'était pas correct : sous les hypothèses usuelles, la cohérence d'une théorie est non démontrable dans cette théorie, mais pas forcément indécidable, comme on le déduit d'ailleurs justement du théorème lui-même. Je rajouterai d'ailleurs probablement quelquechose à ce sujet dans l'article [Fait].

Proz 7 avril 2006 à 01:40 (CEST)

J'ai restructuré le premier paragraphe, éliminé la reférence à une preuve en 1930 dont je n'ai pas trouvé trace [il semble que le résultat ait été annoncé en 1930, je laisse la date de parution de l'article, ce qui est le plus usuel] essayé de simplifier ou d'éclaircir certains points. Je ne considère pas du tout l'article dans un état satisfaisant. La suite est souvent encombrée de considérations qui me semblent hasardeuses par exemple sur les preuves de cohérence, et difficile à reprendre. Je compte réécrire pas mal de choses. Proz 25 avril 2006 à 20:38 (CEST)

Création d'un article théorie axiomatique, déplacement des développement sur les théories récursivement axiomatisable dans cet article, qui contiendra également une partie sur les liens entre complétude et décidabilité.[Fait]

Proz 26 avril 2006 à 22:19 (CEST)

L'article présent pointe sur l'article Diophantien qui semble précis et bien documenté, on peut donc réduire le paragraphe à ce sujet de l'article présent. En fait le paragraphe "Des exemples de systèmes incomplets et d'indécidables" est à restructurer. Le paragraphe "La relativité de l'indécidabilité des énoncés" également.

Par ailleurs la bibliographie est dans un grand désordre, et je doute qu'elle soit très utile. Il faudrait structurer, un peu dans le style de l'article de la version anglaise (qui est dans un meilleur état que celui-ci), je séparerais les livres de vulgarisation, des livres plus scientifiques, et/ou J'ajouterais des commentaires très courts, pour décrire le livre, essentiellement le public à qui il s'adresse. Mais je n'ai pas lu, et ne compte pas lire, tout ce qui est cité actuellement ... j'espère des indications. [Fait partiellement] Proz 27 avril 2006 à 20:45 (CEST)

Ajout d'un paragraphe sur "vérité et démontrabilité" [Fait].

Je commence aussi de restructurer la suite : "La relativité de l'indécidabilité des énoncés", suppression à terme de ce paragraphe, ce qui correspond au titre est déjà décrit plus précisément dans le paragraphe "conséquences directes du 1er th. de G.", il y a aussi des choses dans "vérité et démontrabilité".[Fait]

• Goodstein à recaser (dans un paragraphe "énoncés indécidables de l'arithmétique" ?)[Fait]

• preuves de cohérence : on peut en parler brièvement dans le paragraphe sur le formalisme qui est à reprendre également, voir la partie sur le programme de Hilbert dans fondements des mathématiques.[Fait]

On peut dire un mot sur la preuve de cohérence sémantique dans le paragraphe sur "vérité et démontrabilité", dans le sens communément admis : c'est une trivialité, c'est une preuve de cohérence relativement à une théorie au moins aussi forte en le sens le plus naïf (contient l'arithmétique), plus forte par le 2nd Th. d'inc.

Suppression du paragraphe "TH. de G. en philo." prévue, si pas d'opposition (voir discussion précédente).[Fait]

Proz 4 mai 2006 à 20:25 (CEST)

J'ai, entre autres, restructuré le paragraphe sur "théorie incomplètes et énoncés indécidables", et supprimé à l'occasion le paragraphe sur la géométrie. Parler de l'axiome des parallèles à propos du théorème d'incomplétude est un peu tiré par les cheveux. Mais surtout ça ne semblait pas correct sur le plan historique. Voir les articles géométrie euclidienne, géométrie non euclidienne, axiomes de Hilbert et google : l'apport de Beltrami semble concerner la géométrie hyperbolique, le paragraphe décrivait un modèle de Riemann.

paragraphe créé "Théorèmes d'incomplétude et indécidabilité algorithmique" : à compléter [Fait] (renommé ... et calculabilité)

Proz 17 mai 2006 à 22:42 (CEST)

Restructuration du paragraphe "Une preuve partielle du premier théorème d'incomplétude": à poursuivre, fonction beta ... [Fait]

Considérations purement gratuites sur le "pythagoricisme" supprimées.

A faire (dans un autre paragraphe): citer le Th. de Löb [Fait, mais article à écrire].

Proz 26 mai 2006 à 02:01 (CEST)

A faire : ce qui était appelé "indécidable absolu" a disparu : donner la position de Hilbert ( / Ignorabimus)

Harmoniser et compléter le dernier paragraphe (2nd Th) [Fait] Proz 30 mai 2006 à 20:49 (CEST)

A faire : réordonner les paragraphes de l'article, en particulier, il faut parler plus tôt du programme de Hilbert, un peu plus d'aspects historiques (Von Neumann) [proposition sous le titre "Introduction à l'article", dans la suite].

Proz 19 juin 2006 à 22:52 (CEST)

Bibliographie

Que contient (en rapport avec le sujet) ? Est-ce une référence à maintenir ?

• Jean-Marc Alliot, Thomas Schiex, Pascal Brisset, Frédérik Garcia, Intelligence artificielle & informatique théorique - Cepadues, 2002 - (ISBN 2854285786)

Je déplace ici cette référence, qui est plus à sa place dans la discussion, que comme référence de l'article lui même, me semble-t-il

• Yann Ollivier, Le théorème de Gödel et ses non-interprétations

Références "Autres" à commenter. Proz 30 mai 2006 à 21:21 (CEST)

Rapport avec :le théorème de complétude ?

Quelqu'un pourrait-il indiquer ici (ou dans l'article cousin "Théorème de complétude de Gödel", le rapport exact des deux théorèmes, c'est à dire indiquer ce qui relève de l'un ou de l'autre ? L'idéal serait que ce fût sous forme de tableau, afin de bien fixer les idées. D'avance merci à qui en aura le courage ! 81.64.199.181 8 juillet 2006 à 16:47 (CEST)

Félicitation

J'ai étudié ce théorème à l'université, et je tiens à vous féliciter pour son explication claire et concise ;-) Ce qui permet à terme un décloisonnement des personnes.

Merci à tous. Bonne continuation.

Lecture de Salle, questions posées à Proz, recopiées ici pour mémoire

Bonjour, l'article devant passer AdQ, en tant que contributeur en maths, j'ai tenté de ma lancer dans la lecture. Pour le moment, je n'ai lu que les deux premières parties, et je n'ai pas compris grand-chose, j'ai peur. Je ne sais pas si ça sera utile, mais j'essaie (et ça va forcément être flou, étant donné mon incoompétence avérée en logique) quand même d'expliquer ce qui me bloque, et peut-être pourras-tu en tirer quelque chose pour améliorer l'article ; sinon, tant pis ; et je m'excuse d'avance pour toutes les remarques débiles que je vais faire (plutôt qu'à chaque fois que je ne serai pas sûr de ne pâs dire n'importe quoi), ainsi que toutes celles se référant à des notions présentes ailleurs : j'ai juste jeté un coup d'œil aux liens.Salle 11 août 2006 à 19:28 (CEST)

Merci pour tes réponses et reformulations, cela me semble plus clair. Il reste deux ou trois points obscurs. Pour la suite de l'article, je n'ai pas le temps de le lire en ce moment, mais dès que je peux, j'essaie de m'y mettre.

Partie I

Conditions d'application

• Il est dit qu'on se place dorénavant dans la logique classique, mais que le théorème reste vrai en logique intuitionniste. Or, il est fait usage constant de raisonnement par l'absurde ; si j'ai compris la page sur logique intuitionniste (mais il y a des notations fractionnaires bizarres qui me troublent), on n'y a pas droit. Le problème est-il délicat à surmonter? QUi l'a fait? Gödel lui-même?

Les démonstrations des deux théorèmes n'utilisent pas le raisonnement par l'absurde. Donc il n'y a rien à faire. La suite utilise parfois le raisonnement par l'absurde pour des conséquences des théorèmes, pas pour les preuves. Ce qui m'inquiète, c'est que l'article donne l'impression de faire un usage constant du raisonnement par l'absurde : peux-tu expliquer ? Par ailleurs il est commode de se placer en logique classique pour la notion de modèle et de vérité dans un modèle.

Je répète que ma lecture de l'article s'est limitée pour le moment au deux premières parties. Ta réponse réduit il est vrai mon objection : faire du raisonnement par l'absurde pour les conséquences, c'est OK. Cependant, par curiosité, j'ai regardé les premières lignes de la preuve du théorème 1. A vue de nez, Il est vrai dans N, car s'il était faux, il serait prouvable. Or cet énoncé est de complexité logique suffisamment simple pour que sa prouvabilité dans une théorie cohérente capable de coder l'arithmétique entraîne sa vérité dans N (on n'a pas besoin de supposer que N est modèle de la théorie). Il est donc vrai dans N. ressemble à du raisonnement par l'absurde, mais je ne suis pas bien sûr.Salle 12 août 2006 à 08:24 (CEST)

Effectivement l'article utilise la notion de vérité dans un modèle qui est classique, et tel que rédigé le raisonnement que tu soulignes est bien un raisonnement par l'absurde (tiers-exclu, soit vrai, soit faux). Tu as raison. Mais il s'agit de montrer qu'un énoncé n'est pas prouvable : il n'existe pas d'entier qui code une preuve de l'énoncé. Pour un tel énoncé négatif, les intuitionnistes acceptent ce qu'un mathématicien appelle habituellement raisonnement par l'absurde ("introduction de la négation" en jargon théorie de la démonstration). On pourrait reformuler le raisonnement directement, sans parler de vérité. Mais je n'ai pas du tout cherché à être intuitionniste, et je m'aperçois qu'effectivement je ne le suis pas. Par ailleurs même si la preuve n'était pas intuitionniste (mais elle l'est ou peut l'être), le résultat reste forcément valide pour la prouvabilité intuitionniste, qui est moins forte que la prouvabilité classique. J'ajoute une note à ce sujet dans l'article.

Ca me va.

• Les axiomes de Peano conviennent. Je comprends : les axiomes de Peano constituent une théorie qui vérifie les hypothèses du théorèmes. Est-ce bien ça? Si oui, ne faudrait-il pas plutôt le dire ainsi?

ok, je vais reformuler.

Ok

Csqces du premier théorème

• Là est démontrée une pté importante : dans la théorie T une pté G est démontrable si et seulement si T et nonG est contradictoire. L'implication directe me convient ; en revanche, je ne comprends pas l'implication réciproque j'essaie de reconstituer : supposons T et non G contradictoire. Par déf, cela signifie que G est vraie dans (T et nonG) ; donc G est vraie dans T ; donc G est démontrable dans T. Des deux donc, le premier me semble acceptable même si je serais incapable de le démontrer, n'étant pas logicien. En revanche, le deuxième me semble confondre vérité et démontrabilité, ce que la partie II nous enjoint à ne pas faire. Quid?

Il n'y a pas à parler de vérité. C'est de la démonstration, et c'est à peu près le raisonnement par l'absurde usuel en math, mais sous une forme tellement abstraite, qu'on ne le reconnait pas je suppose. Je rerédige dans l'article, en tentant d'être plus clair.

Là, je ne comprends pas ; j'essaie de dire plus loin.

• Le théorème de Gödel est reformulé en utilisant cette pté ; mais il l'est deux fois (avant et après la démo de ladite pté), et ça ne facilite pas la lecture.

En fait après la preuve, ça n'est pas exactement une reformulation, et ça permet d'enchaîner avec la suite. J'ajoute un mot avant pour expliquer la suite, rien de mieux ne me vient rapidement à l'esprit pour le moment. N'hésite pas à modifier si tu vois mieux.

A la relecture, ça ne me pose plus de problème ; donc, ça va.

• Pour la dernière remarque de ce chapitre (en gros : l'énoncé indécidable obtenu est exprimable dans le langage de l'arithmétique ; et c'est de plus un énoncé assez simple) : il n'est pas clair si cette précision sur le théorème esst une trivialité qu'on devrait savoir faire seul, ou si c'est dur.

ce n'est pas une trivialité. C'est parce que les codages sont arithmétiques. J'ai un peu modifié la formulation dans l'article. D'autre part logiquement assez simple ne signifie pas vraiment simple, je précise également.

Ca me paraît plus clair.

• Bonjour. En relisant la démonstration, et bien qu'il soit mentionné que l'on présume que la théorie T considérée dans le contexte satisfait les hypothèses « utiles », il ne me semblerait pas inutile d'expliciter une propriété-clé de T impliquée dans la déduction ici : la cohérence. Actuellement, on peut lire que : « T augmentée de non G est contradictoire » conduit à « non G est source de contradiction dans T » ; cela est valide bien entendu dans l'hypothèse implicite que T est non contradictoire — autrement, on ne pourrait pas, à mon sens, conclure (décider) sur la source contradictoire (non G ? S une sous-théorie de T ?). Merci pour votre avis sur la pertinence de l'explicitation proposée. --nha de Lyon 26 janvier 2007 à 00:10 (CET)

Ta formulation « non G est source de contradiction dans T » est trompeuse. Pense que T est l'arithmétique de Peano, tu fais ce genre de raisonnement sans invoquer la cohérence de l'arithmétique. "T+non G contradictoire" signifie de "T+non G on déduit l'absurde", ce qui est quasiment pareil que "dans T de non G on déduit l'absurde" (quand on formalise la preuve, ça dépend du choix du formalisme, mais c'est en général complètement évident). C'est du même ordre que (A et B) => Absurde équivaut à A => (B => Absurde), pour donner une idée (mais attention : T peut être infinie). On a besoin que ce soit non G pour la suite bien-sûr, mais ce bout de raisonnement serait tout aussi valide en prenant à la place une formule de T. La cohérence de T n'est pas nécessaire pour ce raisonnement. Ca marche très bien si T est incohérente (mais ça n'a pas grande signification puisqu'alors T démontre n'importe quoi). Par contre G indécidable dans T n'est pas possible si T incohérente. C'est là qu'a déjà servi l'hypothèse de cohérence, pour le résultat que l'on cherche à démontrer. J'avais pensé à mettre un avertissement pour dire que ces démonstrations sont effectivement très simples mais non usuelles, et, par expérience, il n'est pas si simple de se rendre compte qu'elles le sont ! Ceci dit je ne dis pas qu'il n'y a pas moyen de mieux expliquer. Proz 26 janvier 2007 à 01:37 (CET)

Csqces du second théorème

• Dans la petite pruve, il y a une utilisation de la pté du parag précédent, non? Peut-être le dire explicitement faciliterait la lecture.

c'est ce que j'entendais par "d'après ce qui précède", je précise.

D'accord

• Pourquoi la preuve est-elle qualifiée d'esquisse? Elle m'a semblé complète.

Il y a du codage. L'énoncé non coh(T) , c'est "il existe un entier qui code une preuve de l'absurde dans T". De même dans T' . Donc " non cohT a pour conséquence non cohT' " demande de fait un peut d'arithmétique, même si c'est intuitivement tellement évident que personne ne prendra la peine d'en dire plus. J'ai reformulé pour que ce soit plus clair.

D'accord.

• En revanche, le résultat une théorie qui démontre un énoncé exprimant qu'elle n'est pas cohérente, peut très bien ne pas être contradictoire, comme on le déduit du second théorème d'incomplétude lui-même ! est super choquant aux yeux du profane que je suis, infiniment plus que les théorèmes dans leur forme courante. J'imagine qu'étant conséquence immédiate des théorèmes eux-mêmes, il n'a pas fait l'objet de suite particulière ; mais peut-on quand même trouver un exemple, le plus accessible possible, où ce genre de phénomène se produit réellement? Ou dire au moins où on ne risque pas de le rencontrer? Ou, au contraire, si on est susceptible de le rencontrer n'importe où? En gros, j'ai du mal à le croire sans le voir.

L'exemple est quasiment donné : Peano+non coh(Peano). fort heureusement c'est pathologique. Je précise dans l'article.

Précisions rassurantes.

Partie II

• Je ne comprends pas très bien l'enchaînement entre les deux assertions en gras ; d'ailleurs, je crois que je ne comprends pas la deuxième assertion :T est une théorie récursivement axiomatisable qui permet de formaliser "suffisamment d'arithmétique", et dont tous les axiomes sont vrais dans N Que signifie que les axiomes de T sont vrais dans N? Que ce sont des théorèmes de l'arithmétique classique? Mais dans ce cas, juste pour pouvoir exprimer, ces axiomes/théorèmes, il faut déjà disposer d'une construction de l'arithmétique, non? Ca ne doit pas être ça, car on demande ensuite à T, précisément de fonder l'arithmétique. De mon point de vue de profane, on est en train de parler d'une théorie qui doit fonder l'arithmétique, mais qui s'exprime dans, ou au moyen de, l'arithmétique. C'est troublant, et une explication pourrait être éclairante.

J'essayerai (plus tard) de trouver qqchose. La vérité dans N, c'est ce que j'essaye d'expliquer ensuite. Je propose de revenir sur ce point après avoir répondu à "sur la notion de vérité, plus en détail". Quand j'essaye de préciser, ça introduit des redondances. Par ailleurs, la vérité dans N se définit, disons en théorie des ensembles. Il n'est pas question de fondation. Il n'y a pas de raison de se restreindre mathématiquement pour étudier les théories arithmétiques.

Je ne vois pas précisément de qelles théories on parle ; je suis assez convaincu que l'axiomatique de Peano rentre là-dedans ; mais par exemple la théorie ZF? Elle modélise suffisamment d'arithmétique ; mais ses axiomes ne sont ni vrais ni faux dans N? Qu'en fait-on? L'impression que j'ai c'est qu'on est en train de parler d'une théorie qui en définitive modélise l'arithmétique, et rien d'autre (et qui a le bon goût de ne pas introduire d'énoncé faux, mais c'est la moindre des choses). Si tu arrives à voir ce qui bloque, je serai content.

Il y a effectivement une précision à apporter, vis à vis des énoncés du début. Là je suis passé sans le dire dans le langage de l'arithmétique. Pour ZF il faudrait parler des énoncés arithmétiques conséquences de ZF et vrais. Mais je préfère restreindre le langage pour simplifier. Je précise dans l'article.

• Pour l'enchaînement que je ne comprends pas, je pense qu'il s'éclairera tout seul si je sais de quoi on parle.

j'ai ajouté un mot dont je ne suis pas sûr qu'il éclaire.

Ca me paraît clair.

• Une parenthèse contient deux remarques : il s'applique à moins de théories, on ne peut le formaliser dans l'arithmétique, pour en déduire le second théorème d'incomplétude.. J'ai réussi à me convaincre de la première tout seul, en revanche pas de la deuxième. On pourrait dire, pour ce genre de remarques, soit c'est facile, pour le lecteur, soit c'est un nouveau théorème que je ne vous démontre pas. Enfin, trouver un moyen que les trucs triviaux et les trucs difficiles ne soient pas mis sur un même plan.

ok, c'est le th. de Tarski. Je mettrai une note. [fait]

Très bien

• on pourra ne supposer que la vérité dans N des théorèmes de cette complexité logique, et on obtiendra un théorème équivalent au premier théorème d'incomplétude tel que démontré par Gödel. Pour moi, cela signifie qu'en prenant la théorie précédente à laquelle on ajoute comme axiomes tous les théorèmes de cette complexité logique, et en réécrivant le théorème de type 1 pour toutes ces théories, on a évidemment un énoncé plus fort (au sens large) que celui mis en gras ici ; évidemment moins fort (au sens large) que Gödel ; et, non évidemment, aussi fort que Gödel. Si c'est ça, je pense que cela pourrait être reformulé de façon plus explicite ; et qu'on pourrait dire pourquoi l'assertion non évidente est vraie, ou sur quoi repose la démo (c'est peut-être la fonction de la parenthèse, dont je n'arrive pas à voir précisément la fonction, justement).

c'est la fin de l'article, je mettrai un lien.

en fait l'indication y est déjà. Je reformule un peu le tout. On pourrait aussi remplacer le paragraphe, par un renvoi à la fin de l'article sans tenter d'explication.

Le bout d'explication me paraît intéressant, et rassurant, donc pas à enlever. Ce sur quoi je veux insister, c'est en fait le on peut supposer (...), que je comprends comme : on considère une théorie qui a au moins comme axiomes (...). Le problème du terme supposer, c'est qu'il peut vouloir dire, on fait une hypothèse, ou on choisit un axiome, ce qui n'est pas tout à fait la même chose ; il me semble que c'est ce second sens ici, et qu'une reformulation pourrait éviter l'éventuelle ambiguïté et rendre les choses plus claires.

reformulation dans l'article : j'espère que c'est plus clair. si je trouve mieux je reformulerai (On choisit les axiomes de façon à satisfaire l'hypothèse si la théorie est cohérente).

• Voilà comment je comprends la fin de cette partie : on fait quelques considérations (que je ne cerne pas bien) historiques et épistémologiques sur la notion de vérité, plus la déf de la vérité dans N. Je ne vois pas ce que ce développement apporte à la compréhension de l'article (mais comme je n'ai pas lu la suite...). S'il est superflu, peut-être en faire un article lié?

il n'est pas superflu : l'article utilise la vérité dans N. Les reformulations du 1er th. de Gödel en terme de vérité (du genre "il existe une formule vraies non démontrable") sont courantes. Sans en parler on comprend mal la dissymétrie dans l'indécidabilité, et le théorème lui-même (Gödel n'a pas, je crois, parlé de vérité, mais l'avait en tête, d'après des lettres ultérieures). Je souhaiterais que ce § permette, entre autre, de comprendre ce qu'est la vérité dans N.

Je réponds plus loin.

Je corrigerai la seconde partie selon les remarques ci-dessus [fait].

Sur la notion de vérité, plus en détail

• La notation bien connue avec les petits bâtons, ça m'a longtemps troublé... Peut-être faire mieux ressortir le terme unaire, et abandonner ces remarques seraient plus productif.

j'espérai que ce serait plus clair. Pour moi il s'agit de faire comprendre que la syntaxe ne fait que refléter l'idée très intuitive d'entier, que l'on utilise, par exemple quand on compte des votes avec des bâtonnets. je pense que je me suis mal exprimé, s'il faut abandonner, j'abandonnerai, mais avant peux-tu expliquer ce qui trouble ?

C'est peut-être juste le fait de passer de but en blanc de considérations sur des formules atomiques closes à une remarque, assez naïve sur un système de numération. Je ne sais pas trop quel lecteur n'ayant pas au moins une idée de ce qu'est un système de numération arrivera ici, et donc je ne vois pas trop le public pour cette remarque.

ok, je supprime (bien que pas tout à fait sûr qu'il soit si clair que ça que pour quiconque en arrive là, sss0, et ||| c'est "pareil").

• On utilise le terme polynôme. Est-ce dans le sens mathématique courant? Si oui, il faudrait un lien, je pense.

ok;, lien + précision ajoutés

Ok

• Le terme formule atomique close. Close est expliqué, mais pas atomique, il n'y a pas non plus de lien, donc je n'ai pas compris ; je pense que cela doit se ramener aux formules du type (avec notations habituelles) 2=2, 2=3, 1<4 et 4<2, et tout ça...

j'ajoute une explication et un lien. les formules atomiques que tu écris sont closes. On a aussi x + yz = 1+ 2x etc.

Lien utile.

• J'ai l'impression qu'il y a équivalence entre sans quantificateur et sans variable ; si c'est le cas, il faudrait le dire.

non ce n'est pas équivalent.

Pareil avec le lien précédent ; ne faudrait-il pas dire qu'une formule close, c'est sans variable libre?

pour les formules atomiques toutes les variables sont libres ; ça m'a semblé plus simple de ne pas préciser.

• je ne suis pas sûr que le paragraphe où on parle du quantificateur universel ne pourrait pas être mieux rédigé ; peut-être rajouter, un a priori dans cela demande une infinit" de varififcations ; et préciser Les énoncés universels qu'on parvient à démontrer le sont souvent au moyen d'une récurrence, à la place de la phrase actuelle qui pourrait laisser l'impression que tous ces énoncés peuvent être démontrés, et que le habituellement ne porte que sur le mode de démo utilisé.

ok, c'est justement ce que je voulais dire par la phrase relevée ensuite, qui n'a pas l'air claire. Je reformule.

Ok

• Je ne comprends pas ce que cette phrase  : Au passage on a perdu quelque chose, comme l'énonce précisément le théorème de Gödel. signifie ; elle pourrait être explicitée.

reformulé

Je crois que de toutes les modifs, c'était la plus nécessaire. Bien plus clair comme ça.

• au sens informel de cette notion, je pense que ça porte sur preuve. Je pense que ça fait référence à la notion de preuve formelle telle qu'expliquée en méthode formelle (informatique). Si c'est ça, il faudrait un lien, ou même supprimer l'incise, car je pense que pour la majorité des gens, preuve ne signifie pas a priori preuve formelle.

j'ai exprimé les choses autrement, le vocabulaire était probablement mal choisi.

Pour cette remarque et la suivante, c'est Ok.

• Dans les cas abordés ci-dessus, ces preuves sont effectivement formalisables dans les théories pour lesquelles on démontre les théorèmes de Gödel. Encore une fois, on part sur quelque chose d'assez éloigné des considérations initiales, pour ce que j'en comprends. J'imagine encore que formalisable est employé dans le sens précédent. Et ça soulève plus de questions queça n'en résout, j'ai l'impression : une peurve formalisable, j'imagine que c'est encore plus dur à avoir qu'une preuve tout court? Est-ce que c'est la même chose que d'avoir un moyen mécanique de décider la vérité? Où est-ce que ça se situe par rapport à intuitionnisme/logique classique?

idem

remarque : une preuve formelle : c'est la vérification du fait que c'est une preuve qui est mécanique, pas la recherche qui correspond au "moyen mécanique de décider la vérité". Ce serait une preuve au sens mathématique usuel où l'on aurait absolument tout explicité.

Vérité et démonstrabilité

Les remarques pour lesquelles j'ai renvoyé ici sont toutes liées à ce point. Quelle différence entre vérité et démontrabilité? J'en suis là, surtout après cette phrase : L'énoncé de Gödel, qui est vrai et non démontrable est justement un énoncé universel, appellons le ∀ x H(x). Prenons le cas de l'arithmétique de Peano. Quand on définit précisément l'énoncé, on montre que pour chaque entier n, H(n) est prouvable dans l'arithmétique de Peano. Mais on ne peut pas démontrer ∀ x H(x). : tout énoncé clos dans une théorie (satisfaisant les hypothèses utiles?) a une valeur de vérité. Parmi les énoncés vrais, certains ne sont pas démontrables. Car en fait, dans une démonstration, on ne peut faire qu'un nombre fini d'étapes, et même si la récurrence permet de pallier ce problème pour certaines classes d'énoncés, il y en a certains où elle échoue ; le théorème de Gödel exhibe ces énoncés H(n), qui sont démontrables et donc vrais ; donc, par définition ∀ x H(x) est vrai ; en revanche (pour des raisons de complexité logique, je crois?) il n'est pas démontrable.

H(n) est vraie et donc démontrable pour des raisons de complexité logique, mais je ne pense pas qu'il faille préciser à cet endroit. Pour ∀ x H(x) n'est pas démontrable, il faut le bon énoncé et il y a une preuve à faire. Là j'essaye d'expliquer ce qui fait que le th. de Gödel peut être vrai, je ne donne aucune idée de la démonstration.

Mais ceci reste obscur :Étant donné un énoncé G, notons non G sa négation. On montre facilement qu'un énoncé G n'est pas démontrable dans T si et seulement si la théorie T + non G (la théorie T à laquelle on ajoute l'axiome non G) est cohérente. En effet, si G est démontrable dans T, T + non G est évidemment contradictoire. Réciproquement, supposons T + non G contradictoire. Cela signifie que, dans la théorie T, on peut déduire de non G une contradiction. On en déduit que G est conséquence de T (c'est un raisonnement par l'absurde).. Pour la dernière phrase, je la comprends par G est démontrable dans T, parce que c'est ce qu'on voulait obtenir. Maintenant, voilà mon problème : je considère deux classes d'énoncés dans T : celle des démontrables et celle des vrais, la première étant incluse dans la seconde, et même strictement. Le problème, c'est que si je prends dans cet exemple G=(∀ x H(x)) de tout à l'heure, ben G est vrai dans T, donc G+non T est contradictoire, et donc On en déduit que G est conséquence de T ? donc que G est démontrable dans T, Ce qui n'est pas le cas.

Vrai dans une théorie n'a pas de sens. C'est vrai dans un modèle : ici toujours N. Ce sont les axiomes de la théorie, qui peuvent être vrais dans N, et dans ce cas tous les théorèmes le sont. Pour l'énoncé de Gödel pour T, justement T+non G n'est pas contradictoire, mais n'a pas N pour modèle (bien que vérifiant la récurrence, si T est Peano, ce qui peut être contre-intuitif). N'étant pas contradictoire cette théorie a quand même des modèles (non-standards). Je pense que ton problème c'est en partie que tu interprètes "contradiction" en terme de vérité. Mais c'est juste une proposition absurde, disons la conjonction d'une proposition et de sa négation, ou 0=1 dans l'arithmétique de Peano. Dire que Peano+non G est contradictoire, c'est dire que l'on démontre 0=1 dans Peano+non G. J'ai précisé dans l'article. Je ne sais pas si c'est suffisant.

Non, ce n'est pas très convaincant. Tu dis juste ce qu'est une contradiction sur un exemple, et le problème n'était pas là. J'ai enlevé, ça me paraissait d'un niveau un peu trop inégal à ce qu'il y a avant et après. Je pense que ta première phrase (Vrai dans une théorie n'a pas de sens.) m'a éclairé, et je propose une réorganisation de la section en conséquence sur cette page.Salle 20 août 2006 à 14:47 (CEST)

Excusez-moi de m'immiscer dans votre discussion. Je voudrais distinguer trois concepts : validité (satisfaction dans tout modèle), démontrabilité et vérité (un concept philosophique, très important, approché par les deux autres). On notera que j'introduis un quatrième concept la satisfaction et que seuls les deux premiers concepts sont mathématiques. Personnellement, je commençais mon cours d'introduction à la logique par l'explication de ces concepts avant d'attaquer le corps du débat. En conséquence, j'appellerais validité ce que vous appelez vérité. Pierre de Lyon 28 août 2006 à 08:43 (CEST)

Je suis bien-sûr d'accord pour la distinction entre ces 4 concepts. Dans l'article, vérité fait le plus souvent référence à "satisfaction dans le modèle standard de l'arithmétique". C'est assez usuel quand on parle du th. de Gödel (une formule vraie mais non démontrable). Le but du § est de faire comprendre dans le cas particulier de l'arithmétique la différence entre "vraie dans N (au sens de Tarski) et démontrable disons dans Peano. Ca me semble un exemple où les choses sont particulièrement claires, et il ne faudrait pas que le § devienne un "cours d'introduction à la logique" en général. Je souhaiterais, que la majeure partie de l'article soit lisible par un mathématicien non-logicien. Je me suis laissé aller récemment à parler de modèle non standard, et c'est peut-être déjà faire trop de logique. Je suis d'accord que "vérité" est un terme très chargé, j'avais pris d'ailleurs quelques précautions à ce sujet dans une version antérieure, mais la phrase a récemment disparu lors de remaniements. J'aurai tendance à garder tout de même vérité, qui est quand même aussi utilisé dans ce sens, qui me semble plus parlant que validité et satisfaction, et qui est plus en phase avec les énoncés plus ou moins vulgarisés du th. de Gödel que l'on peut rencontrer. Je propose plutôt une phrase expliquant que la vérité Tarskienne n'est qu'une définition mathématique, pas "la" vérité (dit autrement bien-sûr). Proz 28 août 2006 à 10:54 (CEST)

Je propose plutôt une phrase expliquant que la vérité Tarskienne n'est qu'une définition mathématique, pas "la" vérité (dit autrement bien-sûr). D'accord, mais en gardant à l'ersprit ce que Jean-Yves Girard fait dire à Gödel répondant à Monsieur Homais (in Le théorème de Gödel ou une soirée avec M. Homais, Sciences et Avenir, Janvier 2000 ) « la principale force du tarskisme c'est sa platitude ».

Ah oui, c'est moi qui avais râlé contre les précautions prises initialement par Proz sur le terme vérité. Disons que je ne vois pas ce que ça vient faire là. Il me semble clair que cet article parle de maths et pas de philo, et dire que le terme vérité prend d'autres sens ailleurs ne me paraît pas nécessaire. Un peu comme si à chaque fois qu'on dit corps, il fallait préciser <<Attention, en médecine, ça a un sens différent.>>.Salle 28 août 2006 à 11:41 (CEST)

Je défends faiblement le point de vue de Pierre de Lyon sur le remplacement systématique de «vrai» par «valide», tout en soulignant que le mot «vrai» est couramment utilisé par les mathématiciens comme un synonyme de «valide». Je pense comme lui que l'usage de ce mot est un peu trompeur. Néanmoins je ne me battrai pas comme un chiffonier, priorité à l'avis de celui qui a travaillé sur l'article et lui a donné sa cohérence ! Cela étant et pour dire du bien plutôt que du mal, le plan choisi (une partie 1 qui ignore complètement la théorie des modèles suivi d'une partie 2 centrée sur celle-ci) est très judicieux -- les sources confuses sont typiquement celles qui font des allers-retours permanents entre les deux points de vue. Touriste * (Discuter) 28 août 2006 à 12:08 (CEST)

Oui, mais valide dans N ça ne se dit pas trop, il faudrait dire plutôt satisfait dans N. L'usage de "vrai" ou "faux" sans préciser (j'ai essayé d'éviter tant que ce peut, mais il en traîne forcément, et de toute façon c'est courant dans ce contexte) fait clairement référence au fait qu'il y a un modèle standard, et que c'est vrai dans ce modèle. Le remplacement ne peut être aussi simple, et ça n'améliorera pas la lisibilité de mon point de vue. Proz 28 août 2006 à 12:26 (CEST)

Surtout il ne faut pas rentrer dans les débats entre logiciens sur Tarski, et la vérité tarskienne. Mathématiquement son efficacité, par exemple en théorie des ensembles pour ne pas prendre la théorie des modèles, ne fait aucun doute. Je pense quand même rétablir les "précautions", qu'on le veuille ou non un article sur le th. de Gödel doit affronter ce genre de problèmes, plus qu'un article sur la théorie des corps. Proz 28 août 2006 à 12:11 (CEST)

Bon, je n'ai pas d'argument contre ; j'imagine que c'est mon goût personnel qui est trop personnel sur ce coup.Salle 28 août 2006 à 12:19 (CEST)

Comme Touriste et j'ai un point de vue globalement positif sur l'article. je suis d'accord avec le plan. Je reviens sur ce que que dit Salle à savoir (je paraphrase) que les mathématiciens n'ont rien à faire de concepts des philosophes, erreur suivant que vous êtes plantonicien ou réaliste, les objets existeront ou n'existeront pas (je simplifie) et la vérité qui leur est attachée aura tel sens ou tel autre. En revanche, la validité sera la même (du moins je l'espère) pour tout le monde. Pierre de Lyon 28 août 2006 à 12:22 (CEST)

Ah non! Je n'ai pas du tout dit ça, même avec la précaution paraphrase. J'ai juste dit que c'était une autre question.Salle 28 août 2006 à 12:27 (CEST)

J'ai rétabli sans trop le modifier un texte précédent dans l'introduction de la partie "vérité et démontrabilité". Je ne suis pas sûr que ça réponde suffisamment aux critiques émises. Proz 28 août 2006 à 13:03 (CEST)

Je ne suis pas sûr d'avoir bien compris la phrase «  on sait le prouver dans une théorie plus forte que celle de départ ». Ou plus précisément, je devrais dire que je pense qu'elle est ambigüe. Il faut me semble-t-il dire qu'elle est plus « forte » au point de vue de sa puissance logique (induction au delà d'$\epsilon _{0}$) mais pas parce qu'on y a ajouté des axiomes qui font que l'on peut maintenant démontrer un théorème que l'on ne pouvait pas auparavant. Pierre de Lyon 28 août 2006 à 13:09 (CEST)

Je ne fais pas référence forcément à la preuve de Gentzen. Je pensais plutôt d'ailleurs à une preuve de cohérence en théorie des ensembles ou plus précisément en logique du second ordre, en donnant le modèle, puisque l'on parle de sémantique. Passer à la logique du second ordre, ce n'est pas exactement ajouter des axiomes mais pas loin. Pour la preuve de Gentzen, qui est bien plus instructive, c'est effectivement plus subtil qu'ajouter des axiomes, puisqu'il utilise un schéma de récurrence plus fort que celui de Peano, mais sur des formules de faible complexité. Donc cela revient bien me semble-t-il à ajouter, mais aussi à enlever des axiomes. On prouve des th. que l'on ne prouvait pas auparavant, mais on n'en prouve plus que l'on prouvait. D'accord pour l'ambiguïté : on utilise "plus fort" dans les deux sens, plus d'axiomes, et la phrase est quand même correcte, ou prouve la cohérence et la phrase devient tautologique. Je ne pense pas qu'il faille rentrer dans ce genre de subtilités dans cet article, en tout cas pas dans ce §. Enfin, exemple artificiel certes, Peano+coh(Peano) prouve la cohérence de Peano, donc ça marche bien en ajoutant des axiomes !

Ce que j'essaye de dire, en fait, et dont l'expression peut sûrement être amélioré, c'est quelquechose comme la vérité (tarskienne) dans N est une notion "idéale", que concrètement les mathématiciens approximent en choisissant (implicitement d'ailleurs) une théorie suffisamment puissante (dit comme ça c'est trop simplificateur mais c'est l'idée, je préfère le dire sur un exemple). Proz 28 août 2006 à 15:49 (CEST)

J'ai conscience que nous planons assez haut (du moins pour le lecteur lambda). Ce que je voulais mettre en évidence, c'était dans l'optique du lecteur lambda précisément qui dirait crûment (-: « Eh bien sûr, l'ami, si tu ajoutes les bons axiomes, tu vas pouvoir le prouver ton théorème! » Pierre de Lyon 28 août 2006 à 17:12 (CEST)

Une remarque (qui est en même temps une question à haute voix)

C'est au sujet de : "la vérité dans le modèle standard de l'arithmétique, les entiers que «tout le monde connaît»" - En qualité de personne formée mathématiquement mais pas spécialiste en logique, j'ai plusieurs fois été intrigué par cette inévitable apparition des "entiers standard" dans la plupart des exposés sur ce genre de questions. Me trompè-je en croyant comprendre que ce qui est important chez eux ce n'est pas que «tout le monde les connaisse» mais surtout que ce soient les mêmes que ceux qui ont été utilisés en amont pour définir des concepts comme "cohérent", "récursivement axiomatisable" voire tout simplement "formule" ? Je ne suis pas assez expert pour exposer ça précisément, mais si je ne suis pas à côté de la plaque, je trouve que c'est clarificateur - ça intrigue vraiment de voir les entiers «les plus familiers» se mettre en trompeuse apparence à jouer un rôle particulier alors qu'ils sont en fait intevenus mais un peu cachés tout au long de la première partie. Touriste * (Discuter) 28 août 2006 à 12:41 (CEST)

C'est une remarque assez subtile. Je ne suis pas sûr de donner une réponse pertinente. Effectivement les entiers interviennent dès que l'on définit le langage. Dans un modèle non standard, les entiers non standards, on ne peut justement pas en parler dans le langage de la théorie, donc il n'est pas question de les utiliser pour les définitions des formules, de la cohérence etc. C'est effectivement indispensable que les notions de formule, preuve, etc. se codent par des entiers (forcément standards). Il est effectivement important que les prédicats "récursivement axiomatisable", "prouvable", etc. veuille bien dire, via les codages par les entiers, donc interprétés dans N, ce que l'on veut. Ceci dit tout ceci sera démontrable, donc vrai dans un modèle non-standard. La phrase "les entiers que «tout le monde connaît»" est très abusive, mais évite de donner des détails. On peut introduire une remarque dans le sens de ce que tu proposes. Proz 28 août 2006 à 13:48 (CEST)

Merci de ta réponse, inutile de mettre une remarque si personne ne se sent sûr. Il est aussi possible qu'il soit essentiel que le N qu'on utilise soit bien ordonné, et encore plus plausible qu'il y ait un peu des deux à la fois ; il faudrait lire pas à pas, vraiment très pas à pas, les démonstrations notamment dans les sections 6-1-2 et 6-1-3 pour se faire une opinion. Donc n'y touchons pas tant que nous ne sommes sûrs de rien, c'est certainement plus prudent. Touriste * (Discuter) 28 août 2006 à 13:56 (CEST)

Je ne proposais qu'une remarque sur le fait que la connaissance des entiers est déjà implicite. Sinon, à la réflexion, je pense que ce que tu dis corresponds au fait que, la vérité dans N est utilisé comme biais commode pour montrer que ce que l'on définit dans la théorie (prédicat de prouvabilité) correspond bien à la "vraie" prouvabilité, que le codage est fidèle finalement (on parle parfois de "réflexion" de la théorie dans elle-même). Il faudrait peut-être plus insister dans la partie codage. Proz 29 août 2006 à 21:40 (CEST)

Conclusion provisoire

Je ne demande pas de réponse à mes questions une par une (ni ne les refuse, d'ailleurs). L'idée est juste que la perception d'un profane peut aider le rédacteur à voir où il peut clarifier son article. Je serai absent pendant plusieurs jours, donc je ne pourrai pas préciser tout de suite mes questions si tu le demandes. En revanche, après mon retour, je veux bien essayer de lire la suite, si certaines de mes remarques ont pu aider, et revenir sur celles qui auront été obscures. Merci.Salle 11 août 2006 à 21:29 (CEST)

cela m'intéresse que ce soit compréhensible par des non-spécialistes, donc ce sera avec plaisir. De toute façon, tout texte de ce genre devrait être relu. Par ailleurs ne faudrait-il pas reporter cette discussion dans la page de discussion de l'article ? Proz 14 août 2006 à 20:08 (CEST)

Aucun souci pour recopier en page de discussion de l'article. Je vais opérer. Encore quelques jours d'absence, et j'espère finir de lire. Merci.Salle 14 août 2006 à 23:06 (CEST)

Introduction à l'article

J'ai écrit un brouillon pour une introduction : Utilisateur:Proz/Gödel. Bien-sûr la partie du présent article concernant le programme de Hilbert, qui est largement reprise dans cette intro, disparaitrait. Quelques modifications très cosmétiques seraient aussi nécessaires. C'est un peu long. Qu'en pensez-vous ? Proz 29 août 2006 à 21:22 (CEST)

J'ai fait quelques modifications cosmétiques. Pierre de Lyon 31 août 2006 à 13:14 (CEST)

ok, théorie arithmétique ne me gêne pas, mais bon. J'ai juste modérer par un conditionnel l'affirmation finale sur l'intuitionnisme. Je peux opérer la substitution, auf avis contraire. Proz 31 août 2006 à 18:10 (CEST)

Je peux me tromper, mais j'ai l'impression que toutes les allusions à l'intuitionnisme devraient être abandonnées : ce texte doit servir d'intro à l'article sur le théorème de Gödel, et j'ai l'impression que l'intuitionnisme n'a pas de lien direct avec ce théorème, le schéma étant le théorème de Gödel a un lien avec le programme de Hilbert, et ah oui, il y aussi un lien entre le programme de Hilbert et l'intuitionnisme ; pour moi, cela délaie l'information. En définitive, cette intro telle quelle me semblerait plus adaptée à un article Programme de Hilbert. Mais je peux me tromper.

Un autre détail : je ne suis pas convaincu par la formulation des théorèmes ; j'ai l'impression qu'il y a eu tentative d'explication avec les mains, mais qu'en définitive, c'est fait à moitié en langage simplifié, mais pas complètement : il faudrait trouver une vraie formulation en langage simplifié - je sais, c'est dur, et là, je n'ai pas d'idée.Salle 31 août 2006 à 18:20 (CEST)

Pour les allusions à l'intuitionnisme : ça explique le contexte de l'époque, et donne un éclairage sur le programme de Hilbert, mais bien-sûr le tout est à la limite du hors sujet. Un article annexe sur le programme de Hilbert serait probablement la solution (il faudrait alors un peu mieux expliquer d'ailleurs). C'est plus ou moins la raison pour laquelle j'hésite à l'incorporer comme introduction de l'article.

Pour la formulation des théorèmes, pas facile de simplifier sans tomber dans le contre-sens. J'ai trouvé par hasard sur le web cette citation de Ian Stewart que j'aime bien : "Godel showed that there are true statements in arithmetic that can never be proved, and that if anyone finds a proof that arithmetic is consistent, then it isn't!", mais pourtant c'est déjà limite. Peut-être faut-il aller quand même dans cette voie ? [réponse intercalée, je lis la suite] Proz 31 août 2006 à 18:45 (CEST)

Pour l'intuitionnisme, je suis bien conscient de cet avantage. Je dis juste que, pour moi, l'inconvénient (risque de confusion) dépasse l'avantage.Salle 31 août 2006 à 19:01 (CEST)

Grossièrement, le premier théorème énonce qu'une théorie suffisante pour faire de l'arithmétique est nécessairement incomplète, au sens où il existe forcément des énoncés qui ne sont pas démontrables et dont la négation n'est pas non plus démontrable : c'est-à-dire qu'il existe des énoncés sur lesquels on sait qu'on ne pourra jamais rien dire dans le cadre de cette théorie. Sous le même genre d'hypothèses sur les théories considérées, le second théorème affirme qu'il existe un énoncé exprimant la cohérence de la théorie - le fait qu'elle ne permette pas de démontrer tout et donc n'importe quoi - et que cet énoncé ne peut pas être démontré dans la théorie elle-même : il faudrait donc renoncer à ce qu'un discours mathématique ait une valeur de vérité universelle, puisqu'on ne peut même pas savoir s'il est cohérent. Outre les restrictions sur les théories envisagées dues aux hypothèses des théorème, il faut noter que ces deux renonciations (énoncés dont la vérité est inaccessible, cohérence du discours) sont seulement relatives, comme la suite de l'introduction l'indiquera.

Voilà, je tente une reformulation vraiment avec les mains. Je pense que c'est pas mal d'introduire dès maintenant les renoncements auxquels les théorèmes conduisent - avec la réserve d'usage (cf dernière phrase). J'y vais, donc si mon truc est mauvais, n'en tenez pas compte sans discussion, c'est juste un essai de profane.Salle 31 août 2006 à 18:38 (CEST)

C'est pas mal, mais sur la cohérence, ça ne me semble pas tout à fait exact. Je reformule de façon plus interrogative :

Grossièrement, le premier théorème énonce qu'une théorie suffisante pour faire de l'arithmétique est nécessairement incomplète, au sens où il existe forcément des énoncés qui ne sont pas démontrables et dont la négation n'est pas non plus démontrable : c'est-à-dire qu'il existe des énoncés sur lesquels on sait qu'on ne pourra jamais rien dire dans le cadre de cette théorie. Sous le même genre d'hypothèses sur les théories considérées, le second théorème affirme qu'il existe un énoncé exprimant la cohérence de la théorie - le fait qu'elle ne permette pas de démontrer tout et donc n'importe quoi - et que cet énoncé ne peut pas être démontré dans la théorie elle-même. A cause des hypothèses des théorèmes, toute théorie qui prétend formaliser l'ensemble des mathématiques, comme la théorie des ensembles, est concernée. Faut-il pour autant renoncer à ce qu'un discours mathématique ait une valeur de vérité universelle ? Sur quoi se fonder pour savoir s'il est cohérent, puisqu'il semble que l'on ne puisse y arriver par des moyens purement internes aux mathématiques ? Les théorèmes de Gödel ne donnent pas de réponse mais permettent d'écarter celles qui sont trop simples. Il faut déjà noter que ces deux limitations (énoncés dont la vérité est inaccessible, cohérence du discours) sont seulement relatives, comme la suite de l'article l'indiquera.

Proz 31 août 2006 à 19:06 (CEST)

Autre proposition pour l'introduction

Je propose de reprendre le paragraphe de Salle, que j'ai un peu modifié, de le faire suivre du second paragraphe (plus historique) du chapeau de l'introduction que je proposais, de créer un article "ébauche" sur le programme de Hilbert en recopiant le contenu du brouillon d'introduction, de placer un pointeur dans le présent article du genre : pour mieux comprendre le contexte historique voir ... à propos des preuves de cohérence voir ... (pour le moment le même article, mais ça pourrait changer).

J'éliminerais alors tout ce qui concerne le programme de Hilbert et les preuves de cohérence du présent article.

Ca donnera quelquechose d'améliorable (par d'autres éventuellement ;)), mais ça fera une intro à peu près honnête, me semble-t-il ? Proz 31 août 2006 à 19:24 (CEST)

Ca me va!Salle 31 août 2006 à 19:45 (CEST)

J'ai procédé, c'est effectivement mieux que ce que je proposais. Proz 31 août 2006 à 21:58 (CEST)

Proposition d'article de qualité refusée le 2 septembre 2006

Cet article a été proposé comme article de qualité mais a été rejeté car ne satisfaisait pas les critères de sélection dans sa version du 2 septembre 2006 (historique).
Si vous désirez reprendre l'article pour l'améliorer, vous trouverez les remarques que firent les wikipédiens dans la page de vote.

Quelques remarques, ou pointeurs, au sujet de certaines critiques de ce vote, et pour éviter de lancer sur de fausses pistes ceux qui souhaiteraient améliorer l'article.

• une introduction, dont l'absence est déplorée pas de nombreux intervenants, est déjà présente dans la version du 2 septembre (ajoutée le 1er), voir discussion ci-dessus.

• Sur "l'utilisation abusive du th. de Gödel", voir aussi la discussion ci-dessus, sous le titre "Dieu ?".

• Il ya un parti-pris dans l'article, sûrement discutable, qui est d'expliquer comment déduire le 1er théorème de Gödel, du théorème de Matiiassevitch, plutôt que de l'indécidabilité du problème de l'arrêt, via un codage par les formules ∑₁. J'ai pensé que l'énoncé du théorème de Matiiassevitch était plus simple à comprendre pour un non spécialiste (ça évite de parler de ∑₁ et donc de formule), même si la démonstration du th. de Matiiassevitch lui même, qui n'est pas abordée, est bien plus difficile (rmq : le théorème de Gödel est démontré ainsi dans un livre sur le sujet de Yuri Manin). J'ai ajouté une note dans à la partie "codage" expliquant comment déduire le th. de Gödel de l'indécidabilité du pb de l'arrêt. Je pense que ça répond à la critique sur "déduire le 1er th. du th. de Rice".

• Usage du mot "vérité" : voir aussi discussion sur cette page à la fin de "vérité et démontrabilité".

• enfin je signale que je n'ai pas de témoignage d'une relecture scrupuleuse de l'article à partir de la partie 4.

Proz 2 septembre 2006 à 22:11 (CEST)

Au sujet de Matiiasevich, et du probleme d'arret, je propose modestement ce à quoi j'ai contribué pour la page du problème de l'arrêt (cf le paragraphe "consequences" sur le théorème d'incomplétude"...). Le point central, plus que des discussion de codage, c'est de dire qu'il existe un ensemble recursivement enumerable, non récursif (et d'expliquer ce que ca veut dire). Ensuite, à mon sens, il faut laisser l'explication de cette existence à l'article concerné (en l'occurence le pb de l'arret), et donner l'argument de l'enumération algorithmique des preuves. On peut s'inspirer du paragraphe de la page du problème de l'arrêt évoqué. Selon moin il ne fauit parler ni du Xeme pb de Hilbert, ni meme du probleme d'arrêt, mais juste d'enumerabilité récursive --Jawazele (d) 27 avril 2010 à 13:00 (CEST)

Ce qui n'est pas du tout abordé dans ta contribution c'est la "complexité" de la formule non démontrable (une fois les questions de codage réglées, c'est un autre problème). C'est ce qui permet de passer de l'énoncé du théorème de Gödel sur la page problème de l'arrêt, qui est qualifié à juste titre de forme faible, au "vrai" théorème de Gödel. En utilisant l'énumération par un ensemble diophantien (Matiiasevich) ça se décrit plus facilement. Proz (d) 15 décembre 2010 à 01:46 (CET)

typographie

[déplacé ici pour éviter les confusions]

J'ai commencé le travail de correction typographique, qui pourrait à mon avis améliorer grandement la lisibilité de l'article. N'hésitez pas à continuer, car ce travail risque de prendre un certain temps si je m'y attèle seul ! Grob / ? 31 déc 2006 à 13:08 (CET)

Je suis désolé de dire ça, car ça représente sûrement du temps passé si c'est fait à "à la main", mais franchement, je ne crois pas que de changer le gras typographique en gras "tableau noir" améliore la lisibilité. De plus, les lettres deviennent des images (tant qu'il n'y en a qu'une isolée comme ce que tu as fait ça va). Il y a à certe à améliorer, systématiser la typographie des notations mathématiques par ex. (italique pour les variables ...), mais je ne pense pas qu'il faille passer en TeX, ça peut être lourd à charger à la fin, d'autant que l'article est long. (Par ailleurs là on s'intercale dans une vieille discussion sur une version antérieure de l'article, je propose de reporter l'ensemble du dialogue à la fin, quand tu auras lu ceci). Proz 31 décembre 2006 à 13:52 (CET)

Je pense qu'il faut laisser Proz jouer le rôle de chef d'orchestre, car il s'est pas mal investi dans l'article et le connait bien. En ce qui me concerne, je pense qu'il faut encore travailler sur le fond avant d'attaquer la forme. Et si nous décidons d'attaquer la forme, faisons le de façon concertée en se donnant des objectifs acceptés par tous. Pierre de Lyon 31 décembre 2006 à 16:41 (CET)

merci pour ce rôle (mais l'orchestre est bien réduit je crains). Pour l'aspect typographie : sans nouvelles après une semaine, je suis revenu à la version antérieure qui est plus cohérente. Je n'ai pas d'attachement excessif à une certaine typographie, celle actuelle est imparfaite. Sur le travail de fond : eh bien tirons déjà au clair les désaccords (en dehors des questions de vocabulaire). Proz 7 janvier 2007 à 19:40 (CET)

Sur le fond, je pense qu'il faut relire la deuxième partie. Je vais m'y atteler dès que j'ai du temps. Pas pour l'instant.Pierre de Lyon 8 janvier 2007 à 13:53 (CET)

Remarque d'ordre syntaxique

Sous le même genre d'hypothèses sur les théories considérées, le second théorème affirme qu'il existe un énoncé exprimant la cohérence de la théorie : l'expression sous le me semble maladroite, et à mon humble avis la première partie de cette phrase devrait être reformulée. Des avis ? DocteurCosmos - ^✉ 22 mai 2007 à 19:27 (CEST)

Sous des hypothèses voisines ? Proz 22 mai 2007 à 19:57 (CEST)

Et pourquoi pas selon des ... ? DocteurCosmos - ^✉ 22 mai 2007 à 19:59 (CEST)

selon des hypothèses ? Il me semble que ça n'a pas exactement le même sens, on interprète machin selon l'hypothèse truc, on a l'impression de pouvoir faire d'autres hypothèses ; sous ces hypothèses, c'est de la déduction. Peut-être est-ce du jargon de mathématicien (mais courant) ? Est-ce sous + hypo = sous qui gêne ? Proz 22 mai 2007 à 20:11 (CEST)

Oui c'est ça mais c'est pas très grave. « En partant de ces mêmes hypothèses » peut-être... DocteurCosmos - ^✉ 22 mai 2007 à 20:26 (CEST)

Base 1 ?

Une question probablement idiote, le texte mentionne « Les algorithmes en jeu sont essentiellement ceux de l'addition et de la multiplication en base 1. » Ne serait-ce pas plutôt base « 2 » ? Vincent Lextrait (d) 12 avril 2008 à 08:51 (CEST)

Je ne suis pas certain, mais je ne pense pas. Je pense qu'on parle d'une notation à la Peano, avec un seul symbole numérique et une notation en successeur (0 = 0, s(0) = 1, s(s(0)) = 2...), équivalente (au zéro près) à une notation en bâtons (I, II, III), donc en base 1. Ceci dit le terme de base 1 est sans doute abusif, car ce ne peut pas être une numération de position comme en base > 1. - Eusebius ^[causons] 12 avril 2008 à 11:46 (CEST)

C'est bien la base 1, une suite de "petits bâtons" par exemple, additionner c'est mettre bout à bout (éventuellement déplacer un à un), une représentation très proche de l'idée intuitive de nombre entier, et qui est celle choisie dans l'axiomatisation de Peano. J'ajoute (j'ai répondu en même temps qu'Eusebius, je ne l'avais pas lu) que le terme s'emploie et n'est pas vraiment abusif parce que par ex. |||= 3 = 1*1°+1*1¹+1*1². Bon je suis d'accord que c'est un peu limite, parce que la position n'a plus d'importance. Proz (d) 12 avril 2008 à 11:59 (CEST)

3 = 1*1°+1*1¹+1*1², je l'a connaissais pas celle là (ni le contexte), mais j'en ai un grand sourire au lèvre depuis 5 minutes depuis que je l'ai lu; ça me fait penser à la blague éculée : il y a 10 sortent de personnes, ceux qui connaissent le binaire et les autres --Epsilon0 ε₀ 12 avril 2008 à 12:25 (CEST)

On avait eu un grand débat dans mon labo pour savoir si ça méritait l'appellation de numération de position ou pas. Notre argument principal pour conclure à la négative était la non-unicité de la décomposition en facteurs (si l'on a bien un seul symbole et pas de zéro). - Eusebius ^[causons] 12 avril 2008 à 15:12 (CEST)

Je n'ai pas compris l'argument mais je suis d'accord que ce n'est pas une numération de position (à dire le contraire, on risquerait de se faire mal voir des enseignants de CP :) ), puisqu'il n'est pas pas besoin d'attribuer une signification à la position. Proz (d) 12 avril 2008 à 18:32 (CEST)

Je crois que l'écriture "3 = 1*1°+1*1¹+1*1²" m'a surpris, non car ce ne peut être une représentation de la base un, mais parce qu'elle n'est pas homogène avec les écritures uselles en bases 2,3, etc ... vu que l'on pourrait considérer que l'unique chiffre en base un est le nombre zéro (et non pas le nombre un). Mais là bien sûr avec la décomposition 0*1°+0*1¹+0*1²... on ne va pas très loin. Bien sûr la réponse a toute question est 42 A00042 où le chiffre utilisé est "1" --Epsilon0 ε₀ 12 avril 2008 à 22:20 (CEST)

La question de la nécessité (dans l'introduction)

La proposition "il existe des énoncés qui ne sont pas démontrables et dont la négation n'est pas non plus démontrable" peut signifier que l'existence de ses énoncés n'est pas nécessaire. Or l'affirmation de cette nécessité fait partie intégrante du premier théorème. On ne peut donc se dispenser de préciser que les énoncés en question existent nécessairement.

Je ne vois pas comment l'énoncé (du méta-langage) "il existe des énoncés qui ne sont pas démontrables et dont la négation n'est pas non plus démontrable" pourrait impliquer que l'"existence" d'énoncés (du langage de la théorie en question) indécidables (dans la théorie en question) n'est pas nécessaire. C'est au contraire une affirmation d'existence de tels énoncés. D'ailleurs le segment de phrase précédent "une théorie suffisante pour faire de l'arithmétique est nécessairement incomplète" est suffisamment explicite (moyennant peut-être une formalisation de l'expression "suffisante pour faire de l'arithmétique", mais c'est un autre sujet). Répéter le "nécessairement est donc inutile, voire pourrait ajouter de l'ambiguïté. --Michel421 (d) 29 juin 2008 à 15:02 (CEST)

Et en quoi cela pourrait-il rajouter de l'ambiguïté?

Parce que le premier "nécessairement" a joué son rôle dans un certain contexte. --Michel421 (d) 29 juin 2008 à 17:08 (CEST)

Le "nécessairement" marque la quantification (sur les théories suffisantes pour faire de l'arithmétique). Ca me semble également plus clair de doubler (par "forcément" ou "nécessairement") : il s'agit de "traduire" la proposition qui précède. Maintenant on peut espérer que cela aille de soi, mais ça ne rajoute sûrement pas de l'ambiguïté de doubler.

Pour la formalisation de "suffisante pour faire de l'arithmétique" : c'est fait dans la suite, ce n'est pas à cet endroit de l'article qu'il faut formaliser (je précise pour éviter tout malentendu, même si tu n'as pas écrit le contraire). Proz (d) 30 juin 2008 à 08:24 (CEST)

omega-cohérence

Epsilon0 préfère parler d'omega-cohérence dès l'introduction. Je persiste à penser que ça ne sert à rien d'être précis à ce niveau (risque de perdre le lecteur sur des fausses pistes). La omega-cohérence n'est pas quelque chose de très important, par exemple on trouve l'énoncé suivant du 1er th. "Il existe une formule (Pi^0_1) vraie (dans N) qui n'est pas démontrable" : c'est exactement le th. de Gödel di on précise Pi^0_1, inutile de parler de omega-cohérence (qui revient à dire que la négation de cet énoncé n'est pas démontrable).

Pour l'autre proposition, qui est d'écrire un article à ce sujet (lien rouge), ça pourrait être une bonne idée, à condition d'élargir aux autres hypothèses de cohérence (comme la cohérence simple d'un côté, l'hypothèse que toutes les formules démontrables sont vraies de l'autre), et de ne pas y attribuer d'importance excessive. Le titre peut rester omega-cohérence, au pire ce serait un lien après renommage.

Je propose donc de ne pas en aprler dans l'introduction, et de reporter le lien rouge dans la suite de l'article, plus en situation (et de l'appeler omega-cohérence et pas ω qui devient Ω comme première lettre du titre, garder ω-cohérence comme lien). Proz (d) 16 novembre 2008 à 11:16 (CET)

Je n'ai placé cette précision (retirée par Proz) dans l'intro que car elle me semblait appelée par :"Gödel faisait une hypothèse de cohérence un peu plus forte <ajout>appelée ω-cohérence"<ajout>.

Le lecteur, qui est forcément intelligent mais qui ne sait pas forcément tout, peut à se stade se demander ce que peut bien être une "cohérence plus forte" que la cohérence! Et on le laisse avec cette allusion, sans précision? De plus le texte parlait de "cohérence" et de "cohérence simple". Donc j'ai voulu rentre tout ceci + cohérent intelligible.

Sinon pour le nom, dans la traduction aux éditions du Seuil c'est ω-consistant, mais c'est un détail. --Epsilon0 ε₀ 16 novembre 2008 à 21:35 (CET)

En gros c'est un choix de présentation : ne pas tout dire tout de suite, pour les raisons évoquées ci-dessus. De plus les présentations récentes insistent beaucoup moins sur la omega-cohérence (traduction courante également). Cohérence simple : on ne précise que pour distinguer d'autres hypothèses de cohérence. Proz (d) 17 novembre 2008 à 00:04 (CET)

G donné par le théorème ou la démonstration du théorème ?

A propos d'une autre modification dans le paragraphe "Conséquences immédiates du premier théorème d'incomplétude" :

• tout d'abord il s'agit bien d'un énoncé G obtenu par le théorème, quelque soit la démonstration. Les considérations du début n'utilisent pas la forme particulière de l'énoncé donné par Gödel. Dans le paragraphe sur la th. des ens., on utilise que l'énoncé est arithmétique, ce qui n'est peut-être pas évident d'après l'énoncé du début, et on annonce à mots couverts (aucun sens d'être précis à cet endroit) qu'il va être Pi_1, ce qui là n'est pas dans l'énoncé du début. Je propose de parler de la démonstration juste à cet endroit.
• Je préfère ne pas utiliser G(T) pour marquer que G dépend de T, c'est peu usuel, on pourrait utiliser une mise en indice, mais ça semble assez inutile à ce stade, de plus la notation est cohérente (en prenant G) avec la suite de l'article.

Proz (d) 16 novembre 2008 à 16:17 (CET)

Pour rendre compréhensible ce que dit Proz ici, je mets le diff de mes modifs d'hier, vu que mon "G(T)" n'apparaît plus dans la version actuelle.

Mon soucis était double :

• 1. ne pas laisser croire que tout énoncé indécidable dans ZF est arithmétique (la formulation pouvait le laisser entendre, càd était peu claire).
• 2. Préciser, ce qui a été retiré, "L'intérêt de la démonstration de Gödel est qu'elle permet pour toute théorie T satisfaisant les conditions du théorème de construire un énoncé précis G(T) qui sera indécidable dans T. "
  • Qui me semble intéressant pour comprendre en quoi le thm se transmet à toutes les sur-théories cohérentes et récursives de AP et via, implicitement, qu'il n'est pas contournable par une théorie plus "complète". (Enfin si par le théorème de Lindenbaum, mais là c'est plus récursif; en passant ce pourrait être ajouté dans l'article).
  • Maintenant en effet la notation "G(T)" est inhabituelle, mais je fais ce que je peux sur mon petit notepad et je suis nul en jolies formules unicodes ou Latex. ;-).--Epsilon0 ε₀ 16 novembre 2008 à 21:38 (CET)

• Le fait qu'il n'y a pas d'extension récursive complète : c'était déjà dit explicitement à la phrase suivante.

• "énoncé précis" me gênait un peu : l'énoncé construit dépend du codage. En fait tous les énoncés de Gödel qui affirment leur propre non prouvabilité sont bien équivalents, puisque l'on peut montrer qu'ils sont équivalents à la cohérence de la théorie, mais c'est + ou - la preuve du second théorème d'incomplétude ... En fait à ce niveau de l'article on a juste un énoncé indécidable arithmétique. C'est un peu une question de cohérence de l'article. Proz (d) 16 novembre 2008 à 23:58 (CET)

Ok, tes dernières modifs amiliorent ce que j'ai fait et tu as une meilleure vision de l'ensemble de l'article que moi. --Epsilon0 ε₀ 17 novembre 2008 à 21:59 (CET)

Explication

Je suis revenu sur une partie des modifications de User:Sherbrooke sur l'article : outre le croquignolet "Les fonctions récursives primitives ont plusieurs usages" (qui ne veut rien dire dans le contexte, j'ai précisé la formulation précédente), certaines sont de simples effacements d'articulation logique sous prétexte de "PdV" ou de "subjectivité". Quand il pouvait y avoir ambiguïté j'ai reformulé. J'ai bien sûr laissé les modifications correctes (ça aurait été plus commode si ça n'avait pas été mélangé), désambiguïfier le "à recycler". Il se trouve que je venais de laisser un mot sur Discussion_Utilisateur:Sherbrooke#À noter que, pour lui signaler un désaccord sur certaines interventions, dans le style de celles-ci (abus des accusations de "PdV" et de "subjectivité", pour une correction mécanique). Proz (d) 28 novembre 2008 à 00:55 (CET)

Vérité et incomplétude

La phrase « C'est un théorème d'incomplétude, plus faible cependant que le premier théorème d'incomplétude de Gödel, car il s'applique à moins de théories, les hypothèses étant nettement plus fortes. » ne me satisfait pas. Oui les hypothèses sont plus fortes, mais la conséquence est plus forte aussi, donc le théorème dit quelque chose de différent, on ne peut pas le dire plus faible. --Pierre de Lyon (d) 6 mai 2009 à 16:25 (CEST)

Il s'agit du second des deux énoncés. Je ne vois pas que la conclusion soit plus forte : s'il y a un énoncé qui n'est pas démontrable et dont la négation ne l'est pas non plus, l'un des deux est vrai dans N. Le premier ce déduit aussi du théorème de Gödel : si la théorie des énoncés vrais dans N était récursivement axiomatisable, elle en satisferait les hypothèses, or il ne peut y avoir de proposition indécidable dans cette théorie. Pour des énoncés équivalent au théorème de Gödel "sur ce moule", on peut se restreindre aux énoncés Pi^0_1 vrais. Par contre le théorème de Tarski (l'ensemble des énoncés vrais n'est pas arithmétique) n'est pas comparable, même si "plus simple" que le théorème de Gödel. Proz (d) 6 mai 2009 à 21:12 (CEST)

Introduction

Excusez mon insistance sur le texte de l'introduction, qui me semble déjà d'un très bon niveau et pour laquelle je recommande de ne pas écrire à propos du premier théorème qu'en conclusion "il existe des énoncés sur lesquels on sait qu'on ne pourra jamais rien dire", ce qui me semble une formulation trop forte. D'ailleurs, rien qu'écrire cela sur ces énoncés, c'est faire une affirmation (et laquelle!) sur eux.

Il ne s'agit pas bien sûr d'entrer dans trop de détail/sophistication... dès l'introduction, juste d'essayer de trouver une formulation à la fois simple et compatible d'un autre niveau de lecture (j'admets que ce lecteur averti passera rapidement aux paragraphes suivants, faisant fi d'une introduction, mais il reste les cas intermédiaires). Si c'est correct, et si c'est possible...
Gerard (in space...) (d) 20 septembre 2009 à 23:17 (CEST)

J'ai modifié pour éviter de fausses interprétations, mais l'argument ne me convainc pas : le fait que l'on ne puisse pas démontrer un énoncé dans une théorie T cohérente donnée, ne se démontre pas dans cette théorie (sous les hypothèses du 2nd th.). Si c'était le cas cela contradirait le second th. d'incomplétude (si un énoncé n'est pas démontrable dans T c'est que T est cohérente). Proz (d) 20 septembre 2009 à 23:35 (CEST)

Ce que vous avez fait me convient parfaitement et je vous en remercie. Quant à l'argument... c'était une sorte d'apéritif... Encore merci pour l'ensemble de ce que vous avez déjà fait. Humblement. Gerard (in space...) (d) 20 septembre 2009 à 23:44 (CEST)

smullyan

Il manque "le livre qui rend fou" qui est principalement axé sur les théorèmes de Goedel (voir le problème du coffre).Claudeh5 (d) 21 septembre 2009 à 00:13 (CEST)

La signification du premier théorème d'incomplétude de Godel?

Bonjour, je m’intéresse à la logique mathématique par wikipedia, et même si les articles sont bien ficelés c'est pas évident.

Dans de nombreux articles on parle du théorème d'incomplétude de Godel, et donc en allant sur cette page j'ai du mal à comprendre le sens de:

Dans n'importe quelle théorie récursivement axiomatisable, cohérente et capable de « formaliser l'arithmétique », on peut construire un énoncé arithmétique qui ne peut être ni prouvé ni réfuté dans cette théorie.

Est ce que cela veut dire que dans n'importe quelle théorie récursivement axiomatisable, cohérente et capable de « formaliser l'arithmétique », ( comme par exemple le calcul des prédicats intuitionnistes si je ne me trompe pas!) les règles de déductions ne permettent pas d'obtenir les mêmes conclusions que la théorie de modèle correspondant à cette théorie (comme il est défini ainsi l'incomplétude dans différent article de wikipedia)?

Ou bien est ce que dans cette théorie on peut créer des énonces dont on ne peut prouver qu'il soit faux ou qu'il soit vrai par les règles de déductions?

--Nicobzz (d) 17 décembre 2010 à 23:51 (CET)

Le calcul des prédicats intuitionniste ne permet pas plus que celui classique de "formaliser l'arithmétique" : il faut ajouter des axiomes. Ca ne change pas grand chose du point de vue de l'incomplétude que la logique soit classique ou intuitionniste. La suite en logique classique. Dans le cas des entiers pour une théorie arithmétique il y a un modèle attendu (les entiers de la meta-théorie en gros), et sa théorie (les énoncés "vrais" dans ce modèle) ne peut être capturée par un ensemble d'axiomes fini ou même récursif. Dans le cas d'une théorie récursivement axiomatisable (c.a.d. qu'on arrive à énoncer ses axiomes en gros), le modèle attendu n'est pas "le" modèle de la théorie : elle en a plusieurs. Dire qu'il existe des énoncés que l'on ne peut prouver et dont on ne peut prouver la négation a pour conséquence par le théorème de complétude qu'il existe des modèles de la théorie distincts, certains dans lesquels cet énoncé est satisfait (vrai) et d'autres dans lesquels il ne l'est pas (il y est faux). Un énoncé "relâché" du théorème d'incomplétude dit qu'il existe un énoncé vrai (au sens de vrai dans le modèle attendu, le modèle standard des entiers) non démontrable dans une théorie arithmétique récursivement axiomatisable. Proz (d) 18 décembre 2010 à 14:14 (CET)

Merci bien, je comprend mieux, si je comprend bien donc (même si certainement je suis pas très rigoureux dans mes explications), dans le cas d'une de ces théories récursivement axiomatisable il existe des énoncés que l'on ne peut prouver et dont on ne peut prouver la négation par les règles de déductions(et non pas en passant par un modèle), et qu'il existe un modèle, le modèle standard des entiers, qui permet de dire que certains énoncés sont vrais sans pour autant que ces théories arithmétiques récursivement axiomatisable puissent le démontrer.

Par contre j'ai plus de mal à comprendre votre phrase Dans le cas des entiers pour une théorie arithmétique il y a un modèle attendu (les entiers de la meta-théorie en gros), et sa théorie (les énoncés "vrais" dans ce modèle) ne peut être capturée par un ensemble d'axiomes fini ou même récursif ,(ne vouliez vous pas dire énoncé à la place d' entiers ?) mais je ne connais pas la définition de théorie arithmétique exactement et donc c'est sûrement normal que je ne comprenne pas vraiment ce que vous voulez dire, je retournerai peut être sur cette article si j’acquière encore des connaissances.

en tout cas merci, ça m'avance dans la compréhension de cela, j'espère ça pourra éventuellement vous aider à construire l'article, bien qu'ils soit pas vraiment possible de créer un article pas trop long accessible aux novices car ça demande beaucoup de connaissances.--Nicobzz (d) 18 décembre 2010 à 23:12 (CET)

Ca vient probablement du fait que je ne maîtrise pas parfaitement les termes français de la logique mathématique et donc que j'ai une lecture peu rigoureuse, mais c'est vrai qu'en relisant la phrase :

Dans n'importe quelle théorie récursivement axiomatisable, cohérente et capable de « formaliser l'arithmétique », on peut construire un énoncé arithmétique qui ne peut être ni prouvé ni réfuté dans cette théorie.

je trouve qu'on peut éventuellement la comprendre de deux manières différentes, soit l'énoncé ne peut être ni prouvé ni réfuté par les règles de déductions de cette théorie, soit l'énoncé ne peut être ni prouvé ni réfuté dans le modèle qui pourrait correspondre à cette théorie.(enfin c'est vrai que je maitrise pas tout non plus!)

Peut être si vous pensez de même pourriez vous lever l'ambiguité en le précisant plus bas dans l'article?

--Nicobzz (d) 18 décembre 2010 à 23:35 (CET)

Dans un modèle donné un énoncé est vrai ou faux. Un modèle est une structure, un ensemble muni de lois définies de façon non ambiguë sur cet ensemble. Une théorie est définie par un ensemble d'énoncés (ses axiomes). La vérité d'un énoncé dans un modèle peut se définir mais pas se vérifier par un simple calcul. Le fait qu'une démonstration (formelle) donnée soit correcte (utilise bien les règles) oui (à condition que ce soit dans une théorie récursivement axiomatisable). Proz (d) 18 décembre 2010 à 23:52 (CET)

Merci, ça reste un peu confus pour moi, je vais continuer de me documenter pour comprendre tout cela, bonne journée.--Nicobzz (d) 19 décembre 2010 à 12:29 (CET)

Bonjour, j'ai approfondi mes recherches sur wikipedia anglais et dans un livre, et je comprend mieux actuellement mais si je n'ai pas cherché à comprendre le théorème d'incomplétude de godel, cependant je comprend mieux ce que veulent dire les mots structures et modèles car étant donné que les pages wikipedia françaises de la structure (les pages : Structure (mathématiques) et Structure (logique mathématique) sont peu remplies et parle surtout des aspects historiques de celle ci, j'avais donné une mauvaise interprétation à la définition du mot structure, l'article anglais défini bien rigoureusement ce que ça représente. Peut être j'essayerai dans le futur de traduire une partie de l'article anglais en français, car je pense clairement que celui en français est insuffisant, mais si je le fais je demanderais le soutient d'un auteur de wikipedia connaissant vraiment le sujet pour corriger.--Nicobzz (d) 22 janvier 2011 à 14:02 (CET)

Et oui ... c'est souvent mieux sur en: . L'articleStructure (mathématiques) a l'air d'un petit essai sur le bourbakisme, pas notre sujet. L'article Structure (logique mathématique) (il s'agit bien de celui-là ?) est clairement insuffisant et le résumé introduit plus de confusion qu'autre chose, ne pas hésiter. Un livre introductif en français sur le sujet est René Cori et Daniel Lascar, Logique mathématique I. Calcul propositionnel, algèbres de Boole, calcul des prédicats [détail des éditions]. Si je suis disponible quand tu t'y mets je peux être le soutien. Sinon il y a le Projet:Logique, plutôt en sommeil, mais certaines personnes l'ont en liste de suivi. Proz (d) 22 janvier 2011 à 16:13 (CET)

Indémontrable mais vrai!

Gödel montre l'existence d'énoncés indémontrables (dans un contexte de démontration restreint) mais vrais. Le fait important qu'un tel énoncé soit vrai n'apparaît pas clairement dans l'article. On ne peut donc pas compléter un sytème d'axiomes indifféremment par un tel énoncé ou son contraire.

C'est une question importante, mais il ne faut pas confondre le niveau du théorème (qui affirme, justement, qu'on peut compléter comme on veut) et le niveau "méta", où l'on donne un sens "intuitif" aux axiomes, ce qui, en effet, rend l'un des deux choix plus naturel que l'autre. Le problème, c'est que non-Consis(T) est un énoncé arithmétique d'allure innocente (proche, par exemple, de l'affirmation qu'un certain polynôme s'annule), et que c'est seulement le codage qui montre qu'en fait, cet énoncé affirme "aussi" quelque chose de faux, à savoir que la théorie T (supposée cohérente) démontre que 0=1.--Dfeldmann (d) 26 juin 2011 à 03:56 (CEST)

Théorème d’incomplétude et paradoxe de Richard

Bonjour, en réfléchissant quelque peu il me semble qu'on puisse prouver un théorème d'imcomplétude en utilisant le paradoxe de Richard et la diagonale de Cantor... Savez vous si ce résultat est déjà connu?

Merci --Nicobzz (d) 29 juin 2011 à 15:42 (CEST)

Si on considère que la démonstration de Gödel du théorème d'incomplétude est le paradoxe du menteur + la diagonale, il est peut-être possible d'y aboutir en employant un autre paradoxe.. Cela ne me parait pas impossible. Si c'est le cas, ce serait intéressant à mentionner dans l'article. --Jean-Christophe BENOIST (d) 29 juin 2011 à 16:23 (CEST)

Certes... à condition que ce soit déjà écrit quelque part (ou bien connu des spécialistes) Sinon, on frôle le TI, là--Dfeldmann (d) 29 juin 2011 à 18:58 (CEST)

Accord avec Dfeldmann. Surtout qu'il faudrait être précis : Gödel cite le paradoxe de Richard dans son article (pour l'énumération des formules) et le paradoxe de Richard utilise un procédé diagonal ... Proz (d) 29 juin 2011 à 19:24 (CEST)

Quand je disais "si c'est le cas", je voulais dire "s'il y a des sources" bien sûr. Vous me connaissez --Jean-Christophe BENOIST (d) 29 juin 2011 à 20:55 (CEST)

Ah oui il me semblait bien, à moins que j'ai fait une erreur de raisonnement, ça veut dire quoi TI?--Nicobzz (d) 29 juin 2011 à 22:36 (CEST)

WP:TI. Ce qui ne doit pas exister dans WP. Cordialement --Jean-Christophe BENOIST (d) 30 juin 2011 à 00:08 (CEST)

Merci--Nicobzz (d) 30 juin 2011 à 07:38 (CEST)

article pas très bien écrit

Bonjour, on voit bien que plein de personnes intelligentes ont apporté une touche de compréhension à l'article général, mais du coup ça donne vraiment un patchwork étrange, où le français même simple, n'est pas toujours compréhensible: "L'existence de théories incomplètes est banale. Beaucoup de théories, comme la théorie des groupes, des anneaux, des corps, ne sont pas complètes : par exemple on peut dire au premier ordre qu'un groupe ou un corps a 2 éléments, ou 3 éléments. C'est différent pour l'arithmétique, on aurait souhaité capturer par une axiomatique toutes les propriétés des entiers naturels" 1) je ne vois pas bien ce qui est montré (sans être démontré ;) ) dans l'exemple de la théorie des groupes, on peut dire à sa guise qu'un corps a 2 ou 3 éléments sans que ça change quoi que ce soit? Est-ce vraiment un exemple du théorème d'incomplétude, ou juste une absence de précision dans les termes employés? Donc forcément le passage sur l'arithmétique n'est pas non plus clair, il n'y a pourtant que deux phrases, mais on se demande "différent de quoi?", la dernière partie de la phrase laisse à penser que le théorème de godel dit que les objets mathématiques sont forcément décrits de manière complètes par des théories distinctes, je ne crois pas que ce soit exactement le propos, ou alors c'est une très grosse extrapolation non? Klinfran (d) 24 janvier 2012 à 18:46 (CET)

Un groupe possède 2 élements est un énoncé que la théorie des groupes ne décide pas, celle-ci est donc incomplète (ce n'est pas un théorème, juste une évidence). Je ne comprends pas le second commentaire. Proz (d) 24 janvier 2012 à 20:01 (CET)

Discussion trop longue

J'aurais voulu mettre un point sur un énoncé qui me semble faux quelque part, mais je ne sais pas si ce point a été relevé. Serait-il possible de contacter les différents acteurs de cette discussion pour la nettoyer un peu (certains points ont été réglés depuis) ?

Le point qui me chagrine est sur la partie quantification existentielle (Vérité dans le modèle standard) qui énonce qu'il n'est pas évident de résoudre "∃ x, P(x)=Q(x)" sur les enties avec les polynômes à une variable, et rajoute (et pour moi c'est faux) que c'est impossible en vertu du 10ème problème de Hilbert. Or trouver les racines entières du polynôme P-Q est tout à fait possible. Le 10ème problème de Hilbert n'a de problème qu'avec plus de deux variables. Idem pour la quantification universelle: ∀ x P(x)=Q(x) <=> P-Q = 0 et c'est trivial. Sedrikov (d)

C'est juste, et à corriger, il faut des paramètres (je suis responsable de l'erreur). On peut archiver la discussion précédente. Proz (d) 16 avril 2012 à 17:39 (CEST)

Preuve / Démonstration (anglicisme)

Bonjour,

Le mot "preuve" est utilisé un peu partout dans l'article et il s'agit d'un anglicisme. En français l'on parle de démonstration.

Calvus mons (d) 8 juillet 2012 à 20:25 (CEST)

On parle aussi de preuve, du moins dans ce domaine (exemples facilement accessibles sur le web, par ex. la locution "preuve formelle") ; possible que ce soit sous l'influence de l'anglais, de là à parler d'anglicisme ... d'ailleurs ce n'est pas forcément la seule raison. Proz (d) 9 juillet 2012 à 01:33 (CEST)

En anglais la "preuve" est une "evidence" et un 'indice' est "clue". "prouve" étant un verbe demandant d'apporter des "evidences" --Ppignol (discuter) 28 août 2020 à 08:21 (CEST)

Je suis d'accord, mais la bataille est sans espoir. --Pierre de Lyon (discuter) 1 septembre 2020 à 22:18 (CEST)

Formulation

La formulation de l'introduction a été changée.

Avant il était écrit « la cohérence de la théorie [est] le fait qu'elle ne permette pas de démontrer tout, et donc n'importe quoi  ».

Maintenant il est écrit « la cohérence de la théorie [est]  le fait qu'elle ne contienne pas de contradiction, ce qui permettrait de démontrer tout et n'importe quoi  ».

Ce changement n'est pas anodin. Quelle est la formulation qui vous parait la meilleure? --Pierre de Lyon (discuter) 29 août 2013 à 12:25 (CEST)

Je préfère définir intuitivement la cohérence comme le fait de ne pas tout démontrer, ça me semble l'idée essentielle. Proz (discuter) 29 août 2013 à 17:47 (CEST)

Il existe une proposition vraie non démontrable

La proposition G=Δ(⌈Δ⌉) est à la fois vraie et non démontrable. Pourquoi dit-on qu'affirmer qu'il existe un formule vraie et non démontrable nécessite des hypothèses plus fortes? Excusez-moi si je reviens sur un sujet déjà débattu, mais ça me travaille. Relisant la réponse de Proz du 6 mai 2009, je ne la comprends pas. --Pierre de Lyon (discuter) 29 août 2013 à 12:25 (CEST)

Cette proposition se démontre bien sous hypothèses tout à fait minimales : théorie cohérente récursivement axiomatisable et qui a pour conséquence toutes les formules Si^0_1 vraies dans N (donc ne démontre que des Pi^0_1 vraies par cohérence). Mais l'énoncé du paragraphe en question a pour hypothèse (en plus des deux premières) que les axiomes et donc toutes les conséquences de la théorie (sans restriction sur leur complexité logique) sont vrais dans N. C'st une forme du théorème d'incomplétude plus facile à démontrer et que l'on trouve dans les résumés de vulgarisation, dans les cours introductifs de logique, en introduction au théorème, par ex. dans le livre de Smullyan si je me souviens bien. Si ça n'est pas clair, je suppose qu'il faut le dire autrement, mais sans parler de Si^0_1 et Pi^0_1 que tu connais mais pas le lecteur en général. Proz (discuter) 29 août 2013 à 17:45 (CEST)

Lequel est un corollaire de l'autre ?

Il me semblait évident que le 1^er est un corollaire du 2^e, or je lis l'inverse (à 2 reprises) dans le « résumé » introductif et au début du § Énoncés des deux théorèmes. Anne (discuter), 2/5/14 à 08h36

P. S. : le « résumé » introductif est trop long. Suggestion : en délester une partie dans une 1^re section intitulée « histoire » ou « contexte » ou ...

On utilise bien le 1er pour démontrer le second (et de plus une formalisation de la preuve du 1er, la non démontrabilité), de là à parler de corollaire (il y a du travail) ... Le 1er peut être vu comme une conséquence du second si on énonce le 1er comme "il existe un énoncé vrai non démontrable" (c'est de plus en fait cet énoncé que l'on utilise pour le second), celui-ci étant la cohérence que l'on suppose vraie par hypothèse ("vrai" signifie vrai dans le modèle standard des entiers, les entiers de la meta-théorie), et si on met des hypothèses suffisantes pour démontrer le second (hypothèses qui pourraient être affaiblies, ce n'est pas traité dans l'article). Maintenant le th. de Gödel-Rosser (c'est souvent ce qu'on appelle th. de Gödel) et le second th. ne sont pas vraiment comparables. Une "erreur" courante (dans les articles de vulgarisation) est de dire dans la conclusion du 2nd que la cohérence est indécidable, ce qui est en fait contredit par le 2nd th. lui même. Ou alors on imagine une hypothèse restrictive sans intérêt (la non démontrabilité deviendrait essentiellement tautologique), qui n'est pas utile pour la preuve, et pas dans les énoncés sérieux de toute façon.

Pour le PS. l'article n'est pas aux normes de forme actuelles, bien que je crois correct et utile. Je suis d'accord que c'est regarder à l'occasion (des sources seraient utiles en particulier pour la partie historique, même si le peu qui est dit est assez standard, l'édition du ou des volumes concernés des "complete works" par ex.). Proz (discuter) 2 mai 2014 à 11:34 (CEST)

Merci d'avoir pris la peine de me répondre mais tu me surestimes : ça me passe largement au-dessus de la tête et j'ai décroché à partir de « et si on met des hypothèses suffisantes pour démontrer le second ». Tant pis, ta réponse sera peut-être utile à d'autres, ou à moi quand j'aurai le courage de faire les efforts nécessaires. Mon idée pour 2 ⇒ 1 était : 2 dit que T ⊬ coh_T, donc il reste à montrer que T ⊬ ¬coh_T c'est-à-dire T ⊬ Dem_T(⌈⊥⌉), or cela résulte de T ⊬ ⊥ car (c'est sans doute là qu'est mon erreur naïve ?) si on avait une démonstration de ⊥ à partir de T, on pourrait, en la codant, en déduire une démonstration de Dem_T(⌈⊥⌉) à partir de T. Anne (discuter) 3 mai 2014 à 10:53 (CEST)

Ce que tu dis est juste, pas besoin de codage, simplement parce que si on a une démonstration de ⊥, on a une démonstration de n'importe quel énoncé (c'est une règle logique, mais si la règle n'existait pas c'est que ⊥ n'aurait pas de propriétés particulières et pourrait être remplacé par n'importe quoi donc ça marcherait aussi d'une autre façon). Mais on ne peut pas en déduire ce que tu penses. Le 2nd théorème d'incomplétude a pour conséquence justement qu'une théorie cohérente a une extension T qui vérifie T ⊬ ⊥ (cohérence) et T ⊢ Dem_T(⌈⊥⌉) (voir Théorème_d'incomplétude#Conséquences_immédiates_du_premier_théorème_d'incomplétude). Mais la démonstration en question ⊥ de est (codée par) un entier non standard, puisque T ⊬ ⊥. Tu ne peux pas espérer démontrer le théorème de Gödel-Rosser (c'est-à-dire le 1er théorème de Gödel sans hypothèse supplémentaire ad hoc pour la non démontrabilité de la négation de la proposition G, celle qui est "fausse") à partir du second théorème d'incomplétude, il faudrait en gros changer l'énoncé, voir en:Rosser's trick, et ce n'est plus la cohérence. Proz (discuter) 3 mai 2014 à 12:17 (CEST)

Je me suis emmêlé les pinceaux et je voulais dire, comme tu l'as deviné : « si on avait une démonstration de Dem_T(⌈⊥⌉) à partir de T, on pourrait, en la décodant, en déduire une démonstration de ⊥ à partir de T », et tu m'expliques bien mon erreur, merci encore. Anne (discuter) 3 mai 2014 à 12:39 (CEST)

Diagonalisation : une preuve à revoir.

La formule G vérifie, par construction, la propriété suivante :
(1) G est vraie dans N si et seulement si G est improuvable dans T
Puis on montre que G n'est pas prouvable.
Supposons G prouvable.
D'après (1), G est fausse dans N, donc (non G), étant une Σ₁ formule vraie dans N, est prouvable dans T. Ce qui contredit le fait que T est une théorie cohérente.
Donc G est improuvable
Ainsi G est une formule vraie dans N et improuvable dans T
Supposons (non G) prouvable.
Puisque N est modèle de T, il est modèle de ses conséquences logiques, donc de (non G).
Par suite (non G) est vraie dans N, donc, d'après (1), G est prouvable, ce qui contredit la cohérence de T
Donc (non G) n'est pas non plus prouvable.
--Liviusbarbatus (discuter) 1 février 2015 à 19:05 (CET)

(petite correction, vous aviez écrit une chose pour une autre), votre démonstration utilise que N est modèle de T, alors que, sans rien y changer, il suffit d'avoir l'hypothèse beaucoup plus faible que N est modèle des conséquences Pi_1 de T, hypothèse qui est elle-même une conséquence de l'hypothèse d'omega-cohérence que faisait Gödel (la partie importante du théorème est que G est vraie mais non prouvable de toute façon). Ca me paraît alors être en gros la démonstration de la section diagonalisation. Proz (discuter) 2 février 2015 à 17:00 (CET)

Les formules Pi_1 sont (à équivalence près) les négations de formules Sigma_1 (voir hiérarchie arithmétique). En l'occurrence pour faire votre démonstration (seconde partie), il suffit de supposer que les formules Pi_1 (comme non G) prouvables dans T sont vraies dans N (la preuve devient un peu tautologique, mais cette partie de la preuve est tautologique). C'est une conséquence de l'hypothèse que faisait Gödel (en:ω-consistent theory). Ces hypothèses sont beaucoup plus faibles que N est modèle de T. Proz (discuter) 2 février 2015 à 23:20 (CET)

Quelle est la définition formelle du mot "vrai", tel qu'il est utilisé ici ?

Bonjour, je remarque l'utilisation du mot « vrai » dans cet article,

• la première occurence étant Par exemple, Gödel construit effectivement un énoncé dont on montre qu'il est vrai dans N, ce que l'on peut interpréter par « on sait le prouver dans une théorie plus forte que celle de départ ».
• Que signifie ce mot « vrai » ? Plus précisément,
  • où est-il définit ?
  • et dans quelle théorie ayant quel langage ?
• Est-ce un synonyme du mot "valide" (avec la nuance, dans un modèle, dans tout modèle) ?
  • Si oui, pourquoi ne pas employer ce mot formellement défini de "valide" à la place de ce mot opaque de "vrai" ?
  • Si non, quelle est donc la signification, dans ce contexte tout à fait formel ( ma question ne porte pas sur les moult usages informels de ce mot) de ce mot "vrai"  ?

--Epsilon0 ε₀ 5 février 2015 à 21:58 (CET) qui ne joue pas au naïf, car sur ce point il ne comprend réellement pas. Pour préciser, je ne connais aucun texte de logique utilisant le mot "vrai" qui ne soit aisément transformable par un texte, plus formel, l'éliminant. Mais concernant ces thms d'incomplétude, dans quasi toute la littérature, ce mot "vrai" perdure. Bon, pourquoi pas, mais qu'elle est donc sa définition formelle ? A noter que cette remarque ne conteste rien de ce que disent ces thms que je sais parfaitement énoncer sans jamais user du mot "vrai" ; mot qui me semble ainsi inutile et source de confusion. --Epsilon0 ε₀ 5 février 2015 à 22:14 (CET)

Je me demande bien pourquoi valide serait moins opaque que vrai et plus formellement défini ? "Une formule est vraie dans un modèle" signifie que ce modèle satisfait la formule, je pense que personne n'emploie en logique ce mot dans un autre sens. Là il s'agit du modèle standard des entiers, c'est-à-dire des entiers du meta-langage, donc on dit souvent vrai tout court, parce que satisfait par le modèle standard ça correspond à ce que signifie vrai en math. et que donc c'est assez éclairant pour les non spécialistes je pense (et je ne suis pas le seul selon ce que tu dis toi même). Il y a de toute façon quelque chose d'irréductible (standard, vrai ... tu pourras toujours agiter le mot formel ...) que tu n'élimineras pas en changeant de vocabulaire. Par ailleurs ce vocabulaire est introduit dans l'article me semble-t-il tout à fait ouvertement (les titres de sections paraissent explicites), il n'est pas utilisé avant ces sections (au début les choses sont dites du seul point de vue de la démontrabilité). Tu y trouveras les réponses aux questions que tu poses (je ne vais pas quand même les recopier en pdd). Proz (discuter) 5 février 2015 à 23:37 (CET)

Je pense qu'Epsilon0 ε0 soulève un "vrai" problème. Toute la difficulté d'explication du théorème de Gödel à l'homme de la rue porte sur la compréhension de ce que "vrai" signifie. Quand je lis « la notion de vérité, [est] parfois méconnue en dehors de la logique mathématique ». Je tousse. Voici mon point de vue (que je ne veux pas imposer):

• la « vérité » est une notion philosophique et/ou intuitive,
• la « validité » est une notion logique,
• la « démontrabilité » est une notion logique.

--Pierre de Lyon (discuter) 13 février 2015 à 16:23 (CET)

Heu, je me permet de protester courtoisement. Dans le contexte (Gödel), il existe une notion d'entier (une méta-notion, si on veut) déjà connue, celle permettant de parler d'entier (de Gödel) associé à un terme, à un énoncé, à une démonstration, etc;) et ces entiers-là sont les entiers standard pour toute théorie (mettons ZFC) dans laquelle on veut formaliser la démonstration. A ce sens, l'énoncé A=(Pour tout n, P(n)) est vrai signifie que P(1), P(2), etc. est vrai (ou valide,ou démontrable, etc.) de manière explicite (par exemple on a une démonstration explicite de P(k) pour tout k, alors qu'on n'a pas forcément de démonstration de A ; et, d'autre part, on ne dispose pas d'une notion analogue de vérité pour les énoncés de ZFC, parce qu'on ne dispose pas d'une liste intuitivement exhaustive de tous les ensembles (V=L étant ce qui s'en rapproche le plus, mais on sait bien que c'est très loin de faire l'unanimité). Bref, pour les entiers (et plus généralement pour les ensembles explicitement dénombrables, par exemple pour les ordinaux constructibles), on a une notion de vérité (=vrai dans le modèle standard) qui, elle, fait à peu près l'unanimité...--Dfeldmann (discuter) 13 février 2015 à 18:03 (CET)

Question magnifique ! Il faut absolument que l'article y réponde sinon il manque sa cible.

C'est une conséquence qui fut explicitée par Tarski des deux théorèmes d'incomplétudes: la vérité n'est pas définissable mathématiquement. On arrive à faire des approximations en définissant des notions relatives comme « être valide dans un modèle », qui est une définition de la vérité tout à fait tautologique puisque essentiellement de la forme « une formule A est valide dans un modèle M si toute interprétation de A dans M prend la valeur booléenne vraie », schématiquement: « A est vraie dans M si l'interprétation de A est vraie dans M ». On a défini la notion importante d'interprétation des formules dans les modèles qui fonde la théorie des modèles, mais pour ce qui est de définir la vérité on sent que l'on n'a pas beaucoup avancé. Bref point n'est possible de définir la vérité de manière absolue par des moyens mathématiques ; comme Pierre le relève ci-dessus la vérité est d'une autre nature. Ce qui n'empêche pas d'utiliser le concept : si je dis que 0 = 1 est faux j'espère que personne ne me contredira, même si je suis bien incapable de le prouver (je peux bien montrer qu'alors je suis le pape mais ça ne résoud rien, on va me demander de démontrer que je ne suis pas le pape...).

Donc pour répondre à Epsilon0, l'article ne définit pas la vérité parceque c'est impossible (mathématiquement, s'entend). Du reste les deux énoncés des théorèmes n'emploient pas le concept et je crois que l'article original de Gödel prenait grand soin de n'y faire aucune référence non plus, il n'y était question que de prouvabilité. Par contre c'est vrai (tiens j'ai dit vrai) que les discussions en abusent, parceque bon, c'est quand même un concept utile s'pas ? Il serait peut-être bien d'ajouter une petit paragraphe pour expliquer ce que l'on entend par « tel ou tel énoncé est vrai » (vous ferai peut-être une proposition si je trouve le temps). --Laurent de Marseille (discuter) 20 juin 2015 à 11:11 (CEST)

Ca peut être une bonne idée de reprendre des choses à ce sujet sur cet article. L'introduction du paragraphe "Vérité et démontrabilité" est probablement trop naïve. On ne peut pas échapper à la notion de "vérité", qui est indispensable à la compréhension du théorème. Maintenant je doute que l'objectif essentiel de l'article soit de répondre à la question en tête de section. Quelques précisions ou remarques complémentaires :

* Les deux énoncés font référence à la notion de "cohérence" donc implicitement à une notion de vérité (la cohérence c'est affirmer qu'un certain énoncé Pi^0_1 est vrai), les énoncés modernes, y compris vulgarisés (Ian Stewart par exemple) sont souvent donnés en terme de vérité, et en réalité il suffit de parler de vérité des formules Pi^0_1, donc c'est tout à fait arithmétique (le théorème de Tarski n'entre pas en jeu), et quand on dit que l'énoncé de Gödel est vrai ça n'est pas plus mystérieux que de dire que la théorie est cohérente ;

* pour des raisons historiques Gödel (qui a d'ailleurs déclaré plus tard avoir tout d'abord découvert le théorème sur la non définissabilité de la vérité) ne parle pas de vérité, mais de omega-cohérence ce qui est (un peu) plus compliqué que la vérité des formules Pi^0_1 ;

* le théorème de Tarski n'est pas une conséquence des théorèmes d'incomplétude, même si la démonstration est analogue (en plus simple) ;

* La notion utile c'est vrai au sens de satisfait "dans le modèle standard" (de l'arithmétique), on n'a pas donné de définition absolue de la vérité, puisque "standard" n'est pas défini et ne peut l'être pour les raisons que donne Laurent, on sait peut-être juste un peu mieux de quoi on parle, puisque c'est finalement l'usage mathématique que les mathématiciens soient d'accord sur ce que sont les entiers, là c'est juste déstabilisant parce que le théorème porte justement sur les théories arithmétiques, et qu'il y a une illusion, parfois entretenu par un discours ultra-formaliste sans grande substance, qui est qu'il suffirait de parler de "démontrable" et que l'on peut se passer de la notion de "vrai", mais finalement le mot "vrai" est pris au sens usuel en math ;

* la démonstration du 1er théorème pourrait d'ailleurs se faire en prenant un modèle de l'arithmétique non standard, ça conduit en gros à une preuve du second (cf. la preuve dans le livre de théorie des ensembles de Krivine), mais au départ on a un modèle "standard", finalement on comprend que c'est le fait d'être (implicitement) d'accord sur un modèle dit standard qui est utile (il n'y a aucune obligation à adhérer à une position philosophique analogue à celle de Gödel sur la réalité des objets mathématiques, même si cette position a sa cohérence). Proz (discuter) 20 juin 2015 à 13:23 (CEST)

* « pour des raisons historiques Gödel [...] ne parle pas de vérité, mais de omega-cohérence » : je crois que c'est pour des raisons techniques, Gödel produit une formule G qui n'est pas démontrable dans la théorie T considérée mais qui l'est dans le système ambiant (celui dans lequel on démontre le théorème d'incomplétude, l'arithmétique en l'occurrence). On sait donc prouver G, donc que non G n'est pas démontrable... en arithmétique (si celle-ci est consistante) ; pour pouvoir en déduire que non G n'est pas démontrable dans T, compte-tenu du fait que non G est Sigma il faut l'hypothèse de omega-consistance sur T. Cette restriction a été levée par Rosser qui, en construisant une formule R plus complexe, montre sans hypothèse sur T que ni R, ni non R ne sont démontrables.

* « le théorème de Tarski n'est pas une conséquence des théorèmes d'incomplétude » : oui c'est vrai, j'ai été un peu rapide.

* « La notion utile c'est vrai au sens de satisfait "dans le modèle standard" » : alors là je ne suis pas du tout d'accord. Le point de départ de cette discussion est la question d'Epsilon0 qui pointe à très juste titre le fait que l'usage du concept de vérité dans cette article est source de confusion, justement parceque les théorèmes d'incomplétudes traitent du rapport entre vérité et prouvabilité. Je ne dis pas qu'il ne faut pas utiliser le concept fondamental de vérité, mais il faut être précis. Pour moi « vrai dans le modèle standard » est juste une manière commode de dire « prouvable en arithmétique ». Par exemple on dit que la formule de Gödel est vraie dans le modèle standard au lieu de dire qu'on l'a démontrée dans l'arithmétique. C'est commode et incorrect, car comme vous le savez tout ce qui est vrai dans le modèle standard n'est pas forcément prouvable dans l'arithmétique. Du reste Gödel n'utilise absolument pas cette notion dans son article. --Laurent de Marseille (discuter) 21 juin 2015 à 11:10 (CEST)

Pour ta première objection je pense qu'il y un malentendu. Un énoncé "moderne" du théorème que démontre Gödel (pas Rosser qui démontre autre chose, dont en particulier on ne déduit pas le second théorème), c'est qu'il existe une formule Pi^0_1 vraie non démontrable, Gödel ne donne pas cet énoncé, mais ce n'est pas pour des raisons techniques (il est possible d'ailleurs qu'il l'ait pensé plus ou moins comme ça, il faudrait voir les Collected works, vol I ou correspondance). De plus les choses sont plus claires aujourd'hui parce qu'il y a eu depuis un certain nombre d'avancées (dont les définitions de la satisfaction par Tarski), et que des gens ont travaillé sur sujet, Robinson a vraiment "décortiqué" le théorème (cf. Le livre de Smorynski). L'hypothèse d'omega-cohérence permet de démontrer que les formules Sigma démontrables sont vraies dans le modèle standard, et on pourrait tout aussi bien donner cette hypothèse, cette partie de la démonstration est quasi-tautologique. Par ailleurs l'hypothèse de omega-cohérence parle bien tout à fait clairement des entiers standards (même si le mot "standard" n'apparaît pas dans l'article de Gödel).

Pour la seconde, je ne vois pas où tu veux en venir, ni en quoi ce que tu écris est vraiment une objection. Certes ultimement on fait des démonstrations dans un système ambiant (c'est en gros dit dans l'article il me semble), mais justement on n'a pas besoin de préciser celui-ci, ce qui limiterait alors la portée du théorème (au passage je ne pense pas que tu aies à invoquer la cohérence du meta-système dans ton résumé de démonstration, mais seulement celle du système cible, pour la non démontrabilité de non G dans le système cible, bien sûr la cohérence du meta-système est utile pour que tout cela ait un sens). On ne définit pas plus "le modèle standard" dans l'absolu, qu'on ne définit "la vérité", c'est du même ordre, mais ça éclaire les choses, quand il s'agit comme ici d'énoncés arithmétiques et même Pi^0_1 (cohérence, énoncé de Gödel), et quand on parle de vérité pour les théorèmes d'incomplétude 1/ c'est bien pour ce genre de formules, 2/ c'est bien dans N. Le mieux serait de pointer précisément les sources de confusion dans l'article. Proz (discuter) 22 juin 2015 à 01:48 (CEST)

Ou encore mieux : identifier des sources qui présentent les choses de la manière voulue, et dire "je voudrais voir les choses présentées dans cet article comme dans telle source". A un moment donné, il faut se raccrocher aux sources (ne serait-ce que pour essayer de comprendre les propos, qui ne sont pas toujours clairs en discussion, en se reportant à la source), et bien sûr pour se conformer aux exigences de vérifiabilité de Wikipédia. Sinon, la discussion peut tourner en "débat d'expert", à l'issue incertaine, tout autant que la validité des analyses et opinions qui y sont données. --Jean-Christophe BENOIST (discuter) 22 juin 2015 à 11:29 (CEST)

Pour Jean-Christophe : l'idée de revenir aux sources est intéressantes mais en l'occurrence j'ai peur que ça ne nous aide pas beaucoup : je vais avancer Proof theory and logical complexity de Girard, je pense que Proz va me répondre par Logique mathématique de Lascar-Cori et le débat continuera. D'autre part je n'ai rien a priori contre les débats d'experts, il me semble que les pages de discussion sont précisément faites pour ça.

Bien sûr je ne confonds pas débat d'expert et dialogue de sourds, personnellement ce débat m'intéresse car il résonne avec des questions que je me pose, mais mon but, comme celui des autres participants je pense n'est pas d'avoir le dernier mot mais d'aller vers une amélioration de l'article.

Et parlant de débat, il m'arrive de me voir reprocher d'adopter un ton parfois péremptoire ; si c'est le cas ici je vous prie de m'en excuser, c'est absolument non voulu d'autant plus que je ne suis souvent qu'à moitié convaincu par mes propres arguments. Mais il s'agit de discussion s'pas ? on essaye d'avancer.

Revenons à notre débat d'experts.

Pour répondre à Proz : je n'ai pas compris où il y a malentendu, il me semble que sur la omega-consistance nous disons la même chose, même si tu es plus précis. Quant à : « On ne définit pas plus "le modèle standard" dans l'absolu, qu'on ne définit "la vérité", c'est du même ordre » : je suis tout à fait d'accord, cette question de ce que l'on entend par modèle standard m'a longtemps turlupiné ; « mais ça éclaire les choses » : je ne suis plus d'accord, il me semble que la question d'Epsilon0 qui résonne avec celles que je me suis longtemps posé aussi montre justement que ça n'éclaire pas. Cela étant je ne ferai pas de guerre de religion sur ce point, je suis prêt à croire que ça peut être éclairant pour certains et moins pour d'autres (mais j'aimerais bien avoir l'avis d'Epsilon0 là-dessus).

On fait quoi avec tout ça ? Ma proposition serait, dans les parties techniques de limiter au maximum l'emploi du concept de vérité, ce qui n'implique pas grand chose comme changement je crois, et d'expliquer la chose les parties non techniques, ce que j'ai d'ailleurs commencé à faire avec le premier paragraphe de la section Tour d'horizon. Il me semble que le présent débat nous donne des éléments pour ça. -Laurent de Marseille (discuter) 23 juin 2015 à 00:45 (CEST)

Oui, je ne pense pas que l'on avance sans débat, y compris pour la façon rédiger. A Laurent : je ne répondrais vraiment pas du tout Lascar-Cori (il y a vraiment un malentendu, ou alors tu as oublié leur présentation du théorème). Je suis bien au contraire tout à fait d'accord sur Proof theory and logical complexity, il se trouve, je crois, que c'est le premier texte (le premier chapitre "The Fall of Hilbert program") vraiment explicatif et compréhensible que j'ai pu lire (il y a longtemps) sur le sujet (et il donne par ailleurs les liens entre cohérence et vérité de certaines classes de formules, parle de démontrabilité des Sigma_1 vraies et pas de omega-cohérence ...). Sinon les articles ou livres de Smorynski (Handbook et livre cité) sont très bien. Le livre de Franzen, assez vulgarisé, qui est cité sur la version en: et que j'avais feuilleté il y a longtemps m'avait semblé tout à fait intéressant sur des choses moins techniques. Le livre de Smullyan, plutôt vulgarisé lui aussi, est très délayé, et s'étend énormément sur des questions de codage, mais explique aussi bien certaines choses dans mon souvenir (je ne l'ai pas ouvert depuis très longtemps). Et le chapitre 9 du livre de théorie des ensembles Krivine est très éclairant pour le second théorème.

Si je comprends mieux, le débat ce serait parler de "vrai" tout court, comme le fait par exemple Girard, sans préciser sans arrêt modèle standard, comme je l'ai fait non par conviction, mais craignant des interrogations "meta-physiques" au sujet de "vrai" ? Pourquoi pas ? Si je comprends bien tu penses que de préciser les choses en terme d'interprétation dans un modèle trouble plutôt que d'éclairer. Pour aller dans ton sens, on peut se dire que le mot vrai est finalement utilisé au sens usuel en math. Je te précise ce qui me semble éclairant au moins pour certains : la vérité des énoncés Sigma_^0_1 et Pi^0_1 est la chose centrale (au sens du récapitulatif de Girard p 63, 1.3.19), et le fait que vérifier un énoncé Pi^0_1, ce soit vérifier pour chaque entier un énoncé élémentaire (comme le donne la définition de la satisfaisabilité), chaque vérification de cet énoncé élémentaire elle même étant "élémentaire" et "non discutable", est très utile pour comprendre. Le mot "standard" indique juste qu'il s'agit des entiers de la meta-théorie. Mais cela peut être écrit une fois pour toute, et ensuite on utilise uniquement "vrai", pourquoi pas ?

Les précisions sur la cohérence de ton ajout sur le premier paragraphe manquaient, mais remarque bien que cela amène à parler plus tôt de vérité qu'avant. C'était tout à fait volontairement que la première partie (jusqu'au paragraphe vérité et démontrabilité) était écrite en terme uniquement de prouvabilité, parce que ça reste source de malentendu de parler de vérité. Mais c'était peut être une gageure de vouloir l'éviter au début de l'exposé, sinon on pourrait incorporer ton ajout au paragraphe "vérité et démontrabilité" (en allégeant l'existant) ? Proz (discuter) 23 juin 2015 à 18:41 (CEST)

En ce qui me concerne je suis très content de cette discussion, j'ai les idées plus claires sur comment améliorer l'article, maintenant y a plus qu'à...

Désolé Proz mais je ne vois toujours pas où est le malentendu, au contraire j'ai l'impression que nous convergeons.

J'ai remis la main sur mon Proof theory et effectivement j'ai pu constater que Girard use (et abuse) du mot « vrai », par exemple son énoncé du 1er théorème est qu'il existe une formule vraie et non démontrable.

« Si je comprends bien tu penses que de préciser les choses en terme d'interprétation dans un modèle trouble plutôt que d'éclairer. » : oui c'est à peu près ça, du moins ça m'a souvent troublé et la question d'Epsilon0 me donne à penser que je ne suis pas le seul.

« le débat ce serait parler de "vrai" tout court » : pas vraiment, mon idée originale était d'éviter, au moins dans les parties techniques, l'emploi du concept de vérité parceque celui-ci n'est pas définissable, mais maintenant je me dis que l'on peut s'en sortir en explicitant ce que l'on entend par « formule vraie » et je pense que la bonne définition serait alors « prouvable dans l'arithmétique ». C'est typiquement le cas de la formule de Gödel, elle est vraie parceque prouvable (et même prouvée) dans l'arithmétique.

« Les précisions sur la cohérence de ton ajout sur le premier paragraphe manquaient, mais remarque bien que cela amène à parler plus tôt de vérité qu'avant. » C'est tout le problème, malgré tout les théorèmes d'incomplétude parlent, même si c'est en creux, de vérité. Cela étant je vais déplacer ce paragraphe dans la section Vérité et démontrabilité, ça sera plus cohérent avec ce qui suit, tu as raison. Je vais aussi ajouter un paragraphe au résumé introductif, qui est devenu trop court, je crois qu'il faut dire un mot sur le programme de Hilbert. --Laurent de Marseille (discuter) 24 juin 2015 à 22:34 (CEST)

Introduction trop longue, vérité et prouvabilité

Je reviens sur le post-scriptum de Anne avec laquelle je suis entièrement d'accord : l'introduction est trop longue. À mon avis seuls les deux premiers paragraphes font l'introduction, le reste devrait être bougé ailleurs, probablement à la fin de la section Vérité et démontrabilité.

D'autre part la question de Epsilon0 me donne à penser qu'il manque une discussion sur vérité et prouvabilité dans l'article que l'on pourrait ajouter en début de la section Vérité et démontrabilité. --Laurent de Marseille (discuter) 20 juin 2015 à 11:35 (CEST)

plutôt que d'une introduction (c'est vrai que ça ressemble à une introduction), il devrait s'agir d'un résumé introductif (en gros quelque chose qui peut se lire de façon autonome et qui est justifié par le contenu de l'article. Actuellement, c'est peut-être trop détaillé sur la partie historique, d'autant qu'une partie de l'article a migré dans programme de Hilbert, ce qui fait que ça ne résume pas l'article. Mais il y a un équilibre à trouver, qui demande d'intervenir sur le résumé et sur l'article. Proz (discuter) 20 juin 2015 à 13:29 (CEST)

J'ai trouvé une solution qui me semble simple et élégante : rétablir la section Introduction ; sauf que wp déconseille les sections « Introduction », j'ai donc intitulé celle-ci « Tour d'horizon », titre que j'ai été pêcher dans l'article fraction continue. J'ai un peu repris le résumé introductif aussi et surtout j'ai ajouté en début du Tour d'horizon un paragraphe sur vérité et prouvabilité qui j'espère répond un peu à la question d'Epsilon0, je suis curieux d'avoir votre avis. --Laurent de Marseille (discuter) 21 juin 2015 à 14:06 (CEST)

J'ai commencé à réorganiser un peu, déplacé la section Tour d'horizon et renommé ycelle en Accueil des théorèmes par les mathématiciens un titre un peu lourd mais je ne trouve pas mieux. Je ne suis pas certain que le résultat de ces modifs soit très heureux. -Laurent de Marseille (discuter) 24 juin 2015 à 23:24 (CEST)

Continué à travailler sur l'article. Je suis un peu gêné car j'y suis allé avec mes gros sabots et ait repris beaucoup de travail d'autres, notamment de Proz. Je crois avoir conservé l'esprit et la structure générale mais en apportant des précisions ou des éclaircissements. J'espère avoir fait évolué les choses dans un sens positif (j'aimerais bien une confirmation d'Epsilon0 dont la question ci-dessus est ma motivation basique) et aussi que vous n'hésiterez pas à me dire si je me suis planté.

Parmi les modifications que j'envisage encore : déplacer la section « Une preuve partielle... » juste après la section « Vérité et démontrabilité ». Qu'en disez vous ? --Laurent de Marseille (discuter) 28 juin 2015 à 15:23 (CEST)

L'ensemble de la section ? Pas pour du tout, d'une part c'est bien que la première partie de l'article ne rentre pas dans des détails techniques, d'autre part ça n'est plus cohérent.

Par ailleurs je pense que c'est un aspect (ne pas rentrer dans les détails dans les premières sections) dont tu ne prends pas assez compte dans tes modifications, tu as amélioré la structure, il y a des choses qui manquaient comme mentionner le fait que "vraie" (dans ce contexte) est essentiellement "se déduit de la cohérence dans une arithmétique élémentaire".

Mais tu ajoutes me semble-t-il un peu trop de précisions "de logiciens". Le but de ce paragraphe est à mon avis de rendre compte de ce qu'on entend par "formule vraie" (pour la formule de Gödel) pour quelqu'un qui n'est pas logicien, sachant que tout mathématicien a l'habitude de parler de "vrai" pour des énoncés Pi^0_1. Pour les détails on peut renvoyer à d'autres articles.

Une chose avec laquelle je ne suis pas d'accord : le théorème de Tarski est hors sujet à cet endroit, et ça embrouille plutôt. On ne parle pas de la vérité d'une formule en général, or dans le théorème de Tarski c'est la hauteur non bornée de la hiérarchie qui intervient. Ici ce qui n'est pas si clairement défini que ça en a l'air, mais tout à fait habituel en même temps, c'est ce que signifie "pour tout entier".

La remarque sur le fait que Gödel ne parle pas de vérité explicitement : mais il parle de "pour tout entier ...", et ça veut dire que tout modèle est un omega-modèle, c'est plutôt un détail historique qui demande d'être contextualisé plutôt que donner brut (les raisons pour lesquelles Gödel ne parle pas de vérité alors qu'il pense les choses de cette façon). Détail historique parce que les présentations "modernes" (Smorynski, Girard ...) ne le donnent plus sous cette forme.

Il faudrait préciser que ce que Girard appelle arithmétique élémentaire est plus souvent appelée arithmétique de Robinson, mais par ailleurs là c'était tout à fait volontaire de ne pas rentrer dans les détails d'une axiomatisation dans ce paragraphe, détails qui sont évoqués (insuffisamment probablement) plus loin. Je ne suis pas convaincu que ce soit utile. Il me semble qu'ici la notion de preuve intuitive "par le calcul" suffit, et que le fait (intéressant par ailleurs) que ça puisse s'axiomatiser avec un nombre fini d'axiomes simples n'ajoute pas à la compréhension du théorème.

Pour modèle et théorie des ensembles : il faut être prudent, beaucoup de choses se font avec des modèles définissables dans l'arithmétique, et assez naturellement dans des extensions conservatives de l'arithmétique par des méthodes du style théorie des classes adaptée à l'arithmétique (ce qu'ils utilisent dans le reverse-math). Proz (discuter) 30 juin 2015 à 08:39 (CEST)

« Pas pour du tout [déplacer la section Preuves du théorème d'incomplétude] » : ok, j'oublie.

« tu ajoutes me semble-t-il un peu trop de précisions "de logiciens" » : c'est vrai. J'ai viré le paragraphe sur les symboles de l'arithmétique qui n'apporte pas grand chose, c'est mieux comme ça ou il faut encore alléger ?

« le théorème de Tarski est hors sujet à cet endroit » : ok, y a pu Tarski.

« ce que Girard appelle arithmétique élémentaire est plus souvent appelée arithmétique de Robinson » : ok, c'est corrigé.

« Pour modèle et théorie des ensembles : il faut être prudent » : non coupable ! Je ne veux pas dénoncer mais (prétérition) c'est Dfeldmann qui a ajouté la référence à « une théorie des ensembles » là où je mentionnais « quelques principes de théorie des ensembles », j'ai enlevé toute référence à la ou une théorie des ensembles, je suis bien d'accord que ça n'est pas à propos.

« La remarque sur le fait que Gödel ne parle pas de vérité explicitement » : j'ai supprimé la plus grande partie du paragraphe. Ça me dérange un peu parceque je crois (sans en être certain à 100%) que ce qui était dit était... vrai, mais bon si c'est pas consensuel pas la peine d'insister. --Laurent de Marseille (discuter) 30 juin 2015 à 19:25 (CEST)

Je suis désolé de me réveiller si tard, mais j'insiste : la vérité est souvent une notion relative (à l'axiomatique ou au modèle choisi), mais il y a des vérités absolues ("Je crois que 2 et 2 sont 4, Sganarelle, et que 4 et 4 sont 8", dit un esprit fort célèbre...), surtout dans le contexte du théorème (il faut bien disposer des entiers pour pouvoir définir un code de Gödel)--Dfeldmann (discuter) 30 juin 2015 à 21:50 (CEST)

Bien sûr qu'il y a des vérités absolues. Mais on ne peut pas définir celles-ci mathématiquement, donc difficile à invoquer dans la démonstration d'un théorème. Le mieux que l'on puisse faire est d'invoquer la vérité dans le modèle standard comme la référence en matière de vérité en mathématique, j'imagine que c'est le genre de chose que tu voudrais faire ?

Oui, plus ou moins... Comme nous ne sommes pas sur l'article Vérité (mathématiques) (qui n'existe d'ailleurs pas ; le plus proche, c'est Vérité scientifique#Dans les sciences déductives), mon but était plutôt de m'opposer à une rédaction trop binaire (la prouvabilité est une notion syntaxique aisément définissable rigoureusement au niveau de la théorie vs. la vérité est une notion sémantique toujours relative et correspondant à une méta-théorie), mais plutôt écrire quelque chose comme : "la vérité, qui est le plus souvent une notion relative aux axiomes choisis (ou au modèle de référence choisi) peut, dans le contexte des théorèmes de Gödel, recevoir une définition sur laquelle la plupart des mathématiciens se mettent d'accord, à savoir la "vérité" dans le modèle standard de l'arithmétique" . Bon, après, je ne suis pas chaud pour une formulation trop technique (et celle que je viens d'écrire est bien lourde), mais je crois que l'idée est importante, parce qu'on lit trop souvent dans d'autres articles des phrases comme "Si l'hypothèse de Goldbach est indécidable, alors elle est vraie", totalement incompréhensibles si on n'explicite pas cette question. Après, je suis pas vraiment une source, hein --Dfeldmann (discuter) 1 juillet 2015 à 10:10 (CEST)

Tenté d'écrire quelquechose mais je n'arrive pas à faire mieux que ce que tu proposes ; te laisse la main.

Je ne sais pas s'il est nécessaire d'expliquer le coup de la conjecture de Goldbach mais tant pis, ça me fait trop envie, j'explique : c'est un énoncé élémentaire (Pi_0^1 au sens technique) c'est à dire ce la forme : pour tout entier on a telle propriété décidable (s'il est pair c'est la somme de deux premiers). Si cet énoncé est indécidable (sous-entendu dans une théorie qui contient l'arithmétique, par exemple ZF) sa négation en particulier n'est pas prouvable ; mais celle-ci est de la forme : il existe un entier satisfaisant une propriété décidable (être pair et ne pas être la somme de deux premiers). Si cet énoncé était vrai (dans le modèle standard) il serait très facile à démontrer : il suffirait de trouver l'entier en question (en les essayant tous, on finira par en trouver un puisque l'énoncé est vrai) et de vérifier la propriété décidable pour celui-ci. Donc dire qu'il n'est pas prouvable revient à dire qu'il n'est pas vrai, donc que sa négation, à savoir la conjecture de Goldbach, l'est. --Laurent de Marseille (discuter) 1 juillet 2015 à 21:18 (CEST)

Je n'ai pas eu le temps de relire toutes les dernières modif. un peu court en ce moment. je suis également gêné parce que la prouvabilité pour la majorité des personnes ça intègre le fait d'admettre le système d'axiomes (évidemment ce n'est pas ce que tu veux dire et formellement tu as raison). Par ailleurs, si tout ce qui est de l'ordre du calculable, en particulier la vérité des énoncés Sigma_0 comme 2 et 2 font 4, est bien "non discutable", la prouvabilité c'est quand même Sigma_1, déjà ce que tu écris est-il si clair (vérité c'est aussi fausseté) ?

Le réalisme mathématique (position platonicienne qui est celle de Gödel) est une position philosophique tout à fait cohérente avec les théorèmes d'incomplétude et induit une notion de vérité absolue. Même si on ne suit pas cette position, imaginer momentanément la vérité comme absolue n'est pas un problème parce qu'au final on ne lui demandera jamais à un instant donné que de vérifier un nombre fini de règles, mais si on les posait à l'avance on retrouverait l'incomplétude.

Une autre remarque : il faudrait absolument éviter "vérité dans une théorie" (d'ailleurs je ne sais pas ce que ça veut dire), là je pense qu'on perd tout le monde. Il em semble que l'un des problèmes sur tout ce chapeau c'est une confusion pour le lecteur entre "vrai dans un modèle", et "vrai dans le modèle standard" (ou "vrai" tout court si tu préfères). Je pense que seul "vrai dans le modèle standard" est vraiment utile pour cet article (même si on parle un tout petit peu de non standard).

Globablement j'ai l'impression que tu veux trop en dire, il faudrait garder la ligne : ce qui est utile pour comprendre le théorème, et la suite de l'article. Parfois il vaut mieux ne rien dire que des chose qui peuvent être mal interprétées. Ce que propose Denis à propos de l'hypothèse de Goldbach montre exactement ce qu'il faut comprendre, d'ailleurs c'est pour ça que l'exemple est souvent utilisé (conjecture Pi^0_1), donc on pourrait repartir là dessus.

Quelques remarques positives pour ne pas avoir l'air que de critiquer : sur le théorème de Löb c'est très clair et très bien (mais peut-être pas placé dans le bon paragraphe), le paragraphe final de "Vérité et démontabilité" aussi, globablement c'est mieux écrit.

Pour "Gödel ne parle pas explicitement ... " : bien-sûr que, dans son article, c'est juste. Mais c'est à dire dans un paragraphe "histoire" manquant, et surtout avec explication et contexte, à partir d'articles d'histoire des math. de l'édition critique des oeuvres de Gödel, qui prennent en compte d'autre sources que le seul article, mais aussi la correspondance, les déclarations ultérieures de Gödel, de von Neumann et d'autre qui ont échangés avec Gödel à l'époque .... Proz (discuter) 1 juillet 2015 à 21:25 (CEST)

Démonstration alternative contradictoire

Lemme préliminaire

Voir ici l'existence d'un intermédiaire logique ENTRE les propositions P et nonP, nécessairement distinctes (principe de non-contradiction). Cet intermédiaire est de la forme (ni-P ; ni-nonP) AVANT choix décisionnel intelligent et (soit-P ; soit-nonP) APRÈS).
On note que cet intermédiaire N'EST PAS en contradiction avec le principe du tiers exclu si et seulement si on fait un choix décisionnel. Par conséquent ... il suffit de le faire !

Application

T désignant une théorie incomplète dans laquelle G est non-démontrable ALORS T est complétable par une proposition P telle que G soit démontrable dans T + P. Cette proposition existe : elle est de la forme (ni-G ; ni-nonG) et nonP est de la forme (soit-G ; soit-nonG). Nous avons alors :

1. T + G : dans quel cas G est démontrable dans la théorie T complétée.
2. T + nonG : dans quel cas G est non-démontrable dans la théorie complétée.

Tout le problème se concentre sur la proposition transitive Si P ALORS G !
La solution passe par deux questions :

1. Si non-P ALORS (?) non-G : OUI : P est cohérente
2. Si non-P ALORS (?) non-G : NON : P est incohérente

Avec, bien sûr une possibilité intermédiaire (ni-cohérente ; ni-incohérente) Il faut chercher encore ou décider de finir !

Exemple : Soit T la théorie : on peut faire de 2 à 12 avec deux dés et G l'énoncé : faire 1 ?

• Soit la proposition : P = "on fait la somme des dés" : alors, bien sûr, non-G
• essayons non-P : alors ? c'est pas impossible si on définit non-P = "faire la différence" comme variété différentielle de P
• On peut compléter la théorie T par et aussi 1.

--Supreme assis (discuter) 31 août 2015 à 12:45 (CEST)

Désolé, mais Wikipédia n'est pas le lieu pour des travaux personnels, si pertinents et brillants soient-ils. Voyez WP:TI.--Dfeldmann (discuter) 31 août 2015 à 12:37 (CEST)

Oui, je sais bien c'est pour cela que j'ai titré alternative dans la page de discussion. Cela fait l'objet d'un travail de recherche sur la wikiversité (lieu qui exige justement des WP:TI !) qui peut éventuellement intéresser un chercheur. merci de votre remarque --Supreme assis (discuter) 31 août 2015 à 12:45 (CEST)

Pourquoi pas, mais votre développement n'a pas sa place dans la page de discussion de l'article, qui doit seulement servir à l'améliorer (ou à le contester) dans le respect des principes de Wikipédia. Si vous voulez signaler un travail "alternatif" sur Wikiversité, faites-le en donnant seulement le lien, ou mieux encore, en passant par une page adaptée (l'Oracle ?). En rapport avec votre approche, je vous suggérerais bien de jeter un coup d'œil sur l'article Logique modale (et peut-être aussi Intuitionnisme), mais en tout état de cause, cela n'a que peu de rapport avec Gödel...--Dfeldmann (discuter) 31 août 2015 à 13:55 (CEST)

Oui merci. Je pense qu'il s'agit d'une amélioration et donc pas vraiment conflictuel avec la place occupée (?). Toute théorie est ... complétable. je pense intégrer la logique modale prochainement. Quant à la logique intuitionniste elle a ses limites qui dépendent justement d'une possibilité d'intégration (réalité objective). Enfin, il y a une discussion sur wikiversité justement sur le sujet de communiquer ENTRE l'encyclopédie (qui exclut les TI) ET la wikiversité (qui les exige) vous serez le bienvenu ainsi que d'autres de donner un avis. Merci--Supreme assis (discuter) 1 septembre 2015 à 10:28 (CEST)

La Wikiversité « exige » les TI ??? Qu'elle les tolère, je veux bien, mais parler d'exigence me semble très poussé.

Du reste, comme d'habitude : merci de ne pas participer aux pages de discussion des articles de l’encyclopédie si c'est pour publier vos travaux ou recruter de potentiels membres de votre groupe de recherche. Kelam (discuter) 14 septembre 2015 à 14:12 (CEST)

Probleme dans la "preuve" du second theoreme?

Je ne comprends pas l'argument suivant dans la preuve du second theorème d'incomplétude. Il est décreté: <<Récapitulons: on a montré dans T que Dem_T(#G) => non Coh_T.>> En fait c'est ce point que je vois pas! Si j'ai bien compris, l'argument précedant cette ligne est le suivant: si de T on déduit syntaxiquement Dem_T(#G) alors de T on déduit syntaxiquement non Coh_T. Mais cela ne veut pas dire que de T on déduise Dem_T(#G) => non Coh(T).

Me suis-je trompé?

PS: J'ai refait par moi-même une preuve que les 2 arguments "T cohérente" et "de T on déduit coh(T)" menait à une contradiction. Pour ce j'utilise bien les hyp. D1, D2, D3 et D'3 plus un axiome: si de T on deduit Dem_T(#(A et B)) alors de T on deduit aussi Dem_T(#A) et Dem_T(#B).

Merci en tout cas pour votre travail et article intéressant. Désolé si je me suis trompé. Cordiales salutations.

--119.243.7.58 (discuter) 10 juin 2016 à 09:18 (CEST) Vincent Schmitt

Reformulé (Peut-être pas bien clair), c'est de T, Dem_T(#G) on déduit non Coh_T qui veut bien dire de T on déduit Dem_T(#G) => non Coh(T). Inutile d'introduire formellement le "et" par ailleurs, ces conditions sont bien établies (et déjà même si je crois pas entièrement explicite pour cette formulation de D2 dans Hilbert-Bernays). Proz (discuter) 31 janvier 2018 à 21:12 (CET)

Diagramme vérité/démontrabilité

A été ajouté aujourd'hui un diagramme qui suppose que tout ce qui est démontrable est vrai (au sens habituel, je suppose, satisfait dans le modèle standard). C'est une hypothèse très forte sur le système axiomatique en jeu, qui n'est pas nécessaire pour les théorèmes d'incomplétude (ce que montre d'ailleurs le théorème même). Je ne pense pas que que ce soit une bonne illustration. Proz (discuter) 4 avril 2023 à 21:17 (CEST)

Je viens de faire, indépendamment, le même retrait sur l'article Complétude (logique), avec les mêmes arguments. --Pierre Lescanne (discuter) 6 avril 2023 à 12:23 (CEST)