Riepilogo Tecnico: Semantica Dottrinale della Logica del Primo Ordine Diretta

1. Enunciato del Problema

Il lavoro affronta la sfida di formalizzare l'uguaglianza diretta all'interno di un quadro logico. Mentre la prospettiva categorica di Lawvere ha caratterizzato con successo l'uguaglianza classica come un aggiunto sinistro alla contrazione, questo approccio si basa sulla simmetria. Nella teoria dei tipi diretta, dove i tipi sono interpretati come categorie (o preordini) piuttosto che come groupoidi (o insiemi), l'uguaglianza diventa una relazione asimmetrica (ad esempio, una riscrittura $a \to b$ o un ordine $a \le b$).

La difficoltà fondamentale risiede nella gestione della varianza (polarità). In un contesto diretto, una variabile può apparire in una posizione "negativa" (controvariente, ad esempio la sorgente di un morfismo) o in una posizione "positiva" (covariante, ad esempio il target). Le regole logiche standard per l'uguaglianza (riflessività e la regola J/eliminazione) falliscono in questo contesto perché assumono implicitamente la simmetria o permettono alle variabili di apparire in entrambe le polarità simultaneamente in modi che porterebbero a derivare la simmetria ($a \le b \vdash b \le a$), il che è invalido nella logica diretta. I precedenti tentativi di teoria dei tipi diretta spesso faticano con questi vincoli di polarità, in particolare nel contesto della logica irrilevante per le prove (dove l'uguaglianza è una proposizione, non un tipo con più abitanti).

2. Metodologia

Gli autori sviluppano una logica del primo ordine diretta (dFOL) e la sua semantica dottrinale generalizzando il quadro delle iperdottrine di Lawvere.

Sintassi: Contesti Polarizzati

La sintassi introduce un contesto polarizzato $[\Theta \mid \Delta \mid \Gamma]$, partizionando le variabili in tre insiemi in base alla loro varianza:

• $\Theta$ (Negativo): Variabili che appaiono solo in posizioni controvarianti.
• $\Gamma$ (Positivo): Variabili che appaiono solo in posizioni covarianti.
• $\Delta$ (Dinaturale): Variabili che appaiono in entrambe le posizioni (o che sono ammesse come tali).

Le caratteristiche sintattiche chiave includono:

• Uguaglianza Diretta ($\le_A$): Una relazione primitiva $s \le_A t$ dove $s$ è tipata nel contesto negativo e $t$ nel contesto positivo.
• Implicazione Polarizzata: L'implicazione $\psi \Rightarrow \phi$ scambia la polarità del contesto per $\psi$ (spostandolo da sinistra a destra del trattino verticale), riflettendo la controvarianza del primo argomento.
• Quantificatori Polarizzati: I quantificatori ($\forall^p, \exists^p$) sono indicizzati per polarità $p \in \{-, \Delta, +\}$ per tracciare la varianza della variabile vincolata.
• Regole di Sostituzione: Un meccanismo di sostituzione specializzato (Definizione 2.7) gestisce il reindicizzazione dei termini attraverso contesti polarizzati, garantendo che le variabili dinaturali siano sostituite in modo coerente.

Semantica: Dottrine Dirette

La semantica è catturata tramite dottrine dirette, una generalizzazione delle dottrine di Lawvere.

• Categoria Base: Invece di una categoria standard di tipi, la base è una categoria di polarizzazione $ndp(\mathcal{C})$, i cui oggetti sono terne $(\Theta, \Delta, \Gamma)$ e i morfismi rispettano la struttura di varianza.
• Struttura Fibrata: Un funtore $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ mappa i contesti polarizzati in poset di formule.
• Condizioni Chiave:
  • No-Dinatural-Variance (ndv): Una condizione che garantisce che le variabili dinaturali nei predicati sorgano solo dal collasso di variabili positive e negative, prevenendo tipi "terzi" di varianza.
  • Addotti Relativi: L'uguaglianza diretta è caratterizzata non come un aggiunto sinistro standard, ma come un aggiunto sinistro relativo a un'operazione simile alla contrazione che collassa due variabili di polarità opposta in una singola variabile dinaturale. Questo cattura la restrizione sintattica che impedisce di derivare la simmetria.
  • Implicazione Polarizzata: Caratterizzata come un coaggiunto relativo.

