The proof theory and semantics of second-order (intuitionistic) tense logic

Sintesi Tecnica: La Teoria della Dimostrazione e la Semantica della Logica del Tempo del Secondo Ordine (Intuitivista)

Problema e Motivazione
Il saggio affronta lo sviluppo fondazionale della logica del tempo del secondo ordine sia su basi classiche che intuitiviste. Sebbene la logica del secondo ordine sia uno strumento standard nella logica matematica e computazionale, le sue fondamenta metalogiche, in particolare per quanto riguarda la teoria della dimostrazione e la semantica, hanno posto sfide significative. Una difficoltà specifica nella logica modale intuitivista è la mancanza di consenso sulla corretta assiomatizzazione della modalità diamante ($\Diamond$), che non può essere definita in termini di box ($\Box$) come avviene nella logica classica. Esistono varie proposte (ad esempio, CK, IK), ma spesso comportano scelte arbitrarie di assiomi.

Gli autori propongono un approccio unificato utilizzando la quantificazione del secondo ordine. Un'osservazione chiave è che nella logica del secondo ordine intuitivista, i connettivi positivi possono essere definiti a partire dal frammento negativo. Nello specifico, il saggio dimostra che la modalità diamante (e la sua teoria associata) può essere recuperata utilizzando solo i box ($\Box$) e i backward box ($\blacksure$), a condizione che siano incluse sia le modalità in avanti che quelle all'indietro (logica del tempo). Ciò consente una definizione di $\Diamond A$ come $\forall X(\Box(A \to \blacksquare X) \to X)$, evitando assiomatizzazioni arbitrarie.

Metodologia
Gli autori sviluppano tre definizioni parallele per la logica del tempo del secondo ordine:

1. Assiomatica: I sistemi $Kt2$ (classico) e $IKt2$ (intuitivista) vengono definiti. Essi estendono la logica proposizionale del secondo ordine con modalità normali e assiomi di aggiunzione per coppie temporali. Fondamentalmente, includono un pieno assioma di comprensione, consentendo definizioni impredicative.
2. Semantica: Il saggio introduce la semantica (bi)relazionale per il caso intuitivista e la semantica relazionale per il caso classico. Queste strutture includono un ordine parziale (per l'intuizionismo) e una relazione di accessibilità. Una caratteristica centrale è il requisito di "comprensività", in cui il dominio degli insiemi include le estensioni di tutte le formule, modellando efficacementmente l'assioma di comprensione. Gli autori definiscono inoltre le "strutture di predicati" (dove i mondi sono modelli modali classici) e ne dimostrano l'equivalenza con le strutture birelazionali.
3. Teoria della Dimostrazione: Vengono proposti i calcoli a sequenti etichettati ($\ell Kt2$ e $\ell IKt2$). Questi sistemi utilizzano etichette di mondo e atomi relazionali per interiorizzare la semantica. Per il caso intuitivista, viene introdotto un calcolo multi-succedente intermedio ($m\ell IKt2$) per facilitare gli argomenti di ricerca della dimostrazione, il quale si dimostra essere conservativo rispetto alla versione a singolo antecedente.

La strategia tecnica centrale consiste nel dimostrare che queste tre definizioni coincidano. Ciò è visualizzato come "grandi tour" che collegano la dimostrabilità assiomatica, la validità semantica e la derivabilità teorica della dimostrazione. Le dimostrazioni di completezza si basano su un argomento di ricerca della dimostrazione adattato dalla nozione di semi-valutazioni di Schütte e dal concetto di valori possibili di Prawitz, superando gli ostacoli dell'impredicatività.

Contributi Chiave e Risultati

• Definizione dei Diamanti tramite Quantificazione del Secondo Ordine: Il saggio stabilisce che, in presenza di modalità temporali, la modalità diamante è definibile nella logica del secondo ordine intuitivista come $\Diamond A \iff \forall X(\Box(A \to \blacksquare X) \to X)$. Questo recupera la teoria di Fischer Servi e la $IK$ di Simpson e la $IKt$ di Ewald senza scelte arbitrarie di assiomi.
• Correttezza e Completezza:
  • Intuitivista: Il sistema $IKt2$ è dimostrato corretto e completo rispetto alla semantica birelazionale comprensiva (Teorema Principale 3.3).
  • Classica: Il sistema $Kt2$ è dimostrato corretto e completo rispetto alla semantica relazionale comprensiva (Teorema Principale 3.14).
• Eliminazione del Taglio (Cut-Admissibility): Il saggio stabilisce l'ammissibilità del taglio per i calcoli a sequenti etichettati $\ell Kt2$ e $\ell IKt2$ (Teorema Principale 4.2). Ciò viene ottenuto tramite un argomento di ricerca della dimostrazione che costruisce contromodelli da ricerche di dimostrazione fallite.
  • Per il caso classico, l'argomento adatta le semi-valutazioni di Schütte e i valori possibili di Prawitz per estrarre un contromodello relazionale.
  • Per il caso intuitivista, l'argomento è più complesso, richiedendo la costruzione di un albero di ricerca della dimostrazione (anziché un ramo) per gestire l'ordine parziale dei modelli di Kripke, producendo infine un contromodello di struttura di predicati.
• Correttezza Assiomatica delle Dimostrazioni Etichettate: Il saggio fornisce una traduzione dalle dimostrazioni etichettate alle dimostrazioni assiomatiche (Teorema 7.1), completando il ciclo di equivalenze. Ciò comporta l'interpretazione dei sequenti a politree etichettati come formule temporali e la dimostrazione che ogni regola di inferenza corrisponde a una regola ammissibile nel sistema assiomatico.
• Relazione Classica-Intuitivista: Il saggio stabilisce che la logica del tempo del secondo ordine classica ($Kt2$) può essere incorporata nel sistema intuitivista ($IKt2$) tramite una traduzione negativa (Teorema 8.2), similmente alla traduzione di Gödel-Gentzen.

Significatività
Il saggio sostiene di fornire una base robusta e unificata per la logica del tempo del secondo ordine. Dimostrando che le definizioni assiomatica, semantica e della teoria della dimostrazione coincidono, esso valida la scelta della minimalizzazione assiomatica. Il lavoro affronta la specifica sfida di definire le modalità positive in un contesto intuitivista senza assiomi arbitrari, sfruttando il potere espressivo della quantificazione del secondo ordine.

La metodologia è presentata come applicabile sia all'ambiente classico che a quello intuitivista, dove il caso intuitivista richiede nuovi adattamenti tecnici per gestire l'impredicatività e la struttura dei modelli di Kripke. I risultati sono significativi per lo studio metalogico delle logiche modali, offrendo un account completo della teoria della dimostrazione (inclusa l'eliminazione del taglio) per la logica del tempo del secondo ordine, un dominio in cui tali risultati erano precedentemente assenti o limitati alla piena semantica (che non è ricorsivamente enumerabile). Il saggio si posiziona come un contributo agli strumenti teorici necessari per l'adozione della logica modale del secondo ordine in aree come la rappresentazione della conoscenza e l'intelligenza artificiale, come notato in lavori correlati.