Hyperformalism for Relevant Modal Logics

Resumen Técnico: Hiperformalismo para Lógicas Modales Relevantes

Problema y Contexto
El artículo aborda el análisis de las lógicas relevantes a través de la lente del hiperformalismo, una propiedad en la que una lógica permanece cerrada bajo sustituciones no uniformes. En las lógicas formales estándar, las fórmulas atómicas se tratan como independientes mediante la sustitución uniforme. El hiperformalismo extiende esta independencia, permitiendo que ocurrencias distintas del mismo átomo sean tratadas como independientes si aparecen en contextos sintácticos suficientemente diferentes (por ejemplo, a diferentes "profundidades" o bajo diferentes operadores modales). Si bien el hiperformalismo se ha aplicado con éxito a lógicas relevantes no modales (como $B$ y $DR$), revelando fuertes propiedades de compartición de variables e identificando nuevas lógicas relevantes, su aplicación a las lógicas modales relevantes sigue siendo poco explorada. Los autores buscan extender estas técnicas al ámbito modal, investigando específicamente cómo la presencia del operador modal $\square$ interactúa con las sustituciones no uniformes y la compartición de variables.

Metodología
Los autores emplean una combinación de técnicas proof-teóricas y semánticas para analizar las lógicas modales relevantes:

1. Marco Sintáctico (MPos): Los autores definen un conjunto de posiciones, $MPos = \{l, r, n, b\}^*c$, donde $l$ y $r$ denotan las ramas izquierda y derecha de los condicionales, $n$ denota la negación, y $b$ denota el alcance del operador modal $\square$.
2. Sustituciones: Definen las sustituciones MPos como funciones $\sigma: MPos \times At \to L$ que respetan la estructura de las fórmulas. Crucialmente, estas sustituciones tratan los átomos en diferentes posiciones como independientes, sujetas a restricciones específicas de "fidelidad" (por ejemplo, $\sigma_{xnn}(p) = \sigma_x(p)$ para preservar las propiedades de doble negación).
3. Análisis Proof-teórico: El artículo analiza la lógica modal relevante base $B^\square$ (formada al añadir los axiomas $C$ y la regla $RM$ a la lógica relevante $B$). Demuestran la clausura bajo sustituciones MPos mediante inducción sobre las derivaciones.
4. Extensiones: Los autores definen relaciones de equivalencia en $MPos$ correspondientes a los axiomas modales $T, 4, K$ y $RN$. Investigan las lógicas resultantes $B^\square_S$ y su clausura bajo las correspondientes sustituciones $MPos_S$.
5. Caracterización Semántica: Para caracterizar la mayor sublógica hiperformal de MPos de la lógica modal clásica $K$ (denotada $KMPos$), los autores introducen:
   • Asignaciones MPosK: Funciones $\alpha: MPos \times W \times At \to \{0, 1\}$ sobre marcos de Kripke, donde los valores de verdad varían según el índice de posición.
   • Tableaux Analíticos: Un sistema de tableaux con nodos $\langle x, \omega, A, i \rangle$ que rastrean posiciones ($x$), mundos ($\omega$), fórmulas ($A$) y valores de verdad ($i$).
6. Modelos Canónicos: La completitud se establece mediante la construcción de conjuntos de ramas máximos, con testigos y consistentes con el tableau, y sus correspondientes modelos canónicos.

Contribuciones Clave y Resultados

1. Hiperformalismo de $B^\square$ respecto a MPos:

   • Teorema 2.1: Se demuestra que la lógica base $B^\square$ es MPos-hiperformal. La prueba demuestra que los axiomas ($C$) y las reglas ($RM$) del sistema preservan la demostrabilidad bajo sustituciones MPos.
   • Compartición de Variables: Como consecuencia, $B^\square$ satisface la propiedad de compartición de variables MPos. Si $A \to B$ es un teorema, existe una variable compartida $p$ tal que la posición de $p$ en $A$ y $B$ son equivalentes bajo la relación $\sim_{nn}$ (difieren solo por pares de negaciones).
   • Corolario 2.6: Una consecuencia específica es que cualquier teorema $A \to B$ en $B^\square$ comparte una variable anidada dentro del mismo número de operadores $\square$ tanto en el antecedente como en el consecuente.

2. Extensiones de $B^\square$:

   • Teorema 2.7: Para cualquier subconjunto $S \subseteq \{T, 4, K, RN\}$, la lógica $B^\square_S$ es $MPos_S$-hiperformal, donde $MPos_S$ incorpora relaciones de equivalencia que reflejan los axiomas modales específicos (por ejemplo, $xby \sim_4 xbby$ para el axioma 4).
   • Compartición de Variables Refinada: Estas extensiones producen propiedades de compartición de variables refinadas. Por ejemplo, en $B^\square_{\{4\}}$, las variables compartidas deben tener el mismo "modo" (extensional vs. intensional), eliminando efectivamente el conteo de operadores $\square$ de la condición de compartición.

3. Caracterización de $KMPos$:

   • Los autores definen $KMPos$ como la mayor sublógica hiperformal de MPos de la lógica modal clásica $K$.
   • Caracterización Semántica: $KMPos$ se caracteriza por la validez en marcos de Kripke equipados con asignaciones MPosK.
   • Caracterización por Tableau: Se proporciona un sistema de tableau sonido y completo para $KMPos$.
   • Teorema 3.6: $KMPos$ es equivalente al conjunto de fórmulas $A$ tales que para alguna sustitución $\iota$ atómica e inyectiva-hasta-la-fidelidad, $\iota(A)$ es un teorema de $K$. Esto confirma que $KMPos$ es el subconjunto maximal de $K$ cerrado bajo sustituciones MPos.
   • Compartición de Variables: El Teorema 3.9 establece que $KMPos$ posee la propiedad de compartición de variables.

4. Transitividad y Naturaleza de $KMPos$:

   • Teorema 4.1: $KMPos$ es transitiva. Los autores argumentan que, a diferencia de los enfoques de "tamiz sintáctico" para la relevancia (que a menudo fallan en la transitividad), $KMPos$ evita tales patologías porque está definida por una propiedad de clausura (hiperformalismo) en lugar de un filtro estático sobre los teoremas clásicos.

Significancia y Reivindicaciones
El artículo sostiene que el hiperformalismo es una herramienta poderosa para analizar las lógicas modales relevantes, capaz de revelar fuertes propiedades de compartición de variables incluso en sistemas débiles como $B^\square$. Sin embargo, los autores argumentan que $B^\square$ no es la lógica más fuerte con estas características.

La principal significancia radica en la introducción y caracterización de $KMPos$. Los autores postulan que $KMPos$ representa la "mayor" lógica modal relevante en el sentido de ser la sublógica maximal de la lógica clásica $K$ que es cerrada bajo sustituciones MPos. Afirman que $KMPos$ ofrece ventajas semánticas y proof-teóricas sobre $B^\square$ y otras lógicas modales relevantes tradicionales. Específicamente, argumentan que $KMPos$ no es meramente un "tamiz sintáctico" (un término peyorativo para lógicas definidas simplemente filtrando teoremas clásicos) porque es transitiva y está definida por una robusta propiedad de clausura.

El artículo concluye desafiando la preferencia por las lógicas modales relevantes "tradicionales" (como $B^\square$) sobre $KMPos$. Los autores sugieren que, a menos que existan razones específicas para preferir las primeras, los investigadores deberían considerar $KMPos$, ya que retiene las deseables características de compartición de variables mientras es una sublógica maximal de la lógica clásica. El artículo reconoce que la caracterización axiomática de $KMPos$ sigue siendo un problema abierto, señalando que tales lógicas han resistido históricamente la axiomatización recursiva.