En lógica , los marcos generales (o simplemente marcos ) son marcos de Kripke con una estructura adicional, que se utilizan para modelar lógicas modales e intermedias . La semántica de marco general combina las principales virtudes de la semántica de Kripke y la semántica algebraica : comparte la percepción geométrica transparente de la primera y la robusta integridad de la segunda.
Definición
Un marco general modal es un triple, dónde es un marco de Kripke (es decir, R es una relación binaria en el conjunto F ), y V es un conjunto de subconjuntos de F que se cierra bajo lo siguiente:
- las operaciones booleanas de intersección (binaria) , unión y complemento ,
- la operacion , definido por .
Por tanto, son un caso especial de campos de conjuntos con estructura adicional . El propósito de V es restringir las valoraciones permitidas en el marco: un modelo basado en el marco Kripke es admisible en el marco general F , si
- para cada variable proposicional p .
Las condiciones de cierre en V aseguran entonces quepertenece a V para cada fórmula A (no solo una variable).
Una fórmula A es válida en F , si para todas las valoraciones admisibles y todos los puntos . Una lógica modal normal de L es válido en el marco F , si todos los axiomas (o equivalentemente, todos los teoremas ) de L son válidos en F . En este caso llamamos F un L - marco .
Un marco de Kripke puede identificarse con un marco general en el que todas las valoraciones son admisibles: es decir, , dónde denota el conjunto potencia de F .
Tipos de marcos
En general, los marcos generales son poco más que un nombre elegante para los modelos Kripke ; en particular, se pierde la correspondencia de los axiomas modales con las propiedades de la relación de accesibilidad. Esto puede remediarse imponiendo condiciones adicionales al conjunto de valoraciones admisibles.
Un cuadro se llama
- diferenciado , si implica ,
- apretado , si implica ,
- compacto , si cada subconjunto de V con la propiedad de intersección finita tiene una intersección no vacía,
- atómico , si V contiene todos los singleton,
- refinado , si es diferenciado y ajustado,
- descriptivo , si es refinado y compacto.
Los marcos de Kripke son refinados y atómicos. Sin embargo, los marcos infinitos de Kripke nunca son compactos. Cada marco atómico o diferenciado finito es un marco Kripke.
Los marcos descriptivos son la clase de marcos más importante debido a la teoría de la dualidad (ver más abajo). Los marcos refinados son útiles como generalización común de marcos descriptivos y de Kripke.
Operaciones y morfismos en marcos
Cada modelo Kripke induce el marco general, donde V se define como
Las operaciones fundamentales de preservación de la verdad de las subtramas generadas, las imágenes p-mórficas y las uniones disjuntas de las tramas de Kripke tienen análogos en las tramas generales. Un cuadroes una subtrama generada de una trama, si el marco Kripke es una subtrama generada de la trama Kripke (es decir, es un subconjunto de cerrado hacia arriba bajo , y ), y
Un p-morfismo (o morfismo acotado )es una función de F a G que es un p-morfismo de los marcos de Kripke y y satisface la restricción adicional
- para cada .
La unión disjunta de un conjunto indexado de marcos, , es el marco , donde F es la unión disjunta de, R es la unión de, y
El refinamiento de un marco es un marco refinado definido como sigue. Consideramos la relación de equivalencia
y deja ser el conjunto de clases de equivalencia de . Entonces ponemos
Lo completo
A diferencia de las tramas de Kripke, toda lógica modal normal L está completa con respecto a una clase de tramas generales. Esto es una consecuencia del hecho de que L es completo con respecto a una clase de modelos de Kripke.: como L se cierra en sustitución, el marco general inducido pores un marco en L. Además, toda lógica L está completa con respecto a un solo marco descriptivo . De hecho, L es completo con respecto a su modelo canónico, y el marco general inducido por el modelo canónico (llamado marco canónico de L ) es descriptivo.
Dualidad Jónsson-Tarski
![](http://wikiimg.tojsiabtv.com/wikipedia/commons/thumb/3/34/Rieger-Nishimura_ladder.svg/100px-Rieger-Nishimura_ladder.svg.png)
![](http://wikiimg.tojsiabtv.com/wikipedia/commons/thumb/5/5c/Rieger-Nishimura.svg/300px-Rieger-Nishimura.svg.png)
Los marcos generales tienen una estrecha conexión con las álgebras modales . Dejarser un marco general. El conjunto V está cerrado bajo operaciones booleanas, por lo tanto es una subálgebra del conjunto de potencias álgebra booleana . También lleva una operación unaria adicional,. La estructura combinadaes un álgebra modal, que se llama álgebra dual de F , y se denota por.
En la dirección opuesta, es posible construir el marco dual a cualquier álgebra modal . El álgebra de Booletiene un espacio de piedra , cuyo conjunto subyacente F es el conjunto de todos los ultrafiltros de A . El conjunto V de valoraciones admisibles enconsta de los abiertos y cerrados subconjuntos de F , y la relación de accesibilidad R se define por
para todos los ultrafiltros x y y .
Un marco y su dual validan las mismas fórmulas, por lo que la semántica general del marco y la semántica algebraica son en cierto sentido equivalentes. El doble dual de cualquier álgebra modal es isomórfica a sí mismo. Esto no es cierto en general para dobles duales de marcos, ya que el dual de cada álgebra es descriptivo. De hecho, un marco es descriptivo si y solo si es isomorfo a su doble dual dual .
También es posible definir duales de p-morfismos por un lado y homomorfismos de álgebra modal por otro lado. De esta forma los operadores y se convierten en un par de functores contravariantes entre la categoría de marcos generales y la categoría de álgebras modales. Estos functores proporcionan una dualidad (llamada dualidad de Jónsson-Tarski por Bjarni Jónsson y Alfred Tarski ) entre las categorías de marcos descriptivos y álgebras modales. Este es un caso especial de una dualidad más general entre álgebras complejas y campos de conjuntos en estructuras relacionales .
Marcos intuicionistas
La semántica del marco para lógicas intuicionistas e intermedias se puede desarrollar en paralelo a la semántica para lógicas modales. Un marco general intuicionista es un triple, dónde es un orden parcial en F , y V es un conjunto de subconjuntos superiores ( conos ) de F que contiene el conjunto vacío, y está cerrado bajo
- intersección y unión,
- la operacion .
Luego, la validez y otros conceptos se introducen de manera similar a los marcos modales, con algunos cambios necesarios para adaptarse a las propiedades de cierre más débiles del conjunto de valoraciones admisibles. En particular, un marco intuicionista se llama
- apretado , si implica ,
- compacto , si cada subconjunto de con la propiedad de intersección finita tiene una intersección no vacía.
Los marcos intuicionistas estrictos se diferencian automáticamente y, por lo tanto, se refinan.
El dual de un marco intuicionista es el álgebra de Heyting . El dual de un álgebra de Heyting es el marco intuicionista , donde F es el conjunto de todos los filtros principales de A , el ordenes inclusión , y V consta de todos los subconjuntos de F de la forma
dónde . Como en el caso modal, y son un par de functores contravariantes, que hacen que la categoría de álgebras de Heyting sea doblemente equivalente a la categoría de marcos intuicionistas descriptivos.
Es posible construir marcos generales intuicionistas a partir de marcos modales reflexivos transitivos y viceversa, ver compañero modal .
Referencias
- Alexander Chagrov y Michael Zakharyaschev, Modal Logic , vol. 35 de Oxford Logic Guides, Oxford University Press, 1997.
- Patrick Blackburn, Maarten de Rijke y Yde Venema, Modal Logic , vol. 53 de Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001.