3. Contributi Chiave

1. Sintassi della dFOL: Un sistema di deduzione naturale preciso per la logica del primo ordine con uguaglianza diretta, dotato di un rigoroso sistema di polarità ispirato alla dinaturalità. Questo sistema vieta esplicitamente la derivazione della simmetria per l'uguaglianza diretta, mantenendo al contempo i connettivi logici standard.
2. Caratterizzazione dell'Uguaglianza Diretta: Il lavoro generalizza l'"uguaglianza come aggiunto sinistro" di Lawvere all'uguaglianza diretta come aggiunto sinistro relativo. Ciò fornisce una precisa proprietà universale categorica per l'uguaglianza diretta che tiene conto dell'asimmetria della relazione.
3. Dottrine Dirette: L'introduzione delle dottrine dirette come quadro semantico. Gli autori dimostrano che la sintassi della dFOL è corretta e completa rispetto a questa semantica.
4. Completezza per Preordini: Viene dimostrato un risultato specifico di completezza per il frammento classico della dFOL rispetto al modello standard dei preordini ($\mathbf{Preord}$). Ciò stabilisce che qualsiasi conseguenza valida in tutti i modelli di preordini è derivabile nella sintassi.
5. Gestione della Polarità: Il lavoro dimostra come gestire la varianza in un contesto irrilevante per le prove, distinguendolo dalle teorie dei tipi dirette rilevanti per le prove (come quelle in $\mathbf{Cat}$) utilizzando fibrati posetali e fibre a valori posetali.

4. Risultati

• Correttezza e Completezza: Gli autori stabiliscono una bi-addizione tra la categoria delle teorie ($\mathbf{Theory}$) e la 2-categoria delle dottrine dirette ($\mathbf{DDoctrine}$). Ciò implica che la dFOL è il linguaggio interno delle dottrine dirette.
• Completezza per i Preordini: Utilizzando una costruzione di tipo Henkin adattata per contesti polarizzati, il lavoro dimostra che il frammento classico della dFOL è completo rispetto al modello dei preordini. La costruzione definisce il dominio del modello come l'insieme dei termini chiusi ordinati dalla derivabilità dell'uguaglianza diretta ($\le_A$).
• Regole Derivate: Il sistema supporta regole derivate per transitività, riflessività e congruenza dell'uguaglianza diretta, nonché regole di interazione tra quantificatori polarizzati e implicazione.
• Controesempi: Il lavoro illustra che la simmetria ($a \le b \vdash b \le a$) non è derivabile, e il modello di preordini funge da contromodello per tali derivazioni.

5. Significato e Affermazioni

Il lavoro afferma di avanzare il lavoro di Lawvere sul ruolo della varianza e dei funtori hom nella logica. Nello specifico:

• Fornisce una caratterizzazione sintattica e semantica precisa dell'uguaglianza diretta in un contesto irrilevante per le prove, colmando un vuoto tra la logica classica e la teoria dei tipi diretta.
• Generalizza il concetto di uguaglianza come aggiunto al caso diretto tramite addotti relativi, offrendo un nuovo strumento categorico per comprendere le strutture dirette.
• Dimostra che la logica diretta può essere trattata con tecniche logiche standard (come la completezza di Henkin) gestendo attentamente le polarità attraverso contesti polarizzati, piuttosto che richiedere complesse macchine geometriche o di categoria superiore.
• Il lavoro è posizionato come un passo fondazionale per il ragionamento sui sistemi di riscrittura e sui fenomeni diretti (processi, transizioni) all'interno di un quadro logico, distinto dagli approcci rilevanti per le prove della Teoria dei Tipi Omotopica.

Gli autori dichiarano esplicitamente che il loro focus è sul caso irrilevante per le prove, giustificato dalla natura della logica di riscrittura (dove una riscrittura avviene o non avviene) e dall'uso di fibrati posetali nella logica categorica. Non affermano di risolvere la piena complessità della teoria dei tipi diretta dipendente, ma forniscono una solida fondazione per il caso del primo ordine basato su preordini.