Modelos de Demostrabilidad

Información Básica

• ID del Artículo: 2510.06696
• Título: Modelos de Demostrabilidad
• Autores: Mojtaba Mojtahedi (Universidad de Gante), Borja Sierra Miranda (Universidad de Berna)
• Clasificación: math.LO (Lógica Matemática)
• Fecha de Publicación: 15 de octubre de 2025
• Enlace del Artículo: https://arxiv.org/abs/2510.06696

Resumen

Este artículo investiga una nueva semántica tipo Kripke—modelos de demostrabilidad (provability models)—para la lógica modal clásica. La investigación abarca modelos de demostrabilidad para las lógicas modales proposicionales K, K4, S4, GL, GLP y la lógica de interpretabilidad ILM. Los modelos de demostrabilidad combinan características de los modelos de Kripke con el enfoque de asignar lógicas a mundos individuales. Este modelo fue introducido originalmente por Mojtahedi en 2022 para establecer la completitud aritmética de la lógica de demostrabilidad intuicionista. Notablemente, este artículo demuestra que ILM es completo respecto a los mismos modelos de demostrabilidad que GL. En los casos de GL e ILM, el artículo mejora los modelos de demostrabilidad a modelos de demostrabilidad predecibles y decidibles, y demuestra la solidez y completitud de GLP respecto a los modelos de demostrabilidad.

Contexto y Motivación de la Investigación

Problema Central

En la investigación tradicional de lógica de demostrabilidad, los operadores modales se interpretan típicamente como predicados de demostrabilidad en algún sistema aritmético de primer orden o teoría de conjuntos. Sin embargo, también es posible interpretar □A como L ⊢ A (para una teoría proposicional L dada). Aunque puede demostrarse que GL es sólido respecto a las L-interpretaciones para cualquier lógica L que contenga GL, ninguna L-interpretación puede proporcionar completitud para GL.

Importancia del Problema

Este fracaso contrasta con las interpretaciones PA, derivándose principalmente del hecho de que la lógica L no puede simular modelos de Kripke, mientras que la Aritmética de Peano puede aprovechar su capacidad para simular modelos de Kripke (como demostró Solovay). Por lo tanto, no puede esperarse que GL sea la lógica de demostrabilidad de una única lógica proposicional.

Limitaciones de los Enfoques Existentes

1. Restricciones de los modelos de Kripke estándar: No pueden tratar directamente las interpretaciones aritméticas de la lógica de demostrabilidad
2. Incompletitud de las interpretaciones de demostrabilidad proposicional: Una única lógica proposicional no puede proporcionar completitud para GL
3. Propiedades de marco complejas: Tales como las propiedades de marco complejas en la semántica de Iemhoff, que dificultan el establecimiento de teoremas de completitud aritmética

Motivación de la Investigación

Este artículo cierra esta brecha incorporando explícitamente marcos de Kripke en la lógica proposicional, considerando modelos de Kripke estándar donde cada mundo w está equipado con una lógica Lw, e imponiendo relaciones de accesibilidad entre estas teorías basadas en la relación de accesibilidad subyacente.

Contribuciones Principales

1. Propuesta del marco de modelos de demostrabilidad: Introduce una nueva semántica tipo Kripke para la lógica modal clásica
2. Establecimiento de completitud para múltiples lógicas modales: Demuestra solidez y completitud de K, K4, S4, GL respecto a modelos de demostrabilidad
3. Construcción de modelos de demostrabilidad independientes: Particularmente para GL e ILM, muestra cómo construir modelos de demostrabilidad independientes de los modelos de Kripke estándar
4. Realización de decidibilidad: En los casos de GL e ILM, construye modelos de demostrabilidad decidibles
5. Extensión a lógicas multimodales: Demuestra solidez y completitud de GLP (lógica de demostrabilidad multimodal) respecto a modelos de demostrabilidad
6. Establecimiento de completitud de ILM: Demuestra que la lógica de interpretabilidad ILM es completa respecto a los mismos modelos de demostrabilidad que GL

Explicación Detallada de Métodos

Definición de Tareas

Investiga modelos de demostrabilidad como semántica para lógicas modales, donde:

• Entrada: Fórmulas de lógica modal y modelos de demostrabilidad
• Salida: Juicio de validez de la fórmula en el modelo
• Restricciones: El modelo debe satisfacer propiedades lógicas específicas y condiciones de marco

Arquitectura del Modelo

Definición de Premodelo de Demostrabilidad

Un premodelo de demostrabilidad P = (W, <, {Lw}w∈W, V) contiene:

