Dynamic Hypersequents for Public Announcement Logic

Resumen Técnico: Hipersecuentes Dinámicos para la Lógica de Anuncio Público

Planteamiento del Problema
La Lógica Epistémica Dinámica (DEL), y específicamente la Lógica de Anuncio Público (PAL), modela la evolución del conocimiento a través de actualizaciones de información. Si bien la semántica de la PAL está bien entendida como transformaciones de modelos de Kripke (donde un anuncio restringe el conjunto de mundos posibles), los marcos de demostración existentes luchan por capturar esta dinamicidad a nivel sintáctico. Los intentos previos, incluidos los métodos de tablas semánticas y varios cálculos de secuentes (etiquetados y no etiquetados), a menudo fracasan en lograr simultáneamente una propiedad genuina de subsiguiente, la admisibilidad de todas las reglas estructurales (incluida la contracción) y la eliminación sintáctica del corte. Muchos sistemas existentes dependen de axiomas de reducción que traducen fórmulas dinámicas en estáticas, oscureciendo así la naturaleza dinámica de la lógica dentro del propio sistema de demostración.

Metodología
Los autores proponen un nuevo marco de demostración basado en hipersecuentes dinámicos. Este enfoque extiende el cálculo de hipersecuentes para S5 (introducido en [15, 16]) incorporando un mecanismo para modelar transiciones entre modelos epistémicos inducidas por anuncios públicos.

1. Secuentes Dinámicos: Un secuente dinámico se define como una secuencia de secuentes estándar etiquetados por secuencias finitas distintas de anuncios (por ejemplo, $\alpha_1 \Gamma_1 | \dots | \alpha_n \Gamma_n$). Intuitivamente, un secuente dinámico representa un mundo específico $w$ en un modelo inicial $M$ y sus "copias" en modelos actualizados sucesivamente $M_{\alpha}$.
2. Hipersecuentes Dinámicos (DHS): Un hipersecuente dinámico es una colección de secuentes dinámicos. Esta estructura representa sintácticamente un modelo epistémico completo y sus actualizaciones sucesivas simultáneamente. Los autores interpretan un DHS como una disyunción de fórmulas modalizadas, donde cada componente corresponde a un mundo en el modelo o sus actualizaciones.
3. El Cálculo ($DHSPAL$): Los autores definen un cálculo $DHSPAL$ que comprende:
   • Reglas Proposicionales y Modales: Adaptadas de los cálculos de hipersecuentes estándar para S5.
   • Reglas de Anuncio: Reglas $(L[\cdot])$ y $(R[\cdot])$ que descomponen fórmulas de anuncio público $[A]B$. Estas reglas gestionan explícitamente la transición desde un estado actual a un estado actualizado mediante la introducción de nuevos secuentes dinámicos etiquetados con la secuencia de anuncio extendida $\alpha \cdot A$.
   • Reglas Estructurales Dinámicas: Reglas específicas como $(Lat)$y$(Rat)$ (Permanencia Atómica), $(New)$ (asegurando que los mundos en modelos actualizados existan en los anteriores) y $(Recall)$ (asegurando que la fórmula anunciada se cumple en el modelo anterior).
   • Regla Modal Dinámica: Una regla especializada $(L\Box_3)$ que maneja la interacción entre el conocimiento ($\Box$) y secuencias de anuncios, distinguiendo entre los mundos que sobreviven a una actualización y aquellos que no.

Contribuciones y Resultados Clave
El artículo establece que $DHSPAL$ es un sistema de demostración robusto para la PAL, logrando varias propiedades que los sistemas anteriores no satisfacían simultáneamente:

• Admisibilidad de Reglas Estructurales: Los autores prueban la admisibilidad hp (admisibilidad que preserva la altura) del debilitamiento, la contracción y una regla de fusión. Crucialmente, esto incluye la contracción, que a menudo es difícil de lograr en lógicas dinámicas sin perder analiticidad.
• Invertibilidad de Reglas Lógicas: Se demuestra que todas las reglas lógicas en el cálculo son hp-invertibles. Esta propiedad es esencial para la búsqueda de demostraciones y para establecer la eliminación del corte.
• Eliminación Sintáctica del Corte: El artículo proporciona una prueba de la admisibilidad de la regla de Corte. La prueba se basa en una doble inducción: una sobre la complejidad-DHS de la fórmula de corte (una medida de complejidad relativa a la secuencia de anuncios) y otra sobre la suma de las alturas de las derivaciones de las premisas.
• Corrección y Completitud: El cálculo se demuestra correcto y completo con respecto a la semántica estándar de Kripke de la PAL. La prueba de completitud implica derivar todos los axiomas al estilo de Hilbert de la PAL, incluidos los axiomas de reducción, dentro del marco de hipersecuentes dinámicos.
• Propiedad de Subsiguiente: Como consecuencia de la eliminación del corte, el cálculo goza de la propiedad de subsiguiente, asegurando que cualquier fórmula en una derivación sea una subsiguiente del secuente final o de un anuncio que ocurra dentro de él.

Significado y Afirmaciones
Los autores afirman que este trabajo representa un paso significativo hacia la superación de la brecha entre la dinamicidad semántica de la PAL y su teoría de la demostración sintáctica. Al utilizar hipersecuentes dinámicos, el sistema captura el carácter dinámico de la lógica mediante medios puramente estructurales, evitando la necesidad de elementos semánticos explícitos (como etiquetas para mundos) o la reducción a lógica estática.

El artículo afirma que, según su conocimiento, $DHSPAL$ es el primer cálculo para la PAL que satisface simultáneamente:

1. Admisibilidad de todas las reglas estructurales (incluida la contracción).
2. Invertibilidad de todas las reglas lógicas.
3. Eliminación sintáctica del corte.
4. Una propiedad genuina de subsiguiente.

Los autores concluyen que el marco de hipersecuentes dinámicos es lo suficientemente expresivo y robusto para servir como base para el desarrollo de cálculos de secuentes para clases más amplias de lógicas epistémicas dinámicas que involucran diferentes tipos de actualizaciones de información. Sugieren que trabajos futuros podrían explorar la decidibilidad, la interpolación y el análisis de complejidad dentro de este marco.