Uniform Realizability Interpretations

1. Il Problema

La realizzazione (realizability) è una tecnica fondamentale nella logica intuizionistica e nella teoria dei tipi per assegnare significato computazionale alle dimostrazioni. Tuttavia, esistono molte varianti di interpretazioni di realizzazione (es. realizzazione di Kleene, realizzazione modificata di Kreisel, realizzazione di Herbrand, realizzazione classica, realizzazione "learning" di Aschieri-Berardi) che trattano i quantificatori in modi diversi e spesso non uniformi.

Il problema centrale identificato dagli autori è la frammentazione di queste interpretazioni:

• Trattamento non uniforme: Nella realizzazione classica di Kleene, un realizzatore per $\exists n A(n)$ deve fornire esplicitamente un numero $k$ (il testimone) e un realizzatore per $A(k)$.
• Trattamento uniforme: In approcci più recenti (come la realizzazione di Herbrand o quella uniforme di Heyting), i quantificatori sono trattati "uniformemente": un realizzatore per $\exists n A(n)$ non fornisce esplicitamente $n$, ma è una funzione che funziona per tutti gli $n$ (o esiste un $n$ tale che la condizione è soddisfatta, senza estrarre $n$ nel realizzatore stesso).
• Mancanza di unificazione: Non esiste un quadro teorico unificato che mostri come queste diverse interpretazioni siano casi particolari di una struttura più generale, specialmente riguardo al trattamento delle formule atomiche e dei quantificatori.

2. Metodologia

Gli autori propongono un nuovo quadro concettuale chiamato Realizzabilità Uniforme (Uniform Realizability). La metodologia si basa su una definizione parametrica che separa la logica dei quantificatori dall'interpretazione dei predicati atomici.

• Distinzione tra Quantificatori: Si distingue tra quantificatori non qualificati (o uniformi) $\exists x A(x)$ e $\forall x A(x)$, e quantificatori qualificati (tipizzati) $\exists^B x A(x)$ e $\forall^B x A(x)$. Gli autori propongono di interpretare sempre i quantificatori non qualificati in modo uniforme, mentre quelli qualificati sono trattati come abbreviazioni logiche (es. $\forall^B x A(x) \equiv \forall x (B(x) \to A(x))$).
• Interpretazione di Base (Base Interpretation): L'interpretazione è parametrizzata da una "interpretazione di base" che mappa i predicati atomici della teoria sorgente $S$ (es. Aritmetica di Heyting, HA) in relazioni della teoria target $T$.
  • Per un predicato $P(x)$, si definisce una relazione $x \triangleright_P a$, dove $a$ è la tupla di realizzatori che "limita" o "witnessa" $P(x)$.
  • Questa relazione può essere uniforme (se $a$ è la tupla vuota $\langle\rangle$) o non uniforme (se $a$ contiene dati specifici).
