Marco general

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 marcos generales combina las principales virtudes de la semántica de Kripke y la semántica algebraica : comparte la visión geométrica transparente de la primera y la robusta completitud de la segunda.

Definición

Un marco general modal es un triple , donde es un marco de Kripke (es decir, es una relación binaria en el conjunto ), y es un conjunto de subconjuntos de que está cerrado bajo lo siguiente: ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$ ${\displaystyle \langle F,R\rangle }$ ${\displaystyle R}$ ${\displaystyle F}$ ${\displaystyle V}$ ${\displaystyle F}$

• las operaciones booleanas de intersección (binaria) , unión y complemento ,
• la operación , definida por . ${\displaystyle \Box }$ ${\displaystyle \Box A=\{x\in F\mid \forall y\in F\,(x\,R\,y\to y\in A)\}}$

Son, por tanto, un caso especial de cuerpos de conjuntos con estructura adicional . El propósito de es restringir las valoraciones permitidas en el marco: un modelo basado en el marco de Kripke es admisible en el marco general , si ${\displaystyle V}$ ${\displaystyle \langle F,R,\Vdash \rangle }$ ${\displaystyle \langle F,R\rangle }$ ${\displaystyle \mathbf {F} }$

${\displaystyle \{x\in F\mid x\Vdash p\}\in V}$para cada variable proposicional . ${\displaystyle p}$

Las condiciones de cierre entonces garantizan que pertenece a cada fórmula ( no solo a una variable). ${\displaystyle V}$ ${\displaystyle \{x\in F\mid x\Vdash A\}}$ ${\displaystyle V}$ ${\displaystyle A}$

Una fórmula es válida en , si para todas las valoraciones admisibles , y todos los puntos . Una lógica modal normal es válida en el marco , si todos los axiomas (o equivalentemente, todos los teoremas ) de son válidos en . En este caso, llamamos a un - marco . ${\displaystyle A}$ ${\displaystyle \mathbf {F} }$ ${\displaystyle x\Vdash A}$ ${\displaystyle \Vdash }$ ${\displaystyle x\in F}$ ${\displaystyle L}$ ${\displaystyle \mathbf {F} }$ ${\displaystyle L}$ ${\displaystyle \mathbf {F} }$ ${\displaystyle \mathbf {F} }$ ${\displaystyle L}$

Un marco de Kripke puede identificarse con un marco general en el que todas las valoraciones son admisibles, es decir, , donde denota el conjunto potencia de . ${\displaystyle \langle F,R\rangle }$ ${\displaystyle \langle F,R,{\mathcal {P}}(F)\rangle }$ ${\displaystyle {\mathcal {P}}(F)}$ ${\displaystyle F}$

Tipos de marcos

En términos generales, los marcos generales no son más que un nombre elegante para los modelos de Kripke ; en particular, se pierde la correspondencia de los axiomas modales con las propiedades de la relación de accesibilidad. Esto se puede remediar imponiendo condiciones adicionales al conjunto de valoraciones admisibles.

Un marco se llama ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$

• diferenciado , si implica , ${\displaystyle \forall A\in V\,(x\in A\Leftrightarrow y\in A)}$ ${\displaystyle x=y}$
• apretado , si implica , ${\displaystyle \forall A\in V\,(x\in \Box A\Rightarrow y\in A)}$ ${\displaystyle x\,R\,y}$
• compacto , si cada subconjunto de con la propiedad de intersección finita tiene una intersección no vacía, ${\displaystyle V}$
• atómico , si contiene todos los singletons, ${\displaystyle V}$
• refinado , si es diferenciado y estricto,
• descriptivo , si es refinado y compacto.

Los marcos de Kripke son refinados y atómicos. Sin embargo, los marcos de Kripke infinitos nunca son compactos. Todo marco finito diferenciado o atómico es un marco de Kripke.

Los marcos descriptivos son la clase más importante de marcos debido a la teoría de la dualidad (ver más abajo). Los marcos refinados son útiles como una generalización común de los marcos descriptivos y de Kripke.

Operaciones y morfismos sobre cuadros

Todo modelo de Kripke induce el marco general , donde se define como ${\displaystyle \langle F,R,{\Vdash }\rangle }$ ${\displaystyle \langle F,R,V\rangle }$ ${\displaystyle V}$

${\displaystyle V={\big \{}\{x\in F\mid x\Vdash A\}\mid A{\hbox{ is a formula}}{\big \}}.}$

Las operaciones fundamentales de conservación de la verdad de los submarcos generados, las imágenes p-mórficas y las uniones disjuntas de los marcos de Kripke tienen analogías en los marcos generales. Un marco es un submarco generado de un marco , si el marco de Kripke es un submarco generado del marco de Kripke (es decir, es un subconjunto de cerrado hacia arriba bajo , y ), y ${\displaystyle \mathbf {G} =\langle G,S,W\rangle }$ ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$ ${\displaystyle \langle G,S\rangle }$ ${\displaystyle \langle F,R\rangle }$ ${\displaystyle G}$ ${\displaystyle F}$ ${\displaystyle R}$ ${\displaystyle S=R\cap G\times G}$

${\displaystyle W=\{A\cap G\mid A\in V\}.}$

Un p-morfismo (o morfismo acotado ) es una función de a que es un p-morfismo de los marcos de Kripke y , y satisface la restricción adicional ${\displaystyle f\colon \mathbf {F} \to \mathbf {G} }$ ${\displaystyle F}$ ${\displaystyle G}$ ${\displaystyle \langle F,R\rangle }$ ${\displaystyle \langle G,S\rangle }$

${\displaystyle f^{-1}[A]\in V}$para cada . ${\displaystyle A\in W}$

La unión disjunta de un conjunto indexado de marcos , , es el marco , donde es la unión disjunta de , es la unión de , y ${\displaystyle \mathbf {F} _{i}=\langle F_{i},R_{i},V_{i}\rangle }$ ${\displaystyle i\in I}$ ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$ ${\displaystyle F}$ ${\displaystyle \{F_{i}\mid i\in I\}}$ ${\displaystyle R}$ ${\displaystyle \{R_{i}\mid i\in I\}}$

${\displaystyle V=\{A\subseteq F\mid \forall i\in I\,(A\cap F_{i}\in V_{i})\}.}$

El refinamiento de un marco es un marco refinado definido de la siguiente manera. Consideramos la relación de equivalencia ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$ ${\displaystyle \mathbf {G} =\langle G,S,W\rangle }$

${\displaystyle x\sim y\iff \forall A\in V\,(x\in A\Leftrightarrow y\in A),}$

y sea el conjunto de clases de equivalencia de . Entonces ponemos ${\displaystyle G=F/{\sim }}$ ${\displaystyle \sim }$

${\displaystyle \langle x/{\sim },y/{\sim }\rangle \in S\iff \forall A\in V\,(x\in \Box A\Rightarrow y\in A),}$

${\displaystyle A/{\sim }\in W\iff A\in V.}$

Lo completo

A diferencia de los marcos de Kripke, toda lógica modal normal es completa con respecto a una clase de marcos generales. Esto es una consecuencia del hecho de que es completa con respecto a una clase de modelos de Kripke : como es cerrada bajo sustitución, el marco general inducido por es un marco -. Además, toda lógica es completa con respecto a un único marco descriptivo . De hecho, es completa con respecto a su modelo canónico, y el marco general inducido por el modelo canónico (llamado marco canónico de ) es descriptivo. ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle \langle F,R,{\Vdash }\rangle }$ ${\displaystyle L}$ ${\displaystyle \langle F,R,{\Vdash }\rangle }$ ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle L}$

La dualidad Jónsson-Tarski

La escalera de Rieger-Nishimura: un marco Kripke intuicionista 1-universal.

Su álgebra dual de Heyting, la red de Rieger-Nishimura, es el álgebra de Heyting libre sobre 1 generador.

Los marcos generales tienen una estrecha relación con las álgebras modales . Sea un marco general. El conjunto está cerrado respecto de las operaciones booleanas, por lo tanto es una subálgebra del conjunto potencia Álgebra de Boole . También conlleva una operación unaria adicional, . La estructura combinada es un álgebra modal, que se denomina álgebra dual de , y se denota por . ${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$ ${\displaystyle V}$ ${\displaystyle \langle {\mathcal {P}}(F),\cap ,\cup ,-\rangle }$ ${\displaystyle \Box }$ ${\displaystyle \langle V,\cap ,\cup ,-,\Box \rangle }$ ${\displaystyle \mathbf {F} }$ ${\displaystyle \mathbf {F} ^{+}}$

En la dirección opuesta, es posible construir el marco dual para cualquier álgebra modal . El álgebra de Boole tiene un espacio de Stone , cuyo conjunto subyacente es el conjunto de todos los ultrafiltros de . El conjunto de valoraciones admisibles en consiste en los subconjuntos clopen de , y la relación de accesibilidad está definida por ${\displaystyle \mathbf {A} _{+}=\langle F,R,V\rangle }$ ${\displaystyle \mathbf {A} =\langle A,\wedge ,\vee ,-,\Box \rangle }$ ${\displaystyle \langle A,\wedge ,\vee ,-\rangle }$ ${\displaystyle F}$ ${\displaystyle \mathbf {A} }$ ${\displaystyle V}$ ${\displaystyle \mathbf {A} _{+}}$ ${\displaystyle F}$ ${\displaystyle R}$

${\displaystyle x\,R\,y\iff \forall a\in A\,(\Box a\in x\Rightarrow a\in y)}$

para todos los ultrafiltros y . ${\displaystyle x}$ ${\displaystyle y}$

Un marco y su dual validan las mismas fórmulas; por lo tanto, la semántica general del marco y la semántica algebraica son en cierto sentido equivalentes. El dual doble de cualquier álgebra modal es isomorfo a sí mismo. Esto no es cierto en general para los duales dobles 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 dual doble . ${\displaystyle (\mathbf {A} _{+})^{+}}$ ${\displaystyle \mathbf {A} }$ ${\displaystyle \mathbf {F} }$ ${\displaystyle (\mathbf {F} ^{+})_{+}}$

También es posible definir duales de p-morfismos por un lado, y homomorfismos de álgebras modales por otro. De esta manera, los operadores y se convierten en un par de funtores contravariantes entre la categoría de marcos generales y la categoría de álgebras modales. Estos funtores proporcionan una dualidad (llamada dualidad de Jónsson-Tarski en honor a 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 cuerpos de conjuntos en estructuras relacionales . ${\displaystyle (\cdot )^{+}}$ ${\displaystyle (\cdot )_{+}}$

Marcos intuicionistas

La semántica de marcos para lógicas intuicionistas e intermedias se puede desarrollar en paralelo a la semántica para lógicas modales. Un marco general intuicionista es una tripleta , donde es un orden parcial en , y es un conjunto de subconjuntos superiores ( conos ) de que contiene el conjunto vacío, y está cerrado bajo ${\displaystyle \langle F,\leq ,V\rangle }$ ${\displaystyle \leq }$ ${\displaystyle F}$ ${\displaystyle V}$ ${\displaystyle F}$

• intersección y unión,
• La operación . ${\displaystyle A\to B=\Box (-A\cup B)}$

La validez y otros conceptos se introducen de manera similar a los marcos modales, con algunos cambios necesarios para dar cabida a las propiedades de cierre más débiles del conjunto de valoraciones admisibles. En particular, un marco intuicionista se denomina ${\displaystyle \mathbf {F} =\langle F,\leq ,V\rangle }$

• apretado , si implica , ${\displaystyle \forall A\in V\,(x\in A\Leftrightarrow y\in A)}$ ${\displaystyle x\leq y}$
• compacto , si cada subconjunto de con la propiedad de intersección finita tiene una intersección no vacía. ${\displaystyle V\cup \{F-A\mid A\in V\}}$

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 es el conjunto de todos los filtros primos de , el orden es inclusión , y consta de todos los subconjuntos de de la forma ${\displaystyle \mathbf {F} =\langle F,\leq ,V\rangle }$ ${\displaystyle \mathbf {F} ^{+}=\langle V,\cap ,\cup ,\to ,\emptyset \rangle }$ ${\displaystyle \mathbf {A} =\langle A,\wedge ,\vee ,\to ,0\rangle }$ ${\displaystyle \mathbf {A} _{+}=\langle F,\leq ,V\rangle }$ ${\displaystyle F}$ ${\displaystyle \mathbf {A} }$ ${\displaystyle \leq }$ ${\displaystyle V}$ ${\displaystyle F}$

${\displaystyle \{x\in F\mid a\in x\},}$

donde . Como en el caso modal, y son un par de funtores contravariantes, que hacen que la categoría de álgebras de Heyting sea dualmente equivalente a la categoría de marcos intuicionistas descriptivos. ${\displaystyle a\in A}$ ${\displaystyle (\cdot )^{+}}$ ${\displaystyle (\cdot )_{+}}$

Es posible construir marcos generales intuicionistas a partir de marcos modales reflexivos transitivos y viceversa, ver compañero modal .

Véase también

• Semántica de barrio

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.