• W: Conjunto no vacío de mundos
• <: Relación binaria en W
• Lw: Lógica para cada mundo w accesible por <
• V: Relación de asignación para proposiciones atómicas

Definición de Validez

Para una fórmula A, se define P, w |= A por inducción:

• Conmuta con conectivos booleanos
• P, w |= □A si y solo si ∀u ⪯ w (⊢u A)

Condiciones de Modelo de Demostrabilidad

Un premodelo de demostrabilidad se convierte en modelo de demostrabilidad si satisface:

• Completitud modal: Para cada fórmula modal pura A, si P, w |=+ A entonces ⊢w A

Puntos de Innovación Técnica

1. Logificación de Condiciones de Marco

Los modelos de demostrabilidad pueden absorber condiciones de marco como reglas de inferencia de lógicas asignadas a mundos individuales:

• La transitividad puede ser reemplazada por la regla de necesitación
• La irreflexividad bien fundada puede ser reemplazada por la regla de Löb

2. Método Constructivo

Para GL e ILM, proporciona métodos constructivos para construir modelos de demostrabilidad:

Teorema 4.4: Para cada premodelo de demostrabilidad de árbol irreflexivo bien fundado P, existe un modelo de demostrabilidad P̄ con necesitación tal que:

• P̄ tiene necesitación
• P ⊆ P̄
• P̄ es el modelo de demostrabilidad mínimo que contiene P

3. Garantía de Decidibilidad

Si P es bifinito, entonces P̄ es decidible, donde bifinito significa que W y Axiom(Lw) para cada w∈W son finitos.

Configuración Experimental

Marco de Verificación Teórica

El artículo realiza principalmente pruebas teóricas, con marco de verificación que incluye:

1. Pruebas de Solidez

Para varias lógicas modales, demuestra que si la lógica ⊢ A, entonces P |= A para todos los modelos de demostrabilidad P correspondientes.

2. Pruebas de Completitud

Demuestra que si P |= A para todos los modelos de demostrabilidad P correspondientes, entonces la lógica ⊢ A.

3. Completitud Fuerte

Particularmente para GL, demuestra completitud fuerte: Γ |=P A implica Γ ⊢GL A.

Verificación de Métodos de Construcción

Verifica mediante construcción explícita:

• Existencia de modelos de demostrabilidad finitos
• Realización de decidibilidad
• Independencia (no depende de modelos de Kripke estándar)

Resultados Experimentales

Resultados Principales

1. Completitud de Lógicas Modales Básicas

• K: Sólido y completo respecto a modelos de demostrabilidad (Teoremas 3.6, 3.7)
• K4: Sólido y completo respecto a modelos de demostrabilidad con necesitación o transitividad (Teoremas 3.8, 3.9)
• S4: Sólido y completo respecto a modelos de demostrabilidad reflexivos, transitivos, con necesitación y completitud local (Teoremas 3.11, 3.12)

2. Resultados para la Lógica de Demostrabilidad GL

• Solidez: GL es sólido respecto a modelos de demostrabilidad irreflexivos bien fundados con necesitación y regla de Löb (Teorema 3.14)
• Completitud: GL es completo respecto a modelos de demostrabilidad finitos, transitivos y no reflexivos (Teorema 3.17)
• Completitud Fuerte: GL es fuertemente completo respecto a modelos de demostrabilidad con necesitación y regla de Löb (Teorema 3.18)
• Completitud Finitaria: GL es completo respecto a modelos de demostrabilidad finitarios (Teorema 4.6)

3. Resultados para la Lógica de Interpretabilidad ILM

• Solidez: ILM es sólido respecto a modelos de demostrabilidad irreflexivos bien fundados con necesitación (Teorema 5.6)
• Completitud: ILM es completo respecto a modelos de demostrabilidad de árbol irreflexivo bien fundado finito con necesitación (Teorema 5.10)
• Completitud Finitaria: ILM es completo respecto a modelos de demostrabilidad finitarios (Teorema 5.13)

4. Resultados para la Lógica de Demostrabilidad Multimodal GLP

• Solidez y Completitud: GLP es sólido y fuertemente completo respecto a modelos GLP-multidemostración (Teoremas 6.2, 6.3)

Resultados Constructivos

Construcción exitosa de modelos de demostrabilidad independientes de modelos de Kripke estándar, particularmente:

• Para cualquier marco de árbol irreflexivo bien fundado y cualquier asignación de conjuntos de fórmulas a nodos, puede construirse el modelo de demostrabilidad mínimo
• En el caso bifinito, el modelo construido es decidible

Trabajo Relacionado

Investigación Tradicional en Lógica de Demostrabilidad

