DÉMONSTRATION THÉORIE DE LA

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 e [...]