From Herbrand schemes to functional interpretation

Résumé technique : Des schémas de Herbrand à l'interprétation fonctionnelle

Énoncé du problème
L'article traite du défi consistant à extraire des disjonctions de Herbrand directement à partir de preuves du calcul des séquents classique sans dépendre de l'élimination des coupures. Bien que le théorème de Herbrand soit traditionnellement prouvé via l'élimination des coupures (produisant un « milieu de séquence »), des travaux récents d'Afshari, Hetzl et Leigh ont démontré que les disjonctions de Herbrand peuvent être extraites directement en utilisant des « schémas de Herbrand » — une méthode traitant les preuves comme des schémas de récursion d'ordre supérieur. Cependant, cette approche repose sur des règles de réécriture spécifiques basées sur des grammaires. Inversement, les interprétations fonctionnelles (telles que celles de Gerhardy et Kohlenbach) opèrent généralement sur des systèmes axiomatiques de type Hilbert. L'article cherche à jeter un pont entre ces deux domaines : le noyau du mécanisme des schémas de Herbrand peut-il être reformulé comme une interprétation fonctionnelle du calcul des séquents classique, fournissant ainsi une interprétation computationnelle naturelle des preuves de séquents, similaire aux approches de la théorie des jeux ?

Méthodologie
Les auteurs développent une interprétation fonctionnelle pour le calcul des séquents classique basée sur un lambda-calcul typé étendu par un opérateur de distinction de cas. La méthodologie procède comme suit :

1. Structure des types : Le système utilise une théorie des types avec deux types atomiques : $\iota$ (individus) et $\square$ (type nul). Les types complexes sont formés via des produits et des espaces de fonctions. Crucialement, chaque formule $A$ est associée à deux types distincts :

   • Un type d'évidence $[A]$ (représentant un témoin ou une stratégie pour le « Prouveur »).
   • Un type de contre-évidence $\langle A \rangle$ (représentant un contre-témoin ou une stratégie pour le « Réfuteur »).
     Ces types sont définis de manière récursive selon la structure logique de $A$ (par exemple, $[\exists x A] = \iota \times \langle \neg A \rangle$, $[\neg A] = (\langle A \rangle \to [A]) \to \langle A \rangle$).

2. Extraction de termes (Transformateurs de termes) : Les auteurs définissent un « transformateur de termes » pour chaque occurrence de formule dans un séquent. Étant donné une preuve $p$ d'un séquent $A_1, \dots, A_n$, l'extraction associe à chaque indice $i$ un transformateur de termes $F^p_i$. Ce transformateur prend des termes de types de contre-évidence $\langle A_1 \rangle, \dots, \langle A_n \rangle$ en entrée et produit un terme de type d'évidence $[A_i]$.

   • L'extraction est définie par récursion structurelle sur la preuve $p$, correspondant à la dernière règle d'inférence utilisée (par exemple, $\exists$, $\neg\exists$, $\vee$, $\neg\vee$, coupure, contraction).
   • Contrairement aux schémas de Herbrand, qui nécessitent des règles de réécriture ad hoc pour les symboles non terminaux, le comportement de ces termes extraits est entièrement régi par les règles de réécriture standard de la théorie des types sous-jacente (réduction bêta, projection et distinction de cas).

3. Cadre logique : L'extraction opère dans un système sans quantificateurs $QF$ augmenté d'axiomes pour l'opérateur de distinction de cas $[u \text{ si } A \text{ sinon } v]$. Le résultat principal établit que pour toute preuve $p$ d'un séquent $A_1, \dots, A_n$, et pour tout terme de contre-évidence fermé $u_1, \dots, u_n$, la disjonction des formules interprétées est vérifiée :
   $$\vdash_{QF} A_1 \frac{F^p_1 \vec{u}}{u_1} \vee \dots \vee A_n \frac{F^p_n \vec{u}}{u_n}$$
   Ici, la notation $A \frac{t}{u}$ représente la formule $A$ où l'évidence $t$ est opposée à la contre-évidence $u$.

Contributions clés

• Reformulation des schémas de Herbrand : L'article démontre que les schémas de Herbrand peuvent être reformulés comme une interprétation fonctionnelle du calcul des séquents. Les « symboles non terminaux » d'un schéma de Herbrand correspondent aux transformateurs de termes extraits ici, et les « règles de réécriture » du schéma sont remplacées par les règles de réduction intrinsèques du lambda-calcul.
• Extraction directe sans élimination des coupures : La méthode fournit un algorithme direct pour extraire des termes réalisants (et par la suite des disjonctions de Herbrand) à partir de preuves du calcul des séquents sans effectuer d'élimination des coupures.
• Construction modulaire : Le processus d'extraction est modulaire ; le transformateur de termes pour une preuve est construit uniformément à partir des transformateurs de ses sous-preuves immédiates en fonction de la règle d'inférence appliquée.
• Gestion de la contraction : Les auteurs utilisent l'opérateur de distinction de cas (de Gerhardy et Kohlenbach) pour gérer la structure de branchement introduite par les règles de contraction dans le calcul des séquents, évitant ainsi le besoin de structures de types plus complexes « herbrandisées » impliquant des ensembles finis.

Résultats

• Théorème 1 (Correction) : Pour toute preuve $p$ d'un séquent $A_1, \dots, A_n$, les transformateurs de termes extraits satisfont la propriété d'interprétation fonctionnelle : la disjonction des formules interprétées est prouvable dans $QF$ pour toute entrée de contre-évidence fermée.
• Théorème 2 (Théorème de Herbrand) : En tant que corollaire, si une formule existentielle $\exists x A$ (avec $A$ sans quantificateurs) est prouvable, l'extraction produit un ensemble fini de termes fermés $t_1, \dots, t_n$ tels que la disjonction de Herbrand $A[t_1/x] \vee \dots \vee A[t_n/x]$ est prouvable. Ceci est réalisé en réduisant le terme extrait à sa forme normale et en analysant sa structure.
• Normalisation forte : Le système de termes sous-jacent est montré comme étant fortement normalisant, garantissant que les termes extraits se réduisent toujours vers une forme canonique.

Signification et affirmations
L'article affirme que ce travail fournit une « interprétation computationnelle naturelle du calcul des séquents classique ». En reformulant les schémas de Herbrand comme une interprétation fonctionnelle, les auteurs soutiennent que le lien entre le théorème de Herbrand et l'interprétation fonctionnelle est plus fondamental qu'on ne le pensait auparavant.

Plus précisément, l'article souligne un lien conceptuel avec les approches de la théorie des jeux (telles que celles d'Alcolei et al.). Dans cette perspective :

• Les termes extraits représentent les stratégies d'un « Prouveur » dans un jeu concurrent.
• Les entrées (termes de contre-évidence) représentent les stratégies d'un « Réfuteur ».
• La structure de la preuve correspond à des processus concurrents où le Prouveur peut observer les mouvements du Réfuteur dans un « fil » (copie parallèle du jeu) et utiliser cette information pour déterminer ses propres mouvements dans un autre fil.

Les auteurs positionnent ce travail comme complétant une image émergente où les schémas de Herbrand, les interprétations fonctionnelles et la sémantique des jeux convergent pour expliquer le contenu computationnel de la logique classique. Ils déclarent explicitement que les résultats sont auto-suffisants et ne nécessitent pas de connaissance préalable des schémas de Herbrand, bien que la procédure d'extraction ait été dérivée en examinant de près la structure des types de la littérature existante sur les schémas de Herbrand.