Résumé Technique : Sémantique Doctrinale de la Logique du Premier Ordre Dirigée

1. Énoncé du Problème

L'article aborde le défi de formaliser l'égalité dirigée au sein d'un cadre logique. Alors que la perspective catégorielle de Lawvere a caractérisé avec succès l'égalité classique comme un adjoint à gauche de la contraction, cette approche repose sur la symétrie. Dans la théorie des types dirigée, où les types sont interprétés comme des catégories (ou des préordres) plutôt que comme des groupoïdes (ou des ensembles), l'égalité devient une relation asymétrique (par exemple, une réécriture $a \to b$ ou un ordre $a \le b$).

La difficulté centrale réside dans la gestion de la variance (polarité). Dans un cadre dirigé, une variable peut apparaître dans une position « négative » (contravariante, par exemple la source d'un morphisme) ou dans une position « positive » (covariante, par exemple la cible). Les règles logiques standard pour l'égalité (réflexivité et règle J/élimination) échouent dans ce contexte car elles supposent implicitement la symétrie ou permettent aux variables d'apparaître simultanément dans les deux polarités d'une manière qui conduirait à dériver la symétrie ($a \le b \vdash b \le a$), ce qui est invalide en logique dirigée. Les tentatives antérieures de théorie des types dirigée peinent souvent avec ces contraintes de polarité, en particulier dans le contexte de la logique sans pertinence des preuves (où l'égalité est une proposition, et non un type avec plusieurs habitants).

2. Méthodologie

Les auteurs développent une logique du premier ordre dirigée (dFOL) et sa sémantique doctrinale en généralisant le cadre des hyperdoctrines de Lawvere.

Syntaxe : Contextes Polarisés

La syntaxe introduit un contexte polarisé $[\Theta \mid \Delta \mid \Gamma]$, partitionnant les variables en trois ensembles basés sur leur variance :

• $\Theta$ (Négatif) : Variables apparaissant uniquement dans des positions contravariantes.
• $\Gamma$ (Positif) : Variables apparaissant uniquement dans des positions covariantes.
• $\Delta$ (Dinaturel) : Variables apparaissant dans les deux positions (ou autorisées à être traitées comme telles).

Les caractéristiques syntaxiques clés incluent :

• Égalité Dirigée ($\le_A$) : Une relation primitive $s \le_A t$ où $s$ est typée dans le contexte négatif et $t$ dans le contexte positif.
• Implication Polarisée : L'implication $\psi \Rightarrow \phi$ inverse la polarité du contexte pour $\psi$ (la déplaçant de la gauche vers la droite du séquent), reflétant la contravariance du premier argument.
• Quantificateurs Polarisés : Les quantificateurs ($\forall^p, \exists^p$) sont indexés par une polarité $p \in \{-, \Delta, +\}$ pour suivre la variance de la variable liée.
• Règles de Substitution : Un mécanisme de substitution spécialisé (Définition 2.7) gère le réindexage des termes à travers les contextes polarisés, garantissant que les variables dinaturelles sont substituées de manière cohérente.

Sémantique : Doctrines Dirigées

La sémantique est capturée via les doctrines dirigées, une généralisation des doctrines de Lawvere.

• Catégorie de Base : Au lieu d'une catégorie standard de types, la base est une catégorie de polarisation $ndp(\mathcal{C})$, dont les objets sont des triplets $(\Theta, \Delta, \Gamma)$ et dont les morphismes respectent la structure de variance.
• Structure Fibrée : Un foncteur $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ mappe les contextes polarisés vers des ensembles partiellement ordonnés de formules.
• Conditions Clés :
  • Absence de Variance Dinaturelle (ndv) : Une condition garantissant que les variables dinaturelles dans les prédicats proviennent uniquement de l'effondrement de variables positives et négatives, empêchant l'émergence de « troisième » types de variance.
  • Adjonctions Relatives : L'égalité dirigée est caractérisée non pas comme un adjoint à gauche standard, mais comme un adjoint à gauche relatif à une opération de type contraction qui effondre deux variables de polarité opposée en une seule variable dinaturelle. Cela capture la restriction syntaxique empêchant la dérivation de la symétrie.
  • Implication Polarisée : Caractérisée comme un coadjoint relatif.

3. Contributions Clés

1. Syntaxe de la dFOL : Un système de déduction naturelle précis pour la logique du premier ordre avec égalité dirigée, doté d'un système rigoureux de polarités inspiré par la dinaturalité. Ce système interdit explicitement la dérivation de la symétrie pour l'égalité dirigée tout en maintenant les connecteurs logiques standard.
2. Caractérisation de l'Égalité Dirigée : L'article généralise l'« égalité comme adjoint à gauche » de Lawvere en égalité dirigée comme adjoint à gauche relatif. Cela fournit une propriété universelle catégorielle précise pour l'égalité dirigée qui prend en compte l'asymétrie de la relation.
3. Doctrines Dirigées : L'introduction des doctrines dirigées comme cadre sémantique. Les auteurs prouvent que la syntaxe de la dFOL est saine et complète par rapport à cette sémantique.
4. Complétude pour les Préordres : Un résultat de complétude spécifique est prouvé pour le fragment classique de la dFOL par rapport au modèle standard des préordres ($\mathbf{Preord}$). Cela établit que toute conséquence valide dans tous les modèles de préordres est dérivable dans la syntaxe.
5. Gestion de la Polarité : L'article démontre comment gérer la variance dans un cadre sans pertinence des preuves, le distinguant des théories des types dirigées avec pertinence des preuves (comme celles dans $\mathbf{Cat}$) en utilisant des fibrations en ensembles partiellement ordonnés et des fibres à valeurs en ensembles partiellement ordonnés.

4. Résultats

• Santé et Complétude : Les auteurs établissent une bi-adjonction entre la catégorie des théories ($\mathbf{Theory}$) et la 2-catégorie des doctrines dirigées ($\mathbf{DDoctrine}$). Cela implique que la dFOL est le langage interne des doctrines dirigées.
• Complétude pour les Préordres : En utilisant une construction de type Henkin adaptée aux contextes polarisés, l'article prouve que le fragment classique de la dFOL est complet par rapport au modèle des préordres. La construction définit le domaine du modèle comme l'ensemble des termes clos ordonnés par la dérivation de l'égalité dirigée ($\le_A$).
• Règles Dérivées : Le système supporte des règles dérivées pour la transitivité, la réflexivité et la congruence de l'égalité dirigée, ainsi que des règles d'interaction entre les quantificateurs polarisés et l'implication.
• Contre-exemples : L'article illustre que la symétrie ($a \le b \vdash b \le a$) n'est pas dérivable, et le modèle de préordre sert de contre-modèle pour de telles dérivations.

5. Importance et Revendications

L'article revendique faire progresser les travaux de Lawvere sur le rôle de la variance et des foncteurs hom en logique. Plus précisément :

• Il fournit une caractérisation syntaxique et sémantique précise de l'égalité dirigée dans un cadre sans pertinence des preuves, comblant un vide entre la logique classique et la théorie des types dirigée.
• Il généralise le concept d'égalité comme adjoint au cas dirigé via des adjonctions relatives, offrant un nouvel outil catégoriel pour comprendre les structures dirigées.
• Il démontre que la logique dirigée peut être traitée avec des techniques logiques standard (comme la complétude de Henkin) en gérant soigneusement les polarités via des contextes polarisés, plutôt que d'exiger des machineries géométriques complexes ou de haute catégorie.
• Le travail est positionné comme une étape fondamentale pour le raisonnement sur les systèmes de réécriture et les phénomènes dirigés (processus, transitions) au sein d'un cadre logique, distinct des approches avec pertinence des preuves de la Théorie des Types Homotopique.

Les auteurs déclarent explicitement que leur focus porte sur le cas sans pertinence des preuves, justifié par la nature de la logique de réécriture (où une réécriture se produit ou non) et l'utilisation de fibrations en ensembles partiellement ordonnés en logique catégorielle. Ils ne revendiquent pas résoudre la pleine complexité de la théorie des types dirigée dépendante, mais fournissent une base robuste pour le cas du premier ordre basé sur les préordres.