• Definizione Induttiva: L'interpretazione di realizzazione uniforme ($a \text{ ur } A$) è definita induttivamente:
  • Atomiche: $a \text{ ur } P(x) \iff x \triangleright_P a$.
  • Connettivi: Standard (es. $A \to B$ richiede una funzione che mappa realizzatori di $A$ in realizzatori di $B$).
  • Quantificatori (Uniformi):
    • $a \text{ ur } \exists x A(x) \iff \exists x (a \text{ ur } A(x))$ (Il realizzatore non cambia, ma l'esistenza è interna alla teoria target).
    • $a \text{ ur } \forall x A(x) \iff \forall x (a \text{ ur } A(x))$ (Lo stesso realizzatore $a$ deve funzionare per ogni $x$).
• Teorema di Correttezza (Soundness): Viene dimostrato che se gli assiomi non logici della teoria sorgente sono realizzabili rispetto all'interpretazione di base scelta, allora tutti i teoremi della teoria sono realizzabili.

3. Contributi Chiave

1. Unificazione Teorica: Il lavoro dimostra che interpretazioni apparentemente diverse (Kleene, Kreisel, Herbrand, Classica, Learning) sono tutte istanze dello stesso schema di realizzabilità uniforme, differenziandosi solo nella scelta dell'interpretazione di base per i predicati atomici ($=$, $\bot$, $N(n)$).
2. Parametrizzazione dei Predicati Atomici:
   • Uguaglianza ($=$): Può essere interpretata uniformemente ($n=m$) o in modo non banale (es. $\phi(a) \to n=m$ nella realizzazione "learning").
   • Falsità ($\bot$): Può essere interpretata come sempre falsa (Kleene) o come un predicato unario $\psi(a)$ che fornisce contenuto computazionale (realizzazione classica e learning).
   • Numeri Naturali ($N(n)$): Può essere interpretata come:
     • Uniforme: $N(n)$ è sempre vero (realizzazione di Herbrand interna).
     • Approssimata: $a$ è un insieme finito contenente $n$ o un limite superiore (realizzazione di Lifschitz o modificata limitata).
     • Precisa: $a$ è esattamente $n$ (Kleene, Kreisel).
3. Gestione dell'Induzione: Il paper analizza come l'induzione venga realizzata in base all'interpretazione di $N(n)$. In particolare, per interpretazioni approssimate (es. $n \le a$), viene introdotta una struttura di ordine parziale e un'operazione di "unione" ($\cup$) per costruire realizzatori che funzionino uniformemente su tutti gli $n$ limitati da $a$.
4. Estensione a Logiche Classiche: Il framework permette di incorporare la realizzazione classica (tramite la traduzione di Friedman-Dragalin) e la realizzazione "learning" di Aschieri-Berardi, mostrando come la gestione dello stato di conoscenza e l'aggiornamento dei realizzatori emergano naturalmente dall'interpretazione di base di $\bot$ e $=$.

4. Risultati

• Teorema di Correttezza Generale (Teorema 2.7): È stato dimostrato che la realizzazione uniforme è corretta per qualsiasi teoria $S$ i cui assiomi non logici siano realizzabili rispetto all'interpretazione di base scelta. Questo riduce il lavoro di verifica della correttezza di una nuova interpretazione alla semplice verifica degli assiomi atomici.
• Ricostruzione delle Interpretazioni Esistenti:
  • Kleene: Recuperata con $N(n)$ interpretata come $n=a$ e $\bot$ come falso.
  • Kreisel (Modificata): Recuperata con realizzatori totali (funzionalità primitive ricorsive) e tipi finiti.
  • Herbrand: Recuperata con $N(n)$ uniforme (sempre vero) e $st(n)$ (numeri standard) interpretata come appartenenza a un insieme finito $S$.
  • Classica: Recuperata assegnando contenuto computazionale a $\bot$ tramite un predicato $P(a)$.
  • Learning (Aschieri-Berardi): Recuperata introducendo uno stato $s$ e interpretando $\bot$ come "lo stato cambia" ($\gamma(s) \neq s$), permettendo l'interpretazione della legge del terzo escluso per formule $\Sigma^0_1$.
• Proprietà di Indipendenza della Premessa: Viene mostrato come il framework supporti naturalmente schemi come l'Indipendenza della Premessa, specialmente nelle varianti modificata e classica.

5. Significato

L'articolo ha un impatto significativo sulla teoria della dimostrazione e sulla semantica computazionale:

• Semplificazione e Generalizzazione: Fornisce un linguaggio comune per confrontare e combinare diverse tecniche di realizzazione, eliminando la necessità di ridefinire l'intera semantica ogni volta che si cambia l'interpretazione dei quantificatori.
• Flessibilità nella Progettazione: Permette ai ricercatori di progettare nuove interpretazioni di realizzazione semplicemente scegliendo un'interpretazione di base appropriata per i predicati atomici, senza dover riscrivere le regole per i quantificatori.
• Connessione tra Logica Intuizionistica e Classica: Il framework chiarisce come le interpretazioni che estraggono contenuto computazionale da dimostrazioni classiche (tramite negazione doppia o stati di apprendimento) siano strutturalmente simili a quelle intuizionistiche, differendo solo nel trattamento dei predicati atomici fondamentali.
• Implicazioni per la Teoria dei Tipi: Il concetto di quantificatori uniformi si collega direttamente a concetti avanzati nella teoria dei tipi, come i tipi di intersezione e le interpretazioni funzionali uniformi, offrendo nuove prospettive per l'estrazione di programmi da prove formali.

In sintesi, Berger e Oliva offrono una "teoria delle teorie" per la realizzazione, dimostrando che la diversità delle interpretazioni esistenti è una questione di scelta dei parametri atomici, non di differenze strutturali profonde nella logica dei quantificatori.