DÉMONSTRATION THÉORIE DE LA

La logique Π¹₂

L'extension des résultats obtenus par Takeuti, Pohlers, Buchholz... pour le schéma de compréhension Π₁¹ à des systèmes plus forts nécessite de remplacer la ω-logique par des logiques correspondant à de plus grandes complexités logiques, Π₂¹ et plus généralement Π¹_n . 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 f ∈ I(α, β), une α-démonstration f ^-1(P). Si on demande que la famille (P_α) soit telle que f ^-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 (P_n), 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 Π¹₂ .) 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 z < F(x), alors on peut écrire z = (z₀ ; x₀, ..., x_n-1 ; x)_F, ce qui signifie que : (1) z = F(f ) (z₀), si f ∈ I(n, x) est défini par f (0) = x₀, ..., f (n − 1) = x_n-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 ω₁^CK -récursives). Si f est une fonction ω₁^CK -récursive, alors il existe un dilatateur récursif D tel que ∀x (ω ≤x < ω₁^CK  → F(x) < D(x)).

Ce résultat ramène, en quelque sorte, la ω₁^CK -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 [...]