4. 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 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 (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 seulem […]
… pour nos abonnés, l'article se prolonge sur 9 pages…
