Discussion:Gerhard Gentzen

Cohérence relative

L'expression "cohérence relative" me semble incorrecte. C'est une question controversée. A mes yeux la preuve de Gentzen a un caractère de vérité absolue. La formulation "cohérence" tout court a été choisie pour sa neutralité. --TD 18 mar 2005 à 20:08 (CET)

Relativité de la cohérence

La preuve de la cohérence de l'axiome du choix et de l'hypothèse généralisée du continu avec les axiomes de ZFC (donnée par Gödel, 1938 Proceedings of the National Academy of Sciences, U.S.A, 24, 556-557, pour un exposé plus accessible, mais un peu ancien, voir Set theory and the continuum hypothesis de Paul Cohen, 1966) est une preuve de cohérence relative, en un sens presque identique à la preuve de Beltrami (1868) que la négation de l'axiome des parallèles est cohérente avec la géométrie absolue : si la gémométrie absolue (Euclide sans le 5ème postulat) est cohérente alors la géométrie absolue plus la négation de l'axiome des parallèles est cohérente.

On interprète parfois la preuve de Gentzen dans cet esprit parce qu'elle recourt explicitement à une récurrence transfinie jusqu'à un petit (relativement) ordinal infini dénombrable. On dit alors, si la théorie des ensembles infinis est cohérente alors l'arithmétique est cohérénte. L'expression cohérence relative appliquée à la preuve de Gentzen désigne cette interprétation. Celle-ci n'est pas innocente. Elle est souvent utilisée pour diminuer l'importance de la preuve de Gentzen.

Cette interprétation est contraire à l'esprit de l'oeuvre de Gentzen.

