La semántica de Kripke (también conocida como semántica relacional o semántica de marcos , y a menudo confundida con la posible semántica mundial ) es una semántica formal para sistemas lógicos no clásicos creados a finales de la década de 1950 y principios de la de 1960 por Saul Kripke y André Joyal . Primero se concibió para la lógica modal y luego se adaptó a la lógica intuicionista y otros sistemas no clásicos. El desarrollo de la semántica de Kripke supuso un gran avance en la teoría de las lógicas no clásicas, porque la teoría del modelo 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 numerable infinito 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 dey puede definirse en términos de necesidad así:("posiblemente A" se define como equivalente a "no necesariamente no A"). [1]
Definiciones basicas
Un marco Kripke o un 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 . [2]
Un modelo Kripke es un triple, dónde es un marco Kripke, y es una relación entre los nodos de W y fórmulas modales, tal que para todas las fórmulas w ∈ W y modales A y B:
- si y solo si ,
- si y solo si o ,
- si y solo si para todos tal que .
Leemos como " w satisface A ", " A se satisface en w " o " w fuerza A ". La relaciónse 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:
- un modelo , Si para todo w ∈ W ,
- un cuadro , si es válido en para todas las opciones posibles de ,
- una clase C de marcos o modelos, si es válida en todos los miembros de C .
Definimos Thm ( C ) como el conjunto de todas las fórmulas que son válidos en C . A la inversa, si X es un conjunto de fórmulas, y mucho Mod ( X ) sea la clase de todas las tramas que validan cada fórmula de X .
Una lógica modal (es decir, un conjunto de fórmulas) L es sólida con respecto a una clase de marcos C , si L ⊆ Thm ( C ). L es completa wrt 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 ) solo si la relación de consecuencia semántica refleja su contraparte sintáctica, la relación de consecuencia sintáctica ( derivabilidad ). [3] Es vital saber qué lógicas modales son sólidas y completas con respecto a una clase de marcos de Kripke, y también determinar 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 ocurre en general: mientras que la mayoría de los sistemas modales estudiados son clases completas 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 marcos tal que L es WRT sonido C . De ello se deduce que L es Kripke completo si y solo si es completo de su clase correspondiente.
Considere el esquema T :. T es válido en cualquier marco reflexivo: Si , luego 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 solo si w R u . Luego, por lo tanto por T , lo que significa w R w usando la definición de. T corresponde a la clase de fotogramas reflexivos de Kripke.
A menudo es mucho más fácil caracterizar la clase correspondiente de L que probar su integridad, por lo que la correspondencia sirve como guía para las pruebas de integridad. La correspondencia también se usa para mostrar la incompletitud de las lógicas modales: suponga 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 esquemagenera una lógica incompleta, ya que corresponde a la misma clase de tramas que GL (es decir, tramas transitivas y recíprocas bien fundamentadas), pero no prueba la GL -tautología.
Esquemas de axioma modal común
La siguiente tabla enumera axiomas modales comunes junto con sus clases correspondientes. El nombre de los axiomas a menudo varía.
Nombre | Axioma | Condición del cuadro |
---|---|---|
K | N / A | |
T | reflexivo : | |
4 | transitivo : | |
denso : | ||
D | o | serial : |
B | simétrico : | |
5 | Euclidiana : | |
GL | R transitivo, R −1 bien fundado | |
Grz a | R reflexiva y transitiva, R −1 - Id bien fundado | |
H | ||
METRO | (una propiedad complicada de segundo orden ) | |
GRAMO | convergente: | |
discreto: | ||
función parcial : | ||
función: | ||
o | vacío: |
Sistemas modales comunes
La siguiente tabla enumera varios sistemas modales normales comunes. Las condiciones de las tramas para algunos de los sistemas se simplificaron: las lógicas están completas con respecto a las clases de tramas dadas en la tabla, pero pueden corresponder a una clase de tramas más grande.
Nombre | Axiomas | Condición del cuadro |
---|---|---|
K | - | todos los fotogramas |
T | T | reflexivo |
K4 | 4 | transitivo |
S4 | T, 4 | hacer un pedido |
S5 | T, 5 o D, B, 4 | relación de equivalencia |
S4.3 | T, 4, H | preorden total |
S4.1 | T, 4, M | hacer un pedido, |
S4.2 | T, 4, G | pedido anticipado dirigido |
GL , K4W | GL o 4, GL | orden parcial estricto finito |
Grz, S4Grz | Grz o T, 4, Grz | orden parcial finito |
D | D | de serie |
D45 | D, 4, 5 | transitivo, serial y euclidiano |
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 usar conjuntos máximos consistentes como modelos. Los modelos canónicos de Kripke juegan 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 usando los teoremas de L y Modus Ponens. Un set-L consistente máxima (un L - MCS para abreviar) es un L conjunto -consistente que no tiene adecuado L superconjunto -consistente.
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 como sigue:
- si y solo si para cada fórmula , Si luego ,
- si y solo si .
El modelo canónico es un modelo de L , como todos los L - MCS contiene todos los teoremas de L . Según el lema de Zorn , cada conjunto coherente con L 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 la completitud de K con respecto a la clase de todos los marcos de Kripke. Este argumento no funciona para arbitraria L , porque no hay ninguna garantía de que el subyacente del marco del modelo canónico satisface las condiciones 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
- X es válido en todo marco que satisfaga P ,
- para cualquier lógica modal normal de L que contiene X , el marco subyacente del modelo canónico de L satisface P .
Una unión de conjuntos canónicos de fórmulas es canónica en sí misma. De la discusión anterior se deduce 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í mismo no es canónico (Goldblatt, 1991), pero la lógica combinada S4.1 (de hecho, incluso K4.1 ) es canónica.
En general, es indecidible si un axioma dado es canónico. Conocemos una condición suficientemente buena: Henrik Sahlqvist identificó una amplia clase de fórmulas (ahora llamadas fórmulas de Sahlqvist ) tales que
- una fórmula de Sahlqvist es canónica,
- la clase de marcos correspondientes a una fórmula de Sahlqvist es definible de primer orden ,
- hay un algoritmo que calcula la condición de marco correspondiente a una fórmula de Sahlqvist dada.
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 está completa con respecto a una clase de marcos finitos. Una aplicación de este concepto es la decidibilidad pregunta: ¿se desprende del teorema de mensaje de que una lógica modal de forma recursiva axiomatizada L que tiene FMP es decidible, siempre y cuando sea decidible si un marco finito 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 extensiones 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 integridad 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 Kripke integridad de una lógica: cada lógica modal normal es completo con respecto a una clase de álgebra de modales , y una finita modal álgebra se puede transformar en un marco de Kripke. Como ejemplo, Robert Bull demostró con este método que todas las extensiones normales de S4.3 tienen FMP y Kripke está completo.
Lógicas multimodales
La semántica de Kripke tiene una generalización directa a las lógicas con más de una modalidad. Un marco de Kripke para un lenguaje concomo el conjunto de sus operarios necesidad consiste en un conjunto no vacío W equipado con relaciones binarias R i 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 usa a menudo para lógicas de probabilidad polimodal . Un modelo de Carlson es una estructuracon una sola relación de accesibilidad R , y subconjuntos D i ⊆ 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 con los modelos polimodales Kripke habituales; hay, sin embargo, 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, dónde es un preordenado marco Kripke, y cumple las siguientes condiciones:
- si p es una variable proposicional,, y , luego ( condición de persistencia (cf. monotonicidad )),
- si y solo si y ,
- si y solo si o ,
- si y solo si para todos , implica ,
- no .
La negación de A , ¬ A , podría definirse como una abreviatura de A → ⊥. Si para todos u tal que w ≤ u , no u ⊩ A , entonces w ⊩ A → ⊥ es vacuamente verdadero , así que w ⊩ ¬ A .
La lógica intuicionista es sólida y completa con respecto a su semántica de Kripke, y tiene la propiedad de modelo finito .
Lógica intuicionista de primer orden
Sea L un lenguaje de primer orden . Un modelo Kripke de L es un triple, dónde es un marco intuicionista de Kripke, 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 :
- el dominio de M u está incluido en el dominio de M v ,
- las realizaciones de los símbolos de función en M u y M v concuerdan con los elementos de M u ,
- para cada n -predicado P y elementos a 1 , ..., a n ∈ M u : si P ( a 1 , ..., a n ) se cumple en M u , entonces se cumple en M v .
Dada una evaluación e de variables por elementos de M w , definimos la relación de satisfacción:
- si y solo si se mantiene en M w ,
- si y solo si y ,
- si y solo si o ,
- si y solo si para todos , implica ,
- no ,
- si y solo si existe un tal que ,
- si y solo si para cada y cada , .
Aquí e ( x → a ) es la evaluación que le da a x el valor a , y por lo demás concuerda con e .
Vea una formalización ligeramente diferente en. [4]
Semántica de Kripke-Joyal
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 topos . [5] Es decir, el aspecto "local" de la existencia de las secciones de un haz era una especie de lógica de lo "posible". Aunque este desarrollo fue el trabajo de varias personas, el nombre semántica de Kripke-Joyal se usa a menudo en este sentido.
Construcciones de modelos
Como en la teoría clásica de modelos , 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 usa). Un p-morfismo de los fotogramas de Kripke y es un mapeo tal que
- f conserva la relación de accesibilidad, es decir, u R v implica f ( u ) R ' f ( v ),
- siempre que f ( u ) R ' v ', hay un v ∈ W tal que u R v y f ( v ) = v '.
Un p-morfismo de los modelos de Kripke y es un p-morfismo de sus marcos subyacentes , que satisface
- si y solo 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":
- si u B u ' y u R v , existe v' ∈ W ' tal que v B v' y u 'R' v ' ,
- si u B u ' y u' R 'v' , existe v ∈ W tal que v B v ' y u R v .
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 solo si , para cualquier variable proposicional p .
La propiedad clave que se desprende de esta definición es que las bisimulaciones (por lo tanto también p-morfismos) de los modelos preservan la satisfacción de todas las fórmulas, no solo las variables proposicionales.
Podemos transformar un modelo de Kripke en un árbol usando unraveling . Dado un modeloy un nodo fijo w 0 ∈ W , definimos un modelo, donde W ' es el conjunto de todas las secuencias finitastal 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 probar FMP para muchas lógicas. Sea X un conjunto de fórmulas cerradas bajo subfórmulas. Una filtración X de un modeloes un mapeo f de W a un modelo tal que
- f es una sobreyección ,
- f preserva la relación de accesibilidad y (en ambas direcciones) la satisfacción de las variables p ∈ X ,
- si f ( u ) R ' f ( v ) y, dónde , luego .
De ello resulta que f conservas 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 .
Como en el caso de desentrañar, la definición de la relación de accesibilidad sobre el cociente varía.
Semántica de trama general
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. Se puede remediar equipando los marcos de Kripke con una estructura adicional que restrinja el conjunto de posibles valoraciones, utilizando ideas de la semántica algebraica. Esto da lugar a la semántica del marco general .
Aplicaciones informáticas
Blackburn y col. (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 es sorprendente 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 y col. así afirman, debido a esta conexión, que los lenguajes modales son ideales para proporcionar una "perspectiva local interna de las estructuras relacionales". (pág. xii)
Historia y terminología
Trabajo similar que precedió a los revolucionarios avances semánticos de Kripke: [6]
- Rudolf Carnap parece haber sido el primero en tener la idea de que se puede dar una semántica mundial posible para las modalidades de necesidad y posibilidad mediante la asignación de un parámetro a la función de valoración que se extiende a lo largo de los mundos posibles leibnizianos. Bayart desarrolla esta idea más allá, pero ninguno dio definiciones recursivas de satisfacción en el estilo introducido por Tarski;
- JCC McKinsey y Alfred Tarski desarrollaron un enfoque para modelar lógicas modales que todavía es influyente en la investigación moderna, a saber, el enfoque algebraico, en el que se utilizan álgebras booleanas con operadores como modelos. Bjarni Jónsson y Tarski establecieron la representabilidad de las álgebras de Boole con operadores en términos de marcos. Si las dos ideas se hubieran juntado, el resultado habría sido precisamente modelos de marco, es decir, modelos de Kripke, años antes que Kripke. Pero nadie (ni siquiera Tarski) vio la conexión en ese momento.
- Arthur Prior , basándose en un trabajo inédito de CA Meredith , desarrolló una traducción de la lógica modal oracional a la lógica de predicados clásica que, si la hubiera combinado con la teoría del modelo habitual para esta última, habría producido una teoría del modelo equivalente a los modelos de Kripke para la anterior. Pero su enfoque fue decididamente sintáctico y antimodelo-teórico.
- Stig Kanger dio un enfoque bastante más complejo a la interpretación de la lógica modal, pero que contiene muchas de las ideas clave del enfoque de Kripke. Primero señaló la relación entre las condiciones en las relaciones de accesibilidad y los axiomas de estilo de Lewis para la lógica modal. Sin embargo, Kanger falló en dar una prueba completa de su sistema;
- Jaakko Hintikka dio una semántica en sus trabajos introduciendo la lógica epistémica que es una simple variación de la semántica de Kripke, equivalente a la caracterización de valoraciones por medio de conjuntos máximos consistentes. No da reglas de inferencia para la lógica epistémica, por lo que no puede dar una prueba de integridad;
- Richard Montague tenía muchas de las ideas clave contenidas en el trabajo de Kripke, pero no las consideraba significativas, porque no tenía pruebas de integridad, por lo que no las publicó hasta después de que los artículos de Kripke causaron sensación en la comunidad lógica;
- Evert Willem Beth presentó una semántica de lógica intuicionista basada en árboles, que se parece mucho a la semántica de Kripke, excepto por el uso de una definición más engorrosa de satisfacción.
Ver también
- Topología Alexandrov
- Lógica modal normal
- Bidimensionalismo
- Rompecabezas de niños fangosos
Notas
- a ^ Después de Andrzej Grzegorczyk .
- ^ Shoham, Yoav; Leyton-Brown, Kevin (2008). Sistemas multiagente: fundamentos algorítmicos, teóricos de juegos y lógicos . Prensa de la Universidad de Cambridge. pag. 397. ISBN 978-0521899437.
- ^ Gasquet, Olivier; et al. (2013). Los mundos de Kripke: una introducción a la lógica modal a través de Tableaux . Saltador. págs. 14-16. ISBN 978-3764385033. Consultado el 24 de diciembre de 2014 .
- ^ Giaquinto, Marcus (2002). La búsqueda de certeza: una explicación filosófica de los fundamentos de las matemáticas: una explicación filosófica de los fundamentos de las matemáticas . Prensa de la Universidad de Oxford. pag. 256. ISBN 019875244X. Consultado el 24 de diciembre de 2014 .
- ^ Lógica intuicionista . Escrito por Joan Moschovakis . Publicado en la Enciclopedia de Filosofía de Stanford.
- ^ Goldblatt, Robert (2006). "Una semántica de Kripke-Joyal para la lógica no conmutativa en Quantales" (PDF) . En Governatori, G .; Hodkinson, I .; Venema, Y. (eds.). Avances en lógica modal . 6 . Londres: Publicaciones universitarias. págs. 209–225. ISBN 1904987206.
- ^ Stokhof, Martin (2008). "La arquitectura del significado: Tractatus de Wittgenstein y semántica formal" . En Zamuner, Edoardo; Levy, David K. (eds.). Los argumentos perdurables de Wittgenstein . Londres: Routledge. págs. 211–244. ISBN 9781134107070. preimpresión (Véanse los dos últimos párrafos en la Sección 3 Interludio cuasi histórico: el camino de Viena a Los Ángeles ).
Referencias
- Blackburn, P .; de Rijke, M .; Venema, Yde (2002). Lógica modal . Prensa de la Universidad de Cambridge. ISBN 978-1-316-10195-7.
- Bull, Robert A .; Segerberg, K. (2012) [1984]. "Lógica modal básica" . En Gabbay, DM; Guenthner, F. (eds.). Extensiones de la lógica clásica . Manual de lógica filosófica. 2 . Saltador. págs. 1-88. ISBN 978-94-009-6259-0.
- Chagrov, A .; Zakharyaschev, M. (1997). Lógica modal . Prensa de Clarendon. ISBN 978-0-19-853779-3.
- Dummett, Michael AE (2000). Elementos del intuicionismo (2ª ed.). Prensa de Clarendon. ISBN 978-0-19-850524-2.
- Adecuado, Melvin (1969). Lógica intuicionista, teoría de modelos y forzamiento . Holanda Septentrional. ISBN 978-0-444-53418-7.
- Goldblatt, Robert (2006). "Lógica modal matemática: una visión de su evolución" (PDF) . En Gabbay, Dov M .; Woods, John (eds.). Lógica y modalidades en el siglo XX (PDF) . Manual de Historia de la Lógica. 7 . Elsevier. págs. 1-98. ISBN 978-0-08-046303-2.
- Cresswell, MJ; Hughes, GE (2012) [1996]. Una nueva introducción a la lógica modal . Routledge. ISBN 978-1-134-80028-5.
- Mac Lane, Saunders ; Moerdijk, Ieke (2012) [1991]. Gavillas en geometría y lógica: una primera introducción a la teoría de Topos . Saltador. ISBN 978-1-4612-0927-0.
- van Dalen, Dirk (2013) [1986]. "Lógica intuicionista" . En Gabbay, Dov M .; Guenthner, Franz (eds.). Alternativas a la lógica clásica . Manual de lógica filosófica. 3 . Saltador. págs. 225–339. ISBN 978-94-009-5203-4.
enlaces externos
- Garson, James. "Lógica modal" . La Enciclopedia de Filosofía de Stanford .
- Moschovakis, Joan (2018). "Lógica intuicionista" . Enciclopedia de Filosofía de Stanford . Laboratorio de Investigación en Metafísica, Universidad de Stanford.
- Detlovs, V .; Podnieks, K. "4.4 Lógica proposicional constructiva - Semántica de Kripke" . Introducción a la lógica matemática . Universidad de Letonia. NB: Constructivo = intuicionista.
- Burgess, John P. "Modelos Kripke" . Archivado desde el original el 20 de octubre de 2004.
- "Modelos de Kripke" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]