DÉMONSTRATION THÉORIE DE LA
Article modifié le
L'ordinal ε0 et la ω-logique
À plusieurs reprises dans les années trente, Gentzen allait donner des démonstrations de cohérence pour l' arithmétique de Peano AP. Pour obtenir de tels résultats, il était nécessaire, par le second théorème d'incomplétude, de se servir de méthodes extérieures à l'arithmétique. Gentzen utilisa comme méthode l' induction transfinie jusqu'à ε0, où ε0 est défini comme le suprémum des ordinaux ωn, avec ω0 = 1, ωn+1 = ωωn). Dans les années cinquante, Schütte allait donner une version plus accessible de ces mêmes résultats : essentiellement, l'arithmétique de Peano est obtenue à partir du calcul des prédicats en ajoutant le schéma d'axiomes d'induction :
![](/media_src/v07f0174a03.png)
![](/media_src/v07f0174a04.png)
Le schéma d'induction devient démontrable dans la ω-logique ; c'est, en fait, un cas particulier du théorème suivant, dû à Orey :
Théorème d'ω-complétude. Γ ⊢ Δ est vrai dans tout ω-modèle (modèle dont le domaine est exactement N et où 0̄ et S sont interprétés de façon standard) si et seulement s'il y a une ω-démonstration récursive de Γ ⊢ Δ.
Dans la pratique, on se contentera de construire explicitement une démonstration d'un axiome d'induction à l'aide de (d∀ω). On a le Hauptsatz suivant, dû à Schütte :
Théorème. La ω-logique vérifie l'éliminition des coupures. La démonstration consiste, pour l'essentiel, à remplacer toute coupure :
![](/media_src/v07f0174b01.png)
![](/media_src/v07f0174b02.png)
Donc, par une induction jusqu'à ε0, on montre facilement qu'il ne saurait y avoir de démonstration du séquent ⊢. Ici encore, on peut poser la question « N'y a-t-il pas surcharge d'intentions ? » Après tout (Kreisel dixit), « les doutes quant à la cohérence sont infiniment plus douteux que la cohérence elle-même ». On rappellera le mot d'un mathématicien français : « Gentzen est le type qui a prouvé la cohérence de l'arithmétique, c'est-à-dire de l'induction jusqu'à ω, au moyen de l'induction jusqu'à ε[...]
La suite de cet article est accessible aux abonnés
- Des contenus variés, complets et fiables
- Accessible sur tous les écrans
- Pas de publicité
Déjà abonné ? Se connecter
Écrit par
- Jean-Yves GIRARD : docteur ès sciences, maître de recherche au C.N.R.S.
Classification
Média
Autres références
-
GENTZEN GERHARD (1909-1945)
- Écrit par Gabriel SABBAGH
- 133 mots
Logicien allemand, né à Greifswald et mort à Prague lors de son emprisonnement par les Soviétiques. Gentzen a développé l'étude des systèmes de déduction naturelle et établi un théorème d'élimination des coupures. Gerhard Gentzen a également donné une démonstration de consistance de l'arithmétique...
-
HERBRAND JACQUES (1908-1931)
- Écrit par Gabriel SABBAGH
- 87 mots
Logicien et mathématicien français né à Paris et mort à Saint-Christophe-en-Oisans dans un accident de montagne. La brève carrière de Jacques Herbrand est marquée par sa démonstration, essentiellement correcte, d'un théorème central du calcul des prédicats du premier ordre, qui a...
-
HILBERT DAVID (1862-1943)
- Écrit par Rüdiger INHETVEEN , Jean-Michel KANTOR et Christian THIEL
- 14 731 mots
- 2 médias
...Hilbert s'est donné pour but de sauver la position classique de la mathématique et, en même temps, de forger de nouveaux outils permettant de donner une démonstration absolue de non-contradiction de l'arithmétique d'abord, puis de l'analyse. Il se proposa d'établir la non-contradiction absolue d'un système... -
POST EMIL LEON (1897-1954)
- Écrit par Bernard JAULIN
- 623 mots
Mathématicien américain né à Augustów (Pologne) et mort à New York. Arrivé aux États-Unis en 1904, Emil Post obtint son Ph.D. à l'université Columbia de New York en 1920. Il était membre de l'American Mathematical Society depuis 1918 et de l'Association for Symbolic Logic dès sa fondation...
Voir aussi
- CATÉGORIES & FONCTEURS
- FERMAT GRAND THÉORÈME DE
- GOLDBACH CONJECTURES DE
- ORDINAL, mathématiques
- COMPLÉTUDE THÉORÈMES DE
- ARITHMÉTIQUE FORMELLE
- INCOMPLÉTUDE THÉORÈMES D'
- INDUCTION TRANSFINIE
- HILBERT PROGRAMME DE
- RIEMANN HYPOTHÈSE DE
- COHÉRENCE, logique mathématique
- HAUPTSATZ, logique mathématique
- SÉQUENTS CALCUL DES