Le théorème fondamental (Hauptsatz) affirme que toute démonstration purement logique peut se ramener à une forme normale déterminée, qui n'est d'ailleurs nullement univoque. On peut formuler les propriétés essentielles d'une telle démonstration normale à peu près de la façon suivante : elle ne comporte pas de détours. On n'y introduit aucun concept qui ne soit pas contenu dans son résultat final et qui, par conséquent, ne doive pas nécessairement être utilisé pour obtenir ce résultat. (Recherches sur la déduction logique, aperçu d'ensemble, p.4-5)

Les preuves de Gentzen ont toujours un caractère minimaliste. Il n'introduit jamais plus d'hypothèses qu'il n'est vraiment nécessaire pour obtenir ses résultats. Les amateurs ne comprennent pas cela parce qu'ils ne savent pas ce qu'est un petit ordinal dénombrable, dans le cas présent. La preuve de Gentzen ne dépend pas de la théorie de Cantor en sa totalité mais seulement de principes sur des constructions ensemblistes élémentaires.

Cohérence « absolue »

Après le théorème de Gödel (d'incomplétude), il est absurde de parler de cohérence absolue. Toute démonstration de cohérence d'un système d'axiomes (comme l'arithmétique de Peano) est forcément relative (à un système d'axiomes plus fort), et celle de Gentzen n'échappe pas à la règle.

Que Gentzen pour des raisons qui lui sont propres, ait voulu avoir prouvé la cohérence de l'arithmétique dans l'absolu, c'est bien possible et vues l'ingéniosité et l'originalité de sa preuve, on peut facilement lui passer cette lubie, mais nous qui n'avons pas son génie n'aurions aucune excuse de la reprendre à notre compte.

Il est vrai que l'on a pas besoin d'invoquer toute la puissance de ZF pour justifier le théorème de Gentzen ; il n'en reste pas moins qu'il n'est pas conséquence des axiomes de l'arithmétique. Il y a d'ailleurs un rapport direct entre la preuve d'élimination des coupures dans l'arithmétique et le fameux théorème de l'hydre, théorème bien connu pour être non prouvable dans l'arithmétique.

Tout ça pour dire que la notion d'élémentaire est très... relative. On peut considérer élémentaire la preuve de Gentzen, et d'ailleurs elle a été saluée comme la première preuve combinatoire de la cohérence de l'arithmétique. Mais si on se réfère au sens que Hilbert attribuait à élémentaire alors non, la preuve de Gentzen n'est pas élémentaire... Laurent de Marseille 20 janvier 2006 à 23:10 (CET)

Il dit quoi, le théorème de l'hydre ? --Ulysse (alias UKe-CH) 2 août 2007 à 14:32 (CEST)

« Petit » ordinal

Je ne crois pas être un amateur mais je ne sais pas ce qu'est un petit ordinal dénombrable. En tout cas je suis sûr que epsilon_0 ne peut pas être considéré comme petit, il n'est même pas définissable dans l'arithmétique !

Laurent de Marseille 20 janvier 2006 à 23:13 (CET)

Cohérence de l'arithmétique de Peano par récurrence transfinie jusqu'à epsilon-zéro

Citation de l'article: "Gentzen est célèbre pour avoir démontré la cohérence de l'arithmétique de Peano (en 1936) en utilisant un principe d'induction jusqu'à l'ordinal dénombrable ε0, mais pour des formules de faible complexité logique"

Mon désir à ce sujet: peut-on me donner une référence me permettant de faire connaissance de la démonstartion ? Une référence à (une introduction à) cette preuve par un lien vers une page (ou un site pendant qu'on y est) sur la Toile serait également bienvenue; si quelqu'un fournit ça, je propose en plus de l'ajouter à la liste des réf. externes de l'article qui en ce moment ne contient que 2 items. --Ulysse (alias UKe-CH) 2 août 2007 à 14:26 (CEST)

Théorème de Gentzen

Pourquoi les pages sur le théorème sont des redirections vers la page du personnage ? Est-ce qu'il n'y aurait pas moyen de séparer les deux, et de présenter le théorème de manière formelle ? La règle de coupure n'est même pas mentionnée... C'est l'expression d'un besoin plus qu'une critique, en l'état actuel des choses j'ai dû me reporter sur l'article anglais pour me documenter. - Eusebius ^[causons] 22 novembre 2007 à 15:29 (CET)

Petite remarque préliminaire: Gentzen est connu pour deux théorèmes:

1. le théorème d'élimination des coupures en calcul des séqents,
2. le théorème de cohérence de l'arithmétique.

Ceci dit, comme les articles sur ces théorèmes n'existaient pas, c'est je pense une raison de facilité qui a créé ces hyperliens. Il faut donc écrire ces articles ou la partie des articles qui manque. Si j'ai le temps je m'attaquerai au théorème d'élimination des coupures en calcul des séquents comme une section de l'article sur le calcul des séquents. Pierre de Lyon (d) 23 novembre 2007 à 09:48 (CET)

J'ai corrigé les liens mais il faut compléter Calcul des séquents#Théorème d'élimination des coupures Outs (d) 13 mars 2009 à 08:18 (CET)

consistance et incomplétude

La preuve de Gentzen est absolue, comme il est vrai que l'on obtient une théorie formelle axiomatiquement consistante capable de formaliser l'arithmétique de Peano (par exemple) en la complétant avec l'axiome de choix... Cette théorie (Peano + AC) est cependant incomplète, c'est à dire que dans le langage de cette théorie, on pourra formuler une proposition arithmétique dont on ne pourra pas démontrer la valeur de vérité. Cette incomplétude ne remet absolument pas en cause la consistance de l'arithmétique de Peano dans (Peano + axiome de choix)... Le caractère "absolue" résulte du fait que la preuve de Gentzen est parfaitement récursive car elle n'ajoute aucune hypothèse supplémentaire puisqu'elle utilise le caractère dénombrable d'Epsilon 0.

Bien qu'amateur, j'ai l'impression que beaucoup de "pros" n'ont toujours pas compris que les deux théorèmes d'incomplétude ne disent pas qu'il est impossible de concevoir une théorie formelle récursivement axiomatisable capable de formaliser l'arithmétique qui soit consistante... Les théorêmes d'incomplétude affirment seulement (grace au théorême de complétude) que la consistance ne peut pas résulter des axiomes qui formalisent l'arithmétique des entiers naturels... Il faut pour celà adjoindre un axiome supplémentaire (équivalent à l'axiome de choix) qui permet alors de décider de la consistance de PEANO. Mais dans un même temps, celà enrichit le langage de la théorie et permet alors de formuler des propositions arithmétiques indémontrables.

La preuve de Gentzen est absolue :

La démonstration de la cohérence de l'arithmétique de Peano se fait dans un système plus riche que celui qui formalise simplement l'arithmétique de Peano (en celà, il ne contardit pas le second théorême d'incomplétude). En outre, la cohérence du système plus riche ne résulte pas des axiomes de l'arithmétique de Peano. La preuve de Gentzen démontre ainsi la consistance absolue de l'arithmétique de PEANO et du système axiomatique plus riche qui permet cette démonstration. Le premier théorème d'incomplétude permet alors de démontrer que l'arithmétique de PEANO n'est pas complète car elle est consistante...

Mon grand-père (qui était lui un mathématicien "pro") disait toujours qu'il fallait distinguer la récursivité du paradoxe de Richard de l'imprédictivité du paradoxe de Russell en déclarant que : "L'ensemble des idées n'est pas l'idée d'ensemble". — Le message qui précède, non signé, a été déposé par 192.54.145.146 (discuter), le 18 décembre 2014 à 12:27

Bonjour, votre intervention est très intéressante mais je ne crois pas que la preuve de Gentzen [soit] absolue, comme vous le dites au début de votre intervention, si vous entendez par "absolu" que Gentzen a démontré définitivement la cohérence de l'arithmétique.

On a simplement, et je crois, vu vos connaissances, que vous serez d'accord, des théorèmes de cohérences relatives, du genre : cohérence(ZF) |- cohérence(AP), sauf que pour démontrer "cohérence(ZF)" il faudra se placer dans une théorie plus forte que ZF, etc indéfiniment.

Le point sur le sujet est que toute sur-théorie cohérente et récursive de AP, dont AP (si elle est cohérente), ne peut à elle seule démontrer sa (propre) cohérence [d'où toute preuve de cohérence, pour ces théories, amène à une régression à l'infini sur les preuves de cohérence] ; ce que disent justement les thms d'incomplétude.

Sommes-nous d'accord ? Mais p.-e. votre intervention, touffue, portait sur d'autres points.

Bien cordialement,

P.S : n'hésitez pas à vous créer un login (ce qui facilite les échanges) et à participer à l'amélioration des articles au gré de vos compétences et envies.

--Epsilon0 ε₀ 29 décembre 2014 à 22:07 (CET) (<-- oui c'est mon login sur wikipédia ;-) ; pure coïncidence, je crois.)

Le premier théorême d'incomplétude de Godel peut faire croire qu'incomplétude et consistance sont 2 concepts de même nature car alternatifs. Mais ce n'est pas le cas. Dès qu'il existe une proposition inconsistante alors toutes les propositions sont inconsistantes ipso facto. Rien de tel pour une proposition indécidable. La démonstartion de Gentzen utilise cette différence de nature. Il considère que l'on peut utiliser le transfini dénombrable pour démontrer la consistance de l'arithmétique : il n'introduit epsilon 0 de manière imprédictive mais comme conséquence de l'induction logique (celle du calcul des prédicats qui est compléte mais non récursive). Je crois que dans l'esprit de Gentzen celui-ci considère que le second théorême d'incomplétude succombe à la semi-décidabilité. Pour Getzen, l'introduction de l'infini dénombarble si elle enrichie dans un sens la théorie cet enrichissement n'est pas imprédictif. C'est un enrichissement relatif donc sa preuve est absolue... — Le message qui précède, non signé, a été déposé par 192.54.145.146 (discuter), le 4 novembre 2015 à 10:05‎

Qu'appelez-vous « proposition inconsistante »? Que signifie l'adjectif « imprédictif » ? Qu'est-ce que « l'induction logique » --Pierre de Lyon (discuter) 4 novembre 2015 à 11:32 (CET)

Pardon je voulais dire imprédicatif (imprédicativité). Une proposition inconsitante est selon moi une proposition dont on démontre qu'elle est à la fois vraie et fausse à la différence d'une proposition indécidable dont on ne peut connaitre la valeur de vérité. Selon moi la preuve de Gentzen démontre que si l'on ne peut enrichir une théorie formelle récursivement axiomatisable et capable de formaliser l'arithmétique pour la rendre complète, il est possible de l'enrichir en utilisant epsilon 0 (infini dénombrable) pour la rendre consistante donc incomplète. C'est du moins comme ça que je vois les choses... 192.54.145.146 (discuter) 4 novembre 2015 à 16:28 (CET)