DÉMONSTRATION THÉORIE DE LA

Carte mentale

Élargissez votre recherche dans Universalis

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 :

où A est un énoncé arbitraire. Schütte introduit une logique, la ω-logique, où ce schéma est logiquement démontrable : les règles pour ∀ sont :
On écrit des règles symétriques pour le quantificateur ∃. La principale nouveauté de ces règles, c'est leur caractère infinitaire : la règle (d∀ω) nécessite une infinité de prémisses. Dans ces conditions, est-il encore possible de parler d'aspect syntaxique ? oui ; car, bien qu'infinies, ces démonstrations (qui ne sont rien d'autre que des arbres dont les nœuds sont occupés par des séquents) peuvent être représentées par des fonctions récursives dans les bons cas, d'où un concept de ω-démonstration récursive. Par contre, l'ensemble des indices (ou codes) de ω-démonstrations récursives est de complexité logique Π11 .

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 :

par :
Si l'on part d'une démonstration dans AP, alors, on obtient une démonstration avec coupures dans la ω-logique en utilisant la démonstration des axiomes d'induction, puis, par élimination des coupures, une démonstration sans coupures du même séquent en ω-logique. On peut calculer la hauteur d'une telle démonstration (c'est-à-dire l'ordinal qui mesure la hauteur de l'arbre de la démonstration) : elle est strictement inférieure à ε0. En particulier, le principe d'induction transfinie jusqu'à l'ordinal récursif ε0 nous permettra de démontrer que l'arithmétique est non contradictoire... Plus précisément et c'est un résultat dû à Mints, on peut démontrer le théorème d'élimination des coupures pour la ω-logique, de telle manière que l'on ait la borne effective ε0 pour toutes les démonstrations issues de l'arithmétique (mais rien ne dit que les arbres de démonstration ainsi obtenus sont bien fondés) et de telle manière que le tout se fasse élémentairement.

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'à ε0 ». En fait, il est facile de remarquer que, si d'un côté on a l'induction jusqu'à ω, c'est sur des énoncés arbitraires, alors que l'induction jusqu'à ε0 utilisée par Gentzen se fait uniquement sur des énoncés sans quantificateurs. Autrement dit, un quantificateur égale une exponentielle ordinale. Le résultat de Gentzen n'est donc pas aussi stupide que certains le laissent entendre.

La découverte de la relation entre ε0 et AP induisit les théoriciens de la démonstration à parler de l'« ordinal » de AP et à rechercher les ordinaux d'autres théories. En particulier, les travaux de Takeuti (1967), repris et simplifiés par Pohlers (1975), allaient permettre d'analyser, toujours au moyen de la ω-règle, les théories de définitions inductives ou, de manière équivalente, le schéma de compréhension Π11. Par exemple pour le système de définitions inductive [...]

1  2  3  4  5
pour nos abonnés,
l’article se compose de 10 pages

Écrit par :

Classification

Autres références

«  DÉMONSTRATION THÉORIE DE LA  » est également traité dans :

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 du premier ordre fondée sur l'induction transfinie jusqu'au premier nombre ordinal inaccessible pour […] Lire la suite

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 des rapports étroits avec le théorème de complétude et les travaux de Gentzen, ainsi que par d'intéressantes contributi […] Lire la suite

HILBERT DAVID (1862-1943)

  • Écrit par 
  • Rüdiger INHETVEEN, 
  • Jean-Michel KANTOR, 
  • Christian THIEL
  •  • 14 856 mots
  •  • 1 média

Dans le chapitre « Programme de Hilbert et théorie de la démonstration »  : […] Pour deux raisons, la non-contradiction de l'arithmétique par rapport à une autre théorie ne semblait plus démontrable. D'une part, les démonstrations relatives de non-contradiction utilisaient toutes déjà des moyens arithmétiques ; d'autre part, la seule théorie par rapport à laquelle une telle démonstration aurait pu être menée – la logique développée autour d'une théorie classique des ensembles […] Lire la suite

POST EMIL LEON (1897-1954)

  • Écrit par 
  • Bernard JAULIN
  •  • 622 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 en 1935. Sa thèse de doctorat, publiée en 1921, porte sur le calcul propositionnel de A. N. Whitehead et B. Ru […] Lire la suite

RÉCURSIVITÉ, logique mathématique

  • Écrit par 
  • Kenneth Mc ALOON, 
  • Bernard JAULIN, 
  • Jean-Pierre RESSAYRE
  •  • 9 371 mots

Dans le chapitre « Indécidabilité de propriétés classiques »  : […] Propriété b . Pour tout ensemble non vide A ⊂ F R ( p ) , l'ensemble ϕ −1 (A) est non récursif. Ainsi, si on considère une propriété des fonctions calculables définissant un ensemble non vide A ⊂ *F R ( p ) , l'ensemble ϕ −1 (A) des programmes permettant de calculer (ou qui définissent) ces fonctions n'est pas récursif. Par exemple, pour p  = 1, si : ϕ −1 (A) est l'ensemble des programmes qui s' […] Lire la suite

Voir aussi

Pour citer l’article

Jean-Yves GIRARD, « DÉMONSTRATION THÉORIE DE LA », Encyclopædia Universalis [en ligne], consulté le 13 août 2022. URL : https://www.universalis.fr/encyclopedie/theorie-de-la-demonstration/