Discuter:Gerhard Gentzen

Un article de Wikipédia, l'encyclopédie libre.

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)

Sommaire 1 Relativité de la cohérence 2 Cohérence « absolue » 3 « Petit » ordinal 4 Cohérence de l'arithmétique de Peano par récurrence transfinie jusqu'à epsilon-zéro 5 Théorème de Gentzen

[modifier] 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.

[modifier] 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)

[modifier] « 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)

[modifier] 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)

[modifier] 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)