• Solovay (1976): Estableció la lógica de demostrabilidad de PA
• Boolos (1995), Smoryński (1985): Textos clásicos en lógica de demostrabilidad
• Artemov y Beklemishev (2004): Encuesta exhaustiva

Enfoques Semánticos

• Semántica de Kripke estándar: Utilizada para varias lógicas modales
• Modelos de Veltman: Utilizados para la lógica de interpretabilidad ILM
• Semántica topológica: Proporciona completitud para GLP

Lógica de Demostrabilidad Intuicionista

• Iemhoff (2001-2003): Introdujo la semántica de Iemhoff
• Mojtahedi (2022): Primer uso de modelos de demostrabilidad para establecer completitud aritmética de lógica de demostrabilidad intuicionista

Conclusiones y Discusión

Conclusiones Principales

1. Marco Unificado: Los modelos de demostrabilidad proporcionan un marco semántico unificado para múltiples lógicas modales
2. Constructividad: Particularmente para GL e ILM, pueden construirse constructivamente modelos de demostrabilidad independientes
3. Decidibilidad: Bajo condiciones apropiadas, los modelos de demostrabilidad son decidibles
4. Flexibilidad: Las condiciones de marco pueden ser reemplazadas por propiedades lógicas, proporcionando mayor flexibilidad

Limitaciones

1. Restricciones de GLP: Para GLP, aún no se ha encontrado una clase de modelos de demostrabilidad decidibles
2. Complejidad de Construcciones: Algunas construcciones (como el modelo canónico de GLP) pueden no ser constructivas
3. Alcance de Aplicabilidad: Se aplica principalmente a lógicas con propiedades de demostrabilidad

Direcciones Futuras

El artículo plantea explícitamente varios problemas abiertos:

1. Extensión de Lógicas de Prueba: Definir modelos de estilo demostrabilidad para lógica de prueba LP y JGL
2. Lógica Modal Intuicionista: Definir modelos de demostrabilidad para lógica modal intuicionista con dos operadores modales □ y ◇
3. Modelos Decidibles de GLP: Buscar clases de modelos de demostrabilidad decidibles para GLP
4. Simplificación de Completitud Aritmética: Explorar si puede simplificarse la prueba de completitud aritmética de ILM mediante modelos de demostrabilidad

Evaluación Profunda

Fortalezas

1. Innovación Teórica: Propone un marco semántico completamente nuevo que unifica el tratamiento de múltiples lógicas modales
2. Profundidad Técnica: Proporciona pruebas matemáticas detalladas y métodos de construcción
3. Valor Práctico: Las mejoras particularmente en decidibilidad tienen importancia significativa
4. Sistematicidad: Trata sistemáticamente desde lógicas modales básicas hasta lógicas de demostrabilidad complejas

Insuficiencias

1. Complejidad: La complejidad de algunas construcciones (particularmente GLP) puede limitar su aplicación práctica
2. Problemas Abiertos: Aún quedan problemas importantes sin resolver, como modelos decidibles para GLP
3. Alcance de Aplicación: Se limita principalmente a investigación teórica, con valor práctico a explorar

Impacto

1. Contribución Teórica: Proporciona una nueva dirección de investigación para la semántica de lógica modal
2. Valor Metodológico: El método de logificación de condiciones de marco tiene significado universal
3. Investigación Posterior: Proporciona nuevas herramientas para investigación en lógica intuicionista, lógica de prueba y otros campos

Escenarios de Aplicabilidad

1. Investigación en Lógica de Demostrabilidad: Particularmente aplicable a investigaciones que requieren completitud aritmética
2. Semántica de Lógica Modal: Proporciona nuevos métodos semánticos para lógicas modales complejas
3. Lógica Computacional: Tiene valor potencial en aplicaciones que requieren decidibilidad

Referencias

El artículo cita literatura relevante abundante, incluyendo:

• Literatura clásica en lógica de demostrabilidad (Boolos, Smoryński, Solovay, etc.)
• Trabajos importantes en semántica de lógica modal (Blackburn, etc.)
• Investigación clave en lógica de interpretabilidad (Berarducci, Shavrukov, etc.)
• Trabajos relacionados en lógica de demostrabilidad intuicionista (Iemhoff, etc.)

Este artículo realiza contribuciones teóricas importantes en el campo de la semántica de lógica modal, proporcionando un nuevo marco unificado para tratar varias lógicas de demostrabilidad, mientras logra avances significativos en constructividad y decidibilidad. Aunque aún quedan algunos problemas abiertos, este trabajo establece una base sólida para investigación posterior.