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 finales de los años 1950 y principios de los 1960 por Saul Kripke y André Joyal . Primero fue concebido para la lógica modal y luego adaptado 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 la lógica no clásica, porque la teoría modelo de dicha lógica era casi inexistente antes de Kripke (la semántica algebraica existía, pero se consideraba una "sintaxis disfrazada").

Semántica de la lógica modal.

El lenguaje de la lógica modal proposicional consta de un conjunto infinitamente numerable de variables proposicionales , un conjunto de conectivos funcionales de verdad (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 así: ("posiblemente A" se define como equivalente a "no necesariamente no A"). [2]

Definiciones basicas

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 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 :

Se lee 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 las 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 está completo con respecto a C si L  ⊇ Thm( C ).

Correspondencia e integridad

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 marcos de Kripke, 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 todos los modelos de Kripke). Sin embargo, lo contrario no se cumple en general: si bien la mayoría de los sistemas modales estudiados están completos de clases de marcos descritos por condiciones simples, existen lógicas modales normales incompletas de Kripke. Un ejemplo natural de tal sistema es la lógica polimodal de Japaridze .

Una lógica modal normal L corresponde a una clase de tramas C , si C  = Mod( L ). En otras palabras, C es la clase más grande de fotogramas, de modo que L es sonido frente a C. Se deduce que L es Kripke completo si y sólo si está completo en su clase correspondiente.

Considere el esquema T  : .T es válido en cualquier marco reflexivo : si , entonces desde w R w . Por otro lado, 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 lo tanto, por T , 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 demostrar su integridad, por lo que la correspondencia sirve como guía para las pruebas de integridad. 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 Kripke incompleto. Por ejemplo, el esquema genera una lógica incompleta, ya que corresponde a la misma clase de marcos que GL (es decir, marcos transitivos y conversos bien fundamentados), 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 lleva el nombre de Saul Kripke ; el axioma T lleva el nombre del axioma de verdad en la lógica epistémica ; el axioma D lleva el nombre de la lógica deóntica ; el axioma B lleva el nombre de LEJ Brouwer ; y los axiomas 4 y 5 se nombran basándose en la numeración de sistemas lógicos simbólicos de CI Lewis .

El axioma K también se puede reescribir como , que establece lógicamente el modus ponens como regla de inferencia en todos los mundos posibles.

Tenga en cuenta 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

La siguiente tabla enumera varios sistemas modales normales comunes. Las condiciones de marco para algunos de los sistemas se simplificaron: la lógica es sólida y completa con respecto a las clases de marco dadas en la tabla, pero pueden corresponder a una clase de marco más grande.

Modelos canónicos

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

Un conjunto de fórmulas es consistente con L si no se puede derivar de él ninguna contradicción 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 adecuado.

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 sólo si para cada fórmula , si entonces ,
si y solo si .

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

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

Decimos que una fórmula o un conjunto X de fórmulas es canónico 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 Kripke completa 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í solo no es canónico (Goldblatt, 1991), pero la lógica combinada S4.1 (de hecho, incluso K4.1 ) sí es canónica.

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

Este 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 la 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 FMP para una lógica determinada. Los refinamientos y ampliaciones de la construcción del modelo canónico a menudo funcionan, utilizando herramientas como la filtración o el desenredado. Como otra posibilidad, las pruebas de completitud basadas en cálculos secuenciales 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 demostrar 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ó utilizando este método que cada extensión normal de S4.3 tiene FMP y está completa con Kripke.

Lógicas multimodales

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

si y solo 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 Di W para cada modalidad. La satisfacción se define como

si y solo si

Los modelos Carlson son más fáciles de visualizar y trabajar que los modelos polimodales habituales de Kripke; Sin embargo, existen lógicas polimodales completas de Kripke que son incompletas 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 intuicionista de Kripke es un triple , donde es un marco de Kripke reservado 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 cierto , entonces 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 de Kripke de L es un triple , donde es un marco de Kripke intuicionista, M w es una estructura L (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 le da a x el valor a , y por lo demás concuerda con e . [8]

Kripke-Semántica de la alegría

Como parte del desarrollo independiente de la teoría de la gavilla , alrededor de 1965 se comprendió que la semántica de Kripke estaba íntimamente relacionada con el tratamiento de la cuantificación existencial en la teoría del topos . [9] Es decir, el aspecto "local" de la existencia de 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 sentido.

Construcciones modelo

Como en la teoría de modelos clásica , 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 un mapeo 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 morfismos P son un tipo especial de bisimulaciones . En general, una bisimulación entre fotogramas y es una relación B ⊆ W × W' , que satisface la siguiente propiedad de “zig-zag”:

Además, se requiere una bisimulación de modelos para preservar el forzamiento de 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 (de ahí 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 usando desentrañar . 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 sólo si para un proposicional variablep .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 probar FMP para muchas lógicas. Sea X un conjunto de fórmulas cerradas tomando subfórmulas. Una filtración X de un modelo es un mapeo 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 sólo si para todo A  ∈  X , si y sólo si .

Como en el caso de desentrañar, la definición de la relación de accesibilidad sobre el cociente varía.

Semántica general del marco

El principal defecto de la semántica de Kripke es la existencia de lógicas Kripke incompletas y lógicas completas pero no compactas. Puede remediarse equipando los marcos de Kripke con una estructura adicional que restrinja el conjunto de valoraciones posibles, utilizando ideas de la semántica algebraica. Esto da lugar a la semántica general del marco .

Aplicaciones informáticas

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

Historia y terminología

Trabajo similar anterior a los revolucionarios avances semánticos de Kripke: [10]

Ver también

Notas

  1. ^ La posible semántica del mundo 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 necesaria ]
  2. ^ Shoham y Leyton-Brown 2008.
  3. ^ Gasquet y otros. 2013, págs. 14-16.
  4. ^ Tenga en cuenta que la noción de 'modelo' en la semántica de Kripke de la lógica modal difiere de la noción de 'modelo' en la lógica no modal clásica: en lógica clásica decimos que alguna fórmula F tiene un 'modelo' si existe algún ' 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 de lógica modal de Kripke, por el contrario, un "modelo" no es un "algo" específico que hace verdadera una fórmula modal específica; En la semántica de Kripke, un "modelo" debe entenderse más bien como un universo más amplio de discurso dentro del cual cualquier fórmula modal puede "comprenderse" 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, a la lógica entera) . sistema de sus axiomas y reglas de deducción).
  5. ^ Giaquinto 2002.
  6. ^ Después de Andrzej Grzegorczyk .
  7. ^ Simpson 1994, pag. 20, 2.2 La semántica de la lógica intuicionista.
  8. ^ Vea una formalización ligeramente diferente en Moschovakis (2022)
  9. ^ Goldblatt 2006b.
  10. ^ Stokhof 2008, consulte los dos últimos párrafos de la Sección 3 Interludio cuasi histórico: el camino de Viena a Los Ángeles .

Referencias

enlaces externos