Uniform Realizability Interpretations

Resumen Técnico: Interpretaciones de Realizabilidad Uniforme

1. El Problema

La realizabilidad es una semántica para la lógica intuicionista que asocia fórmulas con "testigos" computacionales (realizadores). Históricamente, existen diversas variantes de realizabilidad (Kleene, Kreisel, Herbrand, realizabilidad clásica, etc.) que difieren fundamentalmente en cómo tratan los cuantificadores y las fórmulas atómicas:

• Enfoque Tradicional (ej. Realizabilidad de Kleene): Los realizadores para cuantificadores existenciales ($\exists n A(n)$) deben proporcionar explícitamente el testigo $n$ (el número). Los realizadores para cuantificadores universales ($\forall n A(n)$) son funciones que, dado un $n$, producen un realizador para $A(n)$.
• Enfoques Modernos (ej. Realizabilidad de Herbrand, Realizabilidad Uniforme de Heyting, Realizabilidad de Aprendizaje): En estos sistemas, los cuantificadores se tratan de manera uniforme. Un realizador para $\exists n A(n)$ no necesariamente contiene $n$ explícitamente, sino que garantiza la existencia de un $n$ tal que el realizador funciona para él. De igual forma, un realizador para $\forall n A(n)$ es el mismo objeto que funciona uniformemente para todo $n$, sin depender de una entrada específica de $n$ en su estructura interna.

El problema central abordado por los autores es la falta de un marco unificado que explique la relación entre estas variantes. Cada sistema suele definirse ad-hoc, dificultando la comparación sistemática y la generalización de propiedades como la corrección (soundness).

2. Metodología

Los autores proponen un marco general llamado Realizabilidad Uniforme. La metodología se basa en separar la interpretación de los cuantificadores de la interpretación de las fórmulas atómicas.

• Interpretación Base: Se define una interpretación paramétrica de los predicados atómicos de una teoría fuente $S$ (como la Aritmética de Heyting, HA) hacia una teoría objetivo $T$. Esta base asigna a cada predicado $P$ una relación $x \triangleright_P a$, donde $x$ es la tupla de argumentos y $a$ es el realizador (o testigo) de $P(x)$.
• Interpretación Uniforme de Cuantificadores: Se introduce una definición inductiva donde los cuantificadores no se "desencriptan" en los realizadores, sino que se interpretan uniformemente:
  • $a \text{ ur } \exists x A(x) \iff \exists x (a \text{ ur } A(x))$
  • $a \text{ ur } \forall x A(x) \iff \forall x (a \text{ ur } A(x))$
  • Aquí, el realizador $a$ es el mismo para todos los $x$ en el caso universal, y la existencia de un $x$ se maneja en la meta-teoría, no necesariamente dentro de la estructura de datos de $a$.
• Distinción de Cuantificadores: Se distingue entre cuantificadores no cualificados (uniformes) y cualificados (tipados, ej. $\forall x \in N$). Los autores proponen tratar los cuantificadores cualificados como abreviaturas lógicas de fórmulas con conectivos estándar ($\forall x (N(x) \to A(x))$), permitiendo que la interpretación uniforme maneje la lógica subyacente mientras la base interpreta el predicado $N(x)$.

3. Contribuciones Clave

1. Marco Unificado Paramétrico: Se define una familia de interpretaciones donde la variabilidad entre diferentes sistemas de realizabilidad reside exclusivamente en la interpretación base de los predicados atómicos (igualdad, falsedad, pertenencia a números naturales), mientras que la estructura lógica (cuantificadores y conectivos) permanece fija y uniforme.
2. Teorema de Corrección General (Soundness): Se demuestra un teorema de corrección (Teorema 2.7) que establece que si los axiomas no lógicos de la teoría fuente son realizables bajo una interpretación base específica, entonces todos los teoremas de la teoría son realizables. Esto reduce la carga de prueba para nuevos sistemas de realizabilidad a verificar solo los axiomas atómicos.
3. Unificación de Sistemas Existentes: El marco demuestra que cinco sistemas distintos son casos particulares de realizabilidad uniforme:
   • Realizabilidad de Kleene: Se obtiene interpretando $N(n)$ como $n=a$ (preciso) y la igualdad como identidad.
   • Realizabilidad Modificada de Kreisel: Se obtiene usando funciones totales y tipos finitos, con una interpretación similar a Kleene pero en un sistema de tipos.
   • Realizabilidad de Herbrand: Se logra interpretando $N(n)$ como "verdadero" (uniforme) y los números estándar como conjuntos finitos que contienen al número.
   • Realizabilidad Clásica: Se modela dando contenido computacional a la falsedad ($\bot$) mediante un predicado auxiliar, permitiendo extraer contenido de fórmulas negadas.
   • Realizabilidad de Aprendizaje (Aschieri-Berardi): Se modela introduciendo un estado de conocimiento $s$. Los realizadores son transformadores de estado que actualizan el conocimiento hasta alcanzar un punto fijo.

4. Resultados Técnicos

• Tratamiento de la Inducción: El papel analiza cómo diferentes interpretaciones de $N(n)$ (precisa, aproximada, uniforme) afectan la realizabilidad del esquema de inducción.
  • Para interpretaciones aproximadas (ej. $n \leq a$), se requiere una operación de unión ($\cup$) sobre realizadores para construir el realizador de la inducción.
  • Para interpretaciones precisas ($n=a$), la inducción se reduce a la recursión primitiva estándar.
• Equivalencias y Simplificaciones: Se muestran cómo las definiciones generales se simplifican a las cláusulas clásicas de realizabilidad cuando se eligen interpretaciones base específicas. Por ejemplo, en la realizabilidad de aprendizaje, la igualdad $n=m$ se interpreta como $(\gamma(s)=s) \to (n=m)$, lo que permite que la igualdad sea "falsa" si el estado no es un punto fijo, capturando la naturaleza dinámica del aprendizaje.
• Conservación y Extensiones: Se discute que el marco permite añadir fórmulas clásicamente válidas (como la eliminación de doble negación para fórmulas uniformes) como axiomas, siempre que los predicados involucrados sean interpretados uniformemente.

5. Significado e Impacto

• Abstracción de Diferencias: El trabajo logra aislar las diferencias entre realizabilidades complejas, mostrando que la complejidad reside en la gestión de los predicados atómicos y no en la lógica de los cuantificadores.
• Herramienta para Nuevos Sistemas: Proporciona una receta clara para diseñar nuevas interpretaciones de realizabilidad: basta con definir cómo se interpretan los predicados atómicos de la teoría fuente en la teoría objetivo, y la corrección del sistema completo sigue automáticamente del teorema general.
• Puente entre Lógica Intuicionista y Clásica: Al permitir interpretaciones no triviales de la falsedad y la igualdad, el marco conecta naturalmente la realizabilidad intuicionista con sistemas que extraen contenido computacional de pruebas clásicas (como la traducción de Friedman-Dragalin).
• Fundamento para Futuras Investigaciones: Sugiere que la noción de uniformidad puede extenderse a conectivos proposicionales (como en el enfoque de Schwichtenberg) y a tipos de intersección, ofreciendo una base sólida para la teoría de tipos y la semántica de la computación.

En conclusión, Berger y Oliva presentan una teoría unificada que no solo clasifica las realizabilidades existentes, sino que ofrece un mecanismo robusto para generar y verificar nuevas interpretaciones, simplificando significativamente el estudio de la relación entre pruebas lógicas y programas computacionales.