Labelled Sequent Calculi for Propositional Team Logics

Resumen Técnico: Cálculos de Secuentes Etiquetados para Lógicas de Equipos Proposicionales

Planteamiento del Problema
El artículo aborda los desafíos de la teoría de la prueba asociados con las lógicas proposicionales basadas en la semántica de equipos (team semantics). Si bien las propiedades semánticas de las lógicas de equipos de clausura descendente (downward-closed) —específicamente la lógica inquisitiva básica (InqB), la lógica de dependencia intuicionista proposicional (PID) y sus extensiones con disyunción tensorial (InqB$\lor$ y PID$\lor$)— están bien comprendidas, su teoría de la prueba permanece subdesarrollada. Los sistemas de prueba analíticos existentes para estas lógicas, como los cálculos de display multitipe o los cálculos de secuentes de inferencia profunda, a menudo involucran enriquecimientos estructurales complejos de los secuentes de estilo Gentzen. Los autores identifican la necesidad de cálculos de secuentes etiquetados modulares que puedan manejar las condiciones de satisfacción específicas de la semántica de equipos, particularmente el comportamiento de la disyunción tensorial ($\lor$) y los átomos de dependencia, garantizando al mismo tiempo propiedades como la admisibilidad del corte (cut-admissibility) y la búsqueda de pruebas terminante.

Metodología
Los autores desarrollan dos familias de cálculos de secuentes etiquetados para las cuatro lógicas objetivo:

1. Cálculos Etiquetados Generales ($G(L)$): Estos sistemas utilizan etiquetas construidas a partir de conjuntos infinitos de variables de equipo ($S$ para equipos unitarios, $A$ para equipos arbitrarios) combinadas con operaciones de la teoría de conjuntos (unión $\cup$ e intersección $\cap$). Las etiquetas representan equipos arbitrarios, equipos unitarios y sus combinaciones. Los cálculos incluyen:

   • Secuentes Iniciales y Reglas Lógicas: Reflejan las condiciones de satisfacción definidas en la semántica de equipos (por ejemplo, reglas para $\land$, $\lor$, $\to$ y la disyunción tensorial $\lor$).
   • Reglas de Orden: Un conjunto de reglas que formalizan las propiedades de la teoría de conjuntos (por ejemplo, transitividad, unión, intersección y la propiedad del equipo vacío).
   • Reglas Especiales: Se introduce una regla llamada fin para manejar el supuesto de que el conjunto de variables proposicionales $P$ es finito. Esta regla permite al sistema describir cualquier equipo como una unión de $2^{|P|}$ valoraciones, lo cual es crucial para simular la disyunción tensorial sobre fórmulas clásicas.
   • Modularidad: Los sistemas están diseñados de tal manera que los cálculos para PID y PID$\lor$ se obtienen añadiendo reglas específicas para los átomos de dependencia a los cálculos para InqB e InqB$\lor$.

2. Cálculos Terminantes ($G^\star(L)$): Para facilitar la búsqueda automática de pruebas, los autores introducen una variante simplificada donde las etiquetas se definen como conjuntos finitos de variables en lugar de términos complejos que involucran uniones e intersecciones. Este enfoque elimina la necesidad de átomos relacionales y reglas de orden, reemplazándolos por reglas que operan directamente sobre el conjunto de variables en una etiqueta.

Contribuciones Clave y Resultados

• Corrección y Completitud: Los autores demuestran que los cálculos generales $G(L)$ son correctos y completos con respecto a sus correspondientes semánticas de equipos y axiomatizaciones de estilo Hilbert. Esto se logra demostrando la admisibilidad de las reglas estructurales (debilidad, contracción, corte) y estableciendo la admisibilidad de las reglas derivadas (como mp para el modus ponens y flat para la planitud de las fórmulas clásicas).
• Admisibilidad del Corte: Un resultado técnico central es la demostración de la admisibilidad del corte para los cuatro cálculos. La prueba procede mediante inducción sobre el rango de la fórmula del corte y la altura de la derivación, utilizando un orden lexicográfico que tiene en cuenta tanto la complejidad de la fórmula como la etiqueta.
• Búsqueda de Pruebas Terminante: El artículo presenta algoritmos de búsqueda de pruebas terminantes explícitos para los cálculos simplificados $G^\star(L)$. El algoritmo construye un árbol de búsqueda de pruebas desde la raíz hacia abajo (root-first). Se demuestra que termina porque el número de fórmulas etiquetadas posibles es finito (dado un conjunto finito de variables proposicionales y un conjunto finito de subfórmulas).
• Procedimientos de Decisión: La naturaleza terminante de los cálculos $G^\star(L)$ implica que los problemas de satisfacibilidad y validez para InqB, PID, InqB$\lor$ y PID$\lor$ son decidibles. Los autores proporcionan una construcción de contramodelo a partir de cualquier rama saturada (abierta) del árbol de búsqueda de pruebas, asegurando la completitud del procedimiento de búsqueda.

Significancia y Reivindicaciones
El artículo afirma que su contribución principal radica en proporcionar los primeros cálculos de secuentes etiquetados correctos y completos para todo el rango de lógicas de equipos proposicionales, incluyendo la disyunción tensorial y los átomos de dependencia. Los autores destacan dos ventajas distintas de su enfoque:

1. Modularidad: Los sistemas de prueba pueden adaptarse a diferentes conjuntos de conectivas o átomos simplemente añadiendo o eliminando reglas, una característica que no está presente en los cálculos estructurados más rígidos de la literatura previa.
2. Terminación y Decisión: Al simplificar la estructura de las etiquetas en $G^\star(L)$, los autores proporcionan un procedimiento de decisión concreto para estas lógicas, un paso significativo para el razonamiento automatizado en la semántica de equipos.

Los autores señalan que, si bien los cálculos generales $G(L)$ pueden producir pruebas más cortas debido a las reglas de premisa fija y la capacidad de razonar sobre subconjuntos arbitrarios mediante variables, los cálculos simplificados $G^\star(L)$ son esenciales para establecer la terminación. El trabajo está restringido a lenguajes con infinitamente muchos átomos proposicionales, una condición necesaria para la regla fin y la terminación de la búsqueda de pruebas en presencia de disyunción tensorial. El artículo concluye identificando trabajos futuros, incluyendo la extensión de estos sistemas a lenguajes con infinitos átomos y el desarrollo de sistemas de prueba para otras clases de lógicas de equipos, tales como aquellas sin implicación intuicionista o aquellas que poseen la propiedad de clausura de unión.