Classical Logic as Intuitionistic Logic with Duality

Resumen Técnico: La lógica clásica como lógica intuicionista con dualidad

1. El problema
El artículo aborda un desafío fundacional en la teoría del significado: proporcionar una semántica de prueba-teórica (P-tS) para la lógica clásica que se adhiera a principios anti-realistas (constructivistas) sin presuponer el principio de bivalencia o la verdad de trascendencia de la verificación. Si bien Sandqvist ha desarrollado con éxito la semántica de extensión de base (B-eS) para la lógica intuicionista (IPL) y una versión para la lógica clásica (CPL), persisten ciertas limitaciones. La semántica de CPL de Sandqvist está restringida a conectivas específicas (inicialmente $\to, \bot, \forall$) y depende de una demostración de completitud técnicamente compleja que involucra la inducción sobre la barra (bar induction). Además, los enfoques existentes suelen tener dificultades para tratar el lenguaje proposicional completo (incluyendo $\lor$ y $\exists$) de manera constructiva. Los autores pretenden resolver esto ofreciendo una B-eS para la lógica proposicional clásica completa que mantenga una demostración de completitud elemental y constructiva, respondiendo así al desafío de Dummett respecto a la reconciliación de la inferencia clásica con el significado anti-realista.

2. Metodología y marco filosófico
Los autores proponen un marco bilateralista donde la lógica clásica se conceptualiza como "Lógica Intuicionista + Dualidad". Este enfoque se aparta de las visiones tradicionales al distinguir entre contenido y fuerza ilocutiva a nivel atómico, mientras trata las fórmulas complejas como estructuras logico-gramaticales en lugar de proposiciones que poseen fuerza por sí mismas.

• Literales como proposiciones: El sistema introduce "literales" ($L$) como los únicos objetos de aserción y negación. Un contenido $c$ se empareja con una fuerza para formar un literal positivo ($c^+$, aserción) o un literal negativo ($c^-$, negación). Crucialmente, la dualidad es primitiva: $c^+$ y $c^-$ son actos de habla atómicos independientes, no definidos vía negación ($\neg$).
• Estructuras logico-gramaticales: Las fórmulas complejas (p. ej., $\phi \land \psi$) no son proposiciones para ser asertadas o negadas, sino estructuras que organizan el razonamiento. En consecuencia, la distincción bilateral (aserción frente a negación) se restringe al nivel atómico (literales).
• Dualidad inferencial: La classicalidad se recupera no añadiendo una semántica de valores de verdad, sino introduciendo dos principios inferenciales armoniosos a nivel atómico (siguiendo a Negri y von Plato):
  1. Exclusión (EXC1): Asertar y negar el mismo contenido conduce al absurdo ($l, l^\perp \vdash \bot$).
  2. Análisis de casos (EXC2): Si una conclusión sigue tanto de una aserción como de su negación dual, sigue de forma directa ($l \vdash \phi, l^\perp \vdash \phi \implies \vdash \phi$).

3. Desarrollo técnico

• Sistema de deducción natural ($NK^\pm$): Los autores definen un sistema de deducción natural que comprende las reglas intuicionistas estándar ($NJ$) más las reglas de dualidad atómica (EXC1 y EXC2). Este sistema trata los literales como la base, con fórmulas complejas construidas mediante conectivas estándar.
• Semántica de extensión de base (B-eS):
  • Bases ($B$): Una base es un conjunto de reglas atómicas (relaciones inferenciales entre literales).
  • Derivabilidad ($\vdash_B$): La derivabilidad en una base se define inductivamente. Incluye reglas estructurales estándar (reflexividad, aplicación) y las dos nuevas cláusulas (exc1, exc2) que imponen la dualidad en el nivel del literal.
  • Soporte ($\Vdash_B$): La validez de una fórmula se define inductivamente sobre la estructura de las fórmulas. Crucialmente, las cláusulas de soporte para las conectivas ($\to, \land, \lor$) son idénticas a las definiciones intuicionistas de Sandqvist. El carácter clásico de la semántica es transportado íntegramente por las cláusulas de dualidad en la definición de derivabilidad en la base, no por las cláusulas de soporte para fórmulas complejas.
  • Validez ($\Gamma \Vdash \phi$): Una fórmula es válida si es soportada en todas las bases.

4. Resultados clave

• Solidez (Teorema 5.1): El sistema es sólido: si $\Gamma \vdash_{NK^\pm} \phi$, entonces $\Gamma \Vdash \phi$. La demostración procede por inducción sobre la derivación, mostrando que las reglas clásicas (EXC1, EXC2) preservan el soporte.
• Completitud (Teorema de 6.2): El sistema es completo: si $\Gamma \Vdash \phi$, entonces $\Gamma \vdash_{NK^\pm} \phi$.
  • La demostración adapta el método elemental de Sandqvist para la lógica intuicionista.
  • Utiliza una "base de simulación" ($\mathcal{N}$) construida a partir de los subfórmulas del secuente.
  • Un operador de "aplanamiento" mapea fórmulas complejas a literales atómicos dentro de la base de simulación.
  • El lema de "Naturalización" demuestra que la derivabilidad en la base de simulación puede traducirse de vuelta a la derivabilidad en $NK^\pm$.
  • A diferencia de enfoques anteriores, esta demostración maneja el lenguaje proposicional completo (incluyendo $\lor$) y se apoya en recursos matemáticos elementales, evitando la inducción sobre la barra o los modelos canónicos.

5. Significado y Reivindicaciones
El artículo afirma proporcionar una novedosa semántica de prueba-teórica para la lógica clásica que:

1. Unifica IPL y CPL: Demuestra que la lógica clásica puede entenderse como la lógica intuicionista suplementada por un principio primitivo de dualidad a nivel atómico.
2. Respeta el anti-realismo: Al evitar los valores de verdad y la bivalencia, y al utilizar una demostración de completitud constructiva, ofrece un fundamento genuinamente anti-realista para la lógica clásica, abordando el desafío fundacional de Dummett.
3. Simplifica la complejidad técnica: Al restringir el bilateralismo a los literales y tratar las fórmulas complejas como estructurales, los autores logran una demostración de completitud de "carácter notablemente elemental", comparable al trabajo de Sandqvist sobre la lógica intuicionista, superando las dificultades técnicas de los intentos previos de B-eS clásica.
4. Ofrece una alternativa a la teoría de modelos: Los autores posicionan este trabajo como una alternativa a la semántica de teoría de modelos y a los enfoques de P-tS existentes que dependen de conceptos de la teoría de modelos (como los de Makinson o Eckhardt y Pym), con el fin de establecer un tratamiento puramente inferencialista de la lógica clásica.

El artículo concluye que este marco abre la posibilidad de un tratamiento sistemático de las lógicas clásicas análogo al tratamiento sistemático ya establecido para las lógicas intuicionistas dentro de la tradición de la P-tS.