DÉMONSTRATION THÉORIE DE LA

Carte mentale

Élargissez votre recherche dans Universalis

La logique Π12

L'extension des résultats obtenus par Takeuti, Pohlers, Buchholz... pour le schéma de compréhension Π11 à des systèmes plus forts nécessite de remplacer la ω-logique par des logiques correspondant à de plus grandes complexités logiques, Π21 et plus généralement Π1n . Le problème de la B-règle, posé par Mostowski est le suivant : Caractériser les énoncés qui sont vrais dans tout modèle dans lequel les objets d'un type distingué Ω sont interprétés par un ordinal α et où la relation ≤ distinguée entre objets de type Ω est interprétée par l'ordre de α (B-modèles). Une réponse simple est donnée par : pour tout α, nous avons une démonstration au moyen de la α-règle, qui est l'analogue de la ω-règle, obtenu en remplaçant ω par α. Cela dit, une famille (Pα) de α-démonstrations indexées par tous les ordinaux ne constitue pas spécialement un objet syntaxique ! On définit la catégorie ON des ordinaux en prenant pour morphismes les ensembles I(α, β) d'applications strictement croissantes de α vers β. Si P est une β-démonstration, on peut, dans certaines conditions, définir, si ∈ I(α, β), une α-démonstration -1(P). Si on demande que la famille (Pα) soit telle que -1(Pβ) = Pα, alors cette famille est appelée une B-démonstration. Une B-démonstration apparaît, en fait, comme un foncteur de la catégorie ON dans une catégorie DEM de démonstrations et on vérifie qu'un tel foncteur préserve les limites directes (c'est-à-dire inductives filtrantes) et les produits fibrés. En particulier, la donnée de la famille (Pn), pour n fini, détermine uniquement (par unicité du prolongement par limites directes) la famille (Pα). Il devient alors possible de parler de B-démonstration récursive, autrement dit nous avons un concept syntaxique. (Mais l'ensemble des indices de B-démonstrations est Π12 .) Et Girard a pu établir en 1978 la B-complétude :

Théorème. Γ ⊢ Δ est vrai dans tout B-modèle si et seulement s'il y a une B-démonstration récursive de ce séquent.

Un concept proche est celui de dilatateur : un dilatateur est un foncteur de ON dans ON préservant les limites directes et les produits fibrés. La plupart des fonctions ordinales (x + 1, ωx, la hiérarchie de Veblen) sont, en fait, des dilatateurs. Comme un dilatateur est déterminé par sa restriction à la souscatégorie des entiers, il peut être récursif. Le résultat élémentaire sur les dilatateurs est le théorème de forme normale :

Théorème. Si l'on a < F(x), alors on peut écrire z = (z0 ; x0, ..., xn-1 ; x)F, ce qui signifie que : (1) z = F() (z0), si ∈ I(nx) est défini par f (0) = x0, ..., (n − 1) = xn-1, (2) n est minimum tel que (1) soit vrai. Si (1) et (2) sont vérifiés, alors la forme normale est unique.

Ce résultat généralise le théorème de forme normale de Cantor.

En utilisant une combinaison de B-logique et de dilatateurs, il est possible de donner une nouvelle démonstration de l'élimination des coupures pour l'arithmétique, ainsi que les définitions inductives. Par rapport aux résultats existant auparavant, on a ici un théorème complet d'élimination des coupures, ainsi qu'une propriété de sous-formule ; on a surtout son corollaire, également dû à Girard (1979) :

Théorème (majoration des fonctions ω1CK -récursives). Si f est une fonction ω1CK -récursive, alors il existe un dilatateur récursif D tel que ∀x (ω ≤< ω1CK  → F(x) < D(x)).

Ce résultat ramène, en quelque sorte, la ω1CK -récursion à la récursivité habituelle. L'élimination des coupures utilise un principe d'induction sur les dilatateurs qui a ceci de particulier que la relation d'ordre entre dilatateurs est telle que l'ensemble des prédécesseurs de F est une classe bien ordonnée de type d'ordre F(On). Pour l'arithmétique, l'élimination des coupures donne l'ordinal de Howard η0.

Ces méthodes fonctorielles s'étendent et se généralisent. En particulier, en utilisant les concepts Π13 , analogues des concepts de la logique Π12 , il a été possible de mener à bien l'analyse ordinale du schéma de compréhension Π12 (Girard, 1981) et, vraisemblablement, cette méthode se généralise au schéma de compréhension Π1n . Le principal problème est de trouver des applications à tous ces résultats.

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 09 août 2022. URL : https://www.universalis.fr/encyclopedie/theorie-de-la-demonstration/