Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

Riepilogo Tecnico: Quattro Paradossi e un Assistente di Dimostrazione

Enunciato del Problema
Il lavoro affronta i confini fondazionali del Calcolo delle Costruzioni Induttive (CIC), la teoria dei tipi alla base dell'assistente di dimostrazione Rocq (già Coq). Sebbene la consistenza del CIC sia ben consolidata, le specifiche decisioni progettuali che prevengono l'inconsistenza — in particolare riguardo all'impredicatività, ai vincoli sugli universi e all'eliminazione grande — sono spesso trattate come vincoli ingegneristici astratti. La libreria coq-paradoxes, distribuita con Rocq, contiene quattro derivazioni meccanizzate di False (Burali-Forti, Diaconescu, Reynolds e Hurkens) che dipendono da ipotesi rifiutate dal kernel di Rocq. Il problema centrale è interpretare queste derivazioni non meramente come curiosità storiche o inconsistenze isolate, ma come una "specificazione negativa" che delinea con precisione dove il kernel deve tracciare i propri limiti per mantenere la correttezza.

Metodologia
Il lavoro impiega una lettura attenta del codice sorgente all'interno della libreria coq-paradoxes, analizzando specificamente quattro file: BuraliForti.v, diaconescu.v, Reynolds.v e Hurkens_Set.v. La metodologia prevede:

1. Decostruzione della Macchina Condivisa: Analisi di Logics.v per comprendere il predicato di accessibilità (ACC) e l'infrastruttura di buon fondamento utilizzata da più paradossi.
2. Tracciamento delle Derivazioni: Seguire i passaggi logici in ciascun file per identificare l'ipotesi specifica (ad esempio, un tipo universale di relazioni, un principio di scelta o un'iniezione da Prop a una singola proposizione) che porta a una contraddizione.
3. Mappatura sui Rifiuti del Kernel: Correlare il punto di contraddizione nella formalizzazione con il meccanismo specifico nel kernel di Rocq (aritmetica degli universi, regole di eliminazione o controlli di predicatività) che impedisce la compilazione della costruzione.
4. Sintesi delle Decisioni Progettuali: Aggregare i risultati per estrarre tre condizioni al contorno unificate che governano il comportamento del kernel.

Contributi e Risultati Chiave

Il lavoro analizza quattro paradossi specifici, dimostrando come ciascuno esponga una vulnerabilità distinta nella teoria dei tipi se certe scelte progettuali venissero alterate:

1. Paradosso di Burali-Forti (BuraliForti.v):

   • Meccanismo: Assume un tipo universale di relazioni $A_0$ e un'iniezione $i_0$ che mappa le relazioni negli elementi di $A_0$. Ciò permette la costruzione di un "ordinale di tutti gli ordinali" ($\Omega$) che è immerso in se stesso.
   • Rifiuto del Kernel: Il paradosso si basa sull'istanziare $A_0$ con se stesso. Il kernel di Rocq impone una rigorosa stratificazione degli universi ($Type_j < Type_i$) per impedire che un tipo contenga la propria immagine. La costruzione innesca un errore di "Inconsistenza degli Universi" perché il livello dell'universo richiesto per il tipo interno deve essere almeno grande quanto quello del tipo esterno, violando i vincoli cumulativi del kernel.
   • Risultato: Stabilisce la necessità di vincoli sulla gerarchia degli universi per prevenire definizioni di tipi auto-referenziali che portano a contraddizioni di punto fisso.

2. Paradosso di Diaconescu (diaconescu.v):

   • Meccanismo: Utilizza una versione tipizzata dell'Assioma della Scelta (Tchoice) su una relazione di equivalenza su bool definita da una proposizione $P$. La funzione di scelta $f: bool \to bool$ è utilizzata per decidere $P$ confrontando $f(\text{true})$ e $f(\text{false})$.
   • Rifiuto del Kernel: L'argomento estrae una decisione computazionale (una funzione in Set) da una prova esistenziale in Prop. Ciò costituisce un'"eliminazione grande" da Prop a Set.
   • Risultato: Dimostra che permettere l'Assioma della Scelta in Set (o l'eliminazione grande da Prop a Set) forza la Legge del Terzo Escluso (LEM) all'interno del sistema costruttivo. Il kernel limita l'eliminazione grande per prevenire questa importazione della logica classica nel livello computazionale.

3. Paradosso di Reynolds (Reynolds.v):

   • Meccanismo: Riformula il risultato di Reynolds secondo cui il Sistema F non ha un modello insiemistico. Assume un'iniezione $I: Prop \to Heyt$ (dove $Heyt$ è una singola proposizione) e costruisce un'algebra pre-iniziale (codifica di Church) per un funtore $\Phi$. Utilizzando il teorema del punto fisso di Lawvere, deriva un punto fisso per la negazione, portando a False.
   • Rifiuto del Kernel: La costruzione si basa sull'impredicatività di Prop (quantificazione su tutte le proposizioni all'interno di Prop). Tuttavia, il paradosso richiede un'iniezione da Prop a una singola proposizione, che il kernel rifiuta per motivi di universo prima che la contraddizione logica possa essere raggiunta.
   • Risultato: Evidenzia il ruolo dell'impredicatività in Prop. Sebbene Prop sia impredicativo, il kernel impedisce le specifiche iniezioni strutturali che permetterebbero all'argomento diagonale di Cantor di collassare l'universo delle proposizioni.

4. Paradosso di Hurkens (Hurkens_Set.v):

   • Meccanismo: Un adattamento della semplificazione di Hurkens del paradosso di Girard. Assume una retrazione tra Prop e bool (tramite doppia negazione) e utilizza l'impredicatività di Set (se abilitata) combinata con l'eliminazione grande per costruire una relazione ben fondata auto-referenziale che porta a False.
   • Rifiuto del Kernel: Il paradosso richiede sia impredicatività in Set che eliminazione grande (estrazione di booleani dal contenuto proposizionale). Il kernel predefinito di Rocq mantiene Set predicativo e limita l'eliminazione grande da Prop.
   • Risultato: Mostra che la combinazione di impredicatività ed eliminazione grande in Set è incompatibile con la logica classica (LEM). La decisione del kernel di mantenere Set predicativo e limitare l'eliminazione è la salvaguardia.

Significato e Affermazioni

Il lavoro sostiene che il pacchetto coq-paradoxes funge da specificazione negativa del kernel di Rocq. Piuttosto che elencare semplicemente inconsistenze, il pacchetto fornisce una prova formale per mezzo di esempi falliti della correttezza del kernel.

• Tre Condizioni al Contorno: Il lavoro sintetizza i quattro paradossi in tre specifiche decisioni progettuali imposte dal kernel:

  1. Gerarchia degli Universi: Impedisce ai tipi di quantificare su se stessi in modo da creare punti fissi (Burali-Forti).
  2. Posizionamento dell'Impredicatività: Confina la quantificazione impredicativa a Prop (e opzionalmente a Set con cautela), prevenendo le contraddizioni di Reynolds e Hurkens.
  3. Disciplina dell'Eliminazione Grande: Limita l'estrazione di contenuto computazionale (come bool o funzioni in Set) dalle prove proposizionali, prevenendo le contraddizioni di Diaconescu e Hurkens.

• Ruolo Meta-Matematico: Il lavoro afferma che il pacchetto è un pezzo unico di meta-matematica scritto all'interno del sistema che documenta. Non dimostra teoremi per l'applicazione, ma dimostra l'insoddisfacibilità di ipotesi specifiche. Il "rifiuto" del kernel è mostrato come una conseguenza di politiche uniformi (aritmetica degli universi, regole di eliminazione) piuttosto che di soluzioni ad hoc.

• Conclusione: Il significato risiede nel dimostrare che il rifiuto del kernel di Rocq di compilare queste costruzioni non è arbitrario, ma è il preciso meccanismo strutturale richiesto per mantenere la consistenza del CIC. Il pacchetto convalida che le decisioni progettuali del kernel sono prese per le "ragioni giuste", disegnando efficacemente il confine del sistema dall'esterno verso l'interno.