stringtranslate.com

Semántica de Kripke

La semántica de Kripke (también conocida como semántica relacional o semántica de marcos , y a menudo confundida con la semántica de mundos posibles ) [1] es una semántica formal para sistemas lógicos no clásicos creada a fines de la década de 1950 y principios de la de 1960 por Saul Kripke y André Joyal . Primero fue concebida para lógicas modales , y luego adaptada a la lógica intuicionista y otros sistemas no clásicos. El desarrollo de la semántica de Kripke fue un gran avance en la teoría de las lógicas no clásicas, porque la teoría de modelos de tales lógicas era casi inexistente antes de Kripke (la semántica algebraica existía, pero se consideraba 'sintaxis disfrazada').

Semántica de la lógica modal

El lenguaje de la lógica modal proposicional consiste en un conjunto infinito numerable de variables proposicionales , un conjunto de conectores veritativo-funcionales (en este artículo y ), y el operador modal ("necesariamente"). El operador modal ("posiblemente") es (clásicamente) el dual de y puede definirse en términos de necesidad de la siguiente manera: ("posiblemente A" se define como equivalente a "no necesariamente no A"). [2]

Definiciones básicas

Un marco de Kripke o marco modal es un par , donde W es un conjunto (posiblemente vacío) y R es una relación binaria en W. Los elementos de W se denominan nodos o mundos , y R se conoce como la relación de accesibilidad . [3]

Un modelo de Kripke es un triple , [4] donde es un marco de Kripke, y es una relación entre nodos de W y fórmulas modales, tal que para todo w  ∈  W y fórmulas modales A y B :

Leemos como “ w satisface A ”, “ A se satisface en w ” o “ w fuerza a A ”. La relación se llama relación de satisfacción , evaluación o relación de forzamiento . La relación de satisfacción está determinada únicamente por su valor en variables proposicionales.

Una fórmula A es válida en:

Definimos Thm( C ) como el conjunto de todas las fórmulas que son válidas en C . Por el contrario, si X es un conjunto de fórmulas, sea Mod( X ) la clase de todos los marcos que validan cada fórmula de X .

Una lógica modal (es decir, un conjunto de fórmulas) L es válida con respecto a una clase de marcos C , si L  ⊆ Thm( C ). L es completa con respecto a C si L  ⊇ Thm( C ).

Correspondencia y completitud

La semántica es útil para investigar una lógica (es decir, un sistema de derivación ) sólo si la relación de consecuencia semántica refleja su contraparte sintáctica, la relación de consecuencia sintáctica ( derivabilidad ). [5] Es vital saber qué lógicas modales son sólidas y completas con respecto a una clase de marcos de Kripke, y determinar también qué clase es esa.

Para cualquier clase C de sistemas Kripkeanos, Thm( C ) es una lógica modal normal (en particular, los teoremas de la lógica modal normal mínima, K , son válidos en cada modelo Kripkeano). Sin embargo, lo inverso no se cumple en general: mientras que la mayoría de los sistemas modales estudiados están completos de clases de sistemas descriptos por condiciones simples, existen lógicas modales normales incompletas de Kripkeano. Un ejemplo natural de un sistema de este tipo es la lógica polimodal de Japaridze .

Una lógica modal normal L corresponde a una clase de marcos C , si C  = Mod( L ). En otras palabras, C es la clase más grande de marcos tal que L es sólida con respecto a C . De ello se deduce que L es completa en términos de Kripke si y solo si es completa en su clase correspondiente.

Considérese el esquema T  : . T es válido en cualquier marco reflexivo : si , entonces como w R w . Por otra parte, un marco que valida T tiene que ser reflexivo: fijar w  ∈  W , y definir la satisfacción de una variable proposicional p de la siguiente manera: si y sólo si w R u . Entonces , por tanto por T , lo que significa w R w usando la definición de . T corresponde a la clase de marcos reflexivos de Kripke.      

A menudo es mucho más fácil caracterizar la clase correspondiente de L que probar su completitud, por lo que la correspondencia sirve como guía para las pruebas de completitud. La correspondencia también se utiliza para mostrar la incompletitud de las lógicas modales: supongamos que L 1  ⊆  L 2 son lógicas modales normales que corresponden a la misma clase de marcos, pero L 1 no prueba todos los teoremas de L 2 . Entonces L 1 es incompleto en el sentido de Kripke. Por ejemplo, el esquema genera una lógica incompleta, ya que corresponde a la misma clase de marcos que GL (es decir, marcos bien fundados transitivos y conversos), pero no prueba la tautología GL .

Esquemas de axiomas modales comunes

La siguiente tabla enumera los axiomas modales comunes junto con sus clases correspondientes. La denominación de los axiomas suele variar; aquí, el axioma K recibe su nombre de Saul Kripke ; el axioma T recibe su nombre del axioma de verdad en lógica epistémica ; el axioma D recibe su nombre de la lógica deóntica ; el axioma B recibe su nombre de LEJ Brouwer ; y los axiomas 4 y 5 reciben su nombre de acuerdo con la numeración de sistemas de lógica simbólica de CI Lewis .

El axioma K también puede reescribirse como , lo que establece lógicamente el modus ponens como una regla de inferencia en cada mundo posible.

Nótese que para el axioma D , implica implícitamente , lo que significa que para cada mundo posible en el modelo, siempre hay al menos un mundo posible accesible desde él (que podría ser él mismo). Esta implicación implícita es similar a la implicación implícita del cuantificador existencial en el rango de cuantificación .

Sistemas modales comunes

En la siguiente tabla se enumeran varios sistemas modales normales comunes. Las condiciones marco de algunos de los sistemas se simplificaron: la lógica es correcta y completa con respecto a las clases de marcos que se indican en la tabla, pero pueden corresponder a una clase más amplia de marcos.

Modelos canónicos

Para cualquier lógica modal normal, L , se puede construir un modelo de Kripke (llamado modelo canónico ) que refute con precisión los no teoremas de L , mediante una adaptación de la técnica estándar de utilizar conjuntos consistentes máximos como modelos. Los modelos canónicos de Kripke desempeñan un papel similar a la construcción del álgebra de Lindenbaum-Tarski en la semántica algebraica.

Un conjunto de fórmulas es L - consistente si no se puede derivar ninguna contradicción de él utilizando los teoremas de L y Modus Ponens. Un conjunto L-consistente máximo (un L - MCS para abreviar) es un conjunto L -consistente que no tiene un superconjunto L -consistente propio .

El modelo canónico de L es un modelo de Kripke , donde W es el conjunto de todos los L - MCS , y las relaciones R y son las siguientes:

si y solo si para cada fórmula , si entonces ,
si y sólo si .

El modelo canónico es un modelo de L , ya que cada L - MCS contiene todos los teoremas de L . Por el lema de Zorn , cada conjunto L -consistente está contenido en un L - MCS , en particular cada fórmula indemostrable en L tiene un contraejemplo en el modelo canónico.

La principal aplicación de los modelos canónicos son las pruebas de completitud. Las propiedades del modelo canónico de K implican inmediatamente la completitud de K con respecto a la clase de todos los marcos de Kripke. Este argumento no funciona para un L arbitrario , porque no hay garantía de que el marco subyacente del modelo canónico satisfaga las condiciones de marco de L.

Decimos que una fórmula o un conjunto X de fórmulas es canónica con respecto a una propiedad P de los marcos de Kripke, si

Una unión de conjuntos canónicos de fórmulas es en sí misma canónica. De la discusión anterior se desprende que cualquier lógica axiomatizada por un conjunto canónico de fórmulas es completa según Kripke y compacta .

Los axiomas T, 4, D, B, 5, H, G (y, por tanto, cualquier combinación de ellos) son canónicos. GL y Grz no son canónicos, porque no son compactos. El axioma M por sí mismo no es canónico (Goldblatt, 1991), pero la lógica combinada S4.1 (de hecho, incluso K4.1 ) sí lo es.

En general, es indecidible si un axioma dado es canónico. Conocemos una buena condición suficiente: Henrik Sahlqvist identificó una amplia clase de fórmulas (ahora llamadas fórmulas de Sahlqvist ) tales que

Éste es un criterio poderoso: por ejemplo, todos los axiomas enumerados anteriormente como canónicos son (equivalentes a) fórmulas de Sahlqvist.

Propiedad del modelo finito

Una lógica tiene la propiedad de modelo finito (FMP) si es completa con respecto a una clase de marcos finitos. Una aplicación de esta noción es la cuestión de decidibilidad : del teorema de Post se deduce que una lógica modal recursivamente axiomatizada L que tiene FMP es decidible, siempre que sea decidible si un marco finito dado es un modelo de L . En particular, toda lógica finitamente axiomatizable con FMP es decidible.

Existen varios métodos para establecer el FMP para una lógica dada. Los refinamientos y extensiones de la construcción del modelo canónico suelen funcionar, utilizando herramientas como la filtración o el desenredo. Como otra posibilidad, las pruebas de completitud basadas en cálculos de secuencias sin cortes suelen producir modelos finitos directamente.

La mayoría de los sistemas modales utilizados en la práctica (incluidos todos los enumerados anteriormente) tienen FMP.

En algunos casos, podemos usar FMP para probar la completitud de Kripke de una lógica: toda lógica modal normal es completa con respecto a una clase de álgebras modales , y un álgebra modal finita se puede transformar en un marco de Kripke. Como ejemplo, Robert Bull demostró usando este método que toda extensión normal de S4.3 tiene FMP y es completa de Kripke.

Lógica multimodal

La semántica de Kripke tiene una generalización directa a lógicas con más de una modalidad. Un marco de Kripke para un lenguaje con como el conjunto de sus operadores de necesidad consiste en un conjunto no vacío W equipado con relaciones binarias R i para cada i  ∈  I . La definición de una relación de satisfacción se modifica de la siguiente manera:

Si y sólo si

Una semántica simplificada, descubierta por Tim Carlson, se utiliza a menudo para lógicas de demostrabilidad polimodal . Un modelo de Carlson es una estructura con una única relación de accesibilidad R y subconjuntos D i  ⊆  W para cada modalidad. La satisfacción se define como

Si y sólo si

Los modelos de Carlson son más fáciles de visualizar y trabajar con ellos que los modelos polimodales Kripke habituales; sin embargo, existen lógicas polimodales completas de Kripke que son incompletas desde el punto de vista de Carlson.

Semántica de la lógica intuicionista

La semántica de Kripke para la lógica intuicionista sigue los mismos principios que la semántica de la lógica modal, pero utiliza una definición diferente de satisfacción.

Un modelo Kripke intuicionista es un triple , donde es un marco Kripke preordenado , y satisface las siguientes condiciones: [7]

La negación de A , ¬ A , podría definirse como una abreviatura de A → ⊥. Si para todo u tal que wu , no u A , entonces w A → ⊥ es vacuamente verdadero , por lo que w ¬ A .

La lógica intuicionista es sólida y completa con respecto a su semántica de Kripke, y tiene la propiedad del modelo finito .

Lógica intuicionista de primer orden

Sea L un lenguaje de primer orden . Un modelo Kripke de L es una tripleta , donde es un marco Kripke intuicionista, M w es una L -estructura (clásica) para cada nodo w  ∈  W , y las siguientes condiciones de compatibilidad se cumplen siempre que u  ≤  v :

Dada una evaluación e de variables por elementos de M w , definimos la relación de satisfacción :

Aquí e ( xa ) es la evaluación que da a x el valor a , y por lo demás concuerda con e . [8]

Semántica de Kripke-Joyal

Como parte del desarrollo independiente de la teoría de haces , alrededor de 1965 se advirtió que la semántica de Kripke estaba íntimamente relacionada con el tratamiento de la cuantificación existencial en la teoría de topos . [9] Es decir, el aspecto "local" de la existencia para las secciones de un haz era una especie de lógica de lo "posible". Aunque este desarrollo fue obra de varias personas, el nombre de semántica de Kripke-Joyal se utiliza a menudo en este contexto.

Construcciones de modelos

Al igual que en la teoría de modelos clásicos , existen métodos para construir un nuevo modelo de Kripke a partir de otros modelos.

Los homomorfismos naturales en la semántica de Kripke se denominan p-morfismos (que es la abreviatura de pseudoepimorfismo , pero este último término rara vez se utiliza). Un p-morfismo de los marcos de Kripke y es una aplicación tal que

Un p-morfismo de los modelos de Kripke y es un p-morfismo de sus marcos subyacentes , que satisface

si y sólo si , para cualquier variable proposicional p .

Los p-morfismos son un tipo especial de bisimulaciones . En general, una bisimulación entre los marcos y es una relación B ⊆ W × W' , que satisface la siguiente propiedad de “zigzag”:

Además, se requiere una bisimulación de modelos para preservar el forzamiento de las fórmulas atómicas :

si w B w' , entonces si y sólo si , para cualquier variable proposicional p .

La propiedad clave que se desprende de esta definición es que las bisimulaciones (y por tanto también los p-morfismos) de modelos preservan la satisfacción de todas las fórmulas, no sólo de las variables proposicionales.

Podemos transformar un modelo de Kripke en un árbol utilizando desenredado . Dado un modelo y un nodo fijo w 0  ∈  W , definimos un modelo , donde W' es el conjunto de todas las secuencias finitas tales que w i  R w i+1 para todo i  <  n , y si y solo si para una variable proposicional p . La definición de la relación de accesibilidad R' varía; en el caso más simple, ponemos

,

pero muchas aplicaciones necesitan el cierre reflexivo y/o transitivo de esta relación, o modificaciones similares.

La filtración es una construcción útil que se utiliza para demostrar FMP para muchas lógicas. Sea X un conjunto de fórmulas cerradas bajo la toma de subfórmulas. Una X -filtración de un modelo es una aplicación f de W a un modelo tal que

De ello se deduce que f preserva la satisfacción de todas las fórmulas de X. En aplicaciones típicas, tomamos f como la proyección sobre el cociente de W sobre la relación

u ≡ X  v si y solo si para todo A  ∈  X , si y solo si .

Al igual que en el caso del desenredo, la definición de la relación de accesibilidad en el cociente varía.

Semántica general de los marcos

El principal defecto de la semántica de Kripke es la existencia de lógicas incompletas de Kripke y lógicas que son completas pero no compactas. Esto se puede remediar dotando a los marcos de Kripke de una estructura adicional que restrinja el conjunto de posibles valoraciones, utilizando ideas de la semántica algebraica. Esto da lugar a la semántica de marcos generales .

Aplicaciones de la informática

Blackburn et al. (2001) señalan que, puesto que una estructura relacional es simplemente un conjunto junto con una colección de relaciones en ese conjunto, no es sorprendente que las estructuras relacionales se encuentren prácticamente en todas partes. Como ejemplo de la informática teórica , dan los sistemas de transición etiquetados , que modelan la ejecución del programa . Blackburn et al. afirman, por tanto, debido a esta conexión, que los lenguajes modales son ideales para proporcionar una "perspectiva interna y local sobre las estructuras relacionales" (p. xii).

Historia y terminología

Trabajo similar que precedió a los avances semánticos revolucionarios de Kripke: [10]

Véase también

Notas

  1. ^ La semántica de mundos posibles es un término más amplio que abarca varios enfoques, incluida la semántica de Kripke. Generalmente se refiere a la idea de analizar enunciados modales considerando mundos posibles alternativos donde diferentes proposiciones son verdaderas o falsas. Si bien la semántica de Kripke es un tipo específico de semántica de mundos posibles, existen otras formas de modelar mundos posibles y sus relaciones. La semántica de Kripke es una forma específica de semántica de mundos posibles que emplea estructuras relacionales para representar las relaciones entre mundos posibles y proposiciones en lógica modal. [ cita requerida ]
  2. ^ Shoham y Leyton-Brown 2008.
  3. ^ Gasquet y otros. 2013, págs. 14-16.
  4. ^ Nótese que la noción de 'modelo' en la semántica Kripke de la lógica modal difiere de la noción de 'modelo' en las lógicas no modales clásicas: En las lógicas clásicas decimos que alguna fórmula F tiene un 'modelo' si existe alguna 'interpretación' de las variables de F que hace que la fórmula F sea verdadera; esta interpretación específica es entonces un modelo de la fórmula F. En la semántica Kripke de la lógica modal, por el contrario, un 'modelo' no es un 'algo' específico que hace que una fórmula modal específica sea verdadera; en la semántica Kripke un 'modelo' debe entenderse más bien como un universo más amplio de discurso dentro del cual cualquier fórmula modal puede ser 'entendida' significativamente. Así: mientras que la noción de 'tiene un modelo' en la lógica no modal clásica se refiere a alguna fórmula individual dentro de esa lógica, la noción de 'tiene un modelo' en la lógica modal se refiere a la lógica misma como un todo (es decir: el sistema entero de sus axiomas y reglas de deducción).
  5. ^ Giaquinto 2002.
  6. ^ Según Andrzej Grzegorczyk .
  7. ^ Simpson 1994, p. 20, 2.2 La semántica de la lógica intuicionista.
  8. ^ Véase una formalización ligeramente diferente en Moschovakis (2022)
  9. ^ García-García y García-García 2006b.
  10. ^ Stokhof 2008, Véanse los dos últimos párrafos de la Sección 3 Interludio cuasihistórico: el camino de Viena a Los Ángeles .

Referencias

Enlaces externos