Semántica formal para sistemas lógicos no clásicos
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").
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 .
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 todos los w ∈ W y fórmulas modales A y B :
- si y sólo si ,
- si y solo si o ,
- si y sólo si para todos tales que .
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:
- un modelo , si para todo w ∈ W ,
- un marco , si es válido para todas las opciones posibles de ,
- una clase C de marcos o modelos , si es válida en cada miembro de C.
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 ). 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.
Obsérvese 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
- X es válido en cualquier marco que satisfaga P ,
- para cualquier lógica modal normal L que contenga X , el marco subyacente del modelo canónico de L satisface P.
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
- Una fórmula de Sahlqvist es canónica,
- La clase de marcos correspondiente a una fórmula de Sahlqvist es definible en primer orden ,
- Hay un algoritmo que calcula la condición de marco correspondiente a una fórmula de Sahlqvist dada.
É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:
- si p es una variable proposicional, , y , entonces ( condición de persistencia (cf. monotonía )),
- si y solo si y ,
- si y solo si o ,
- si y sólo si para todos , implica ,
- no .
La negación de A , ¬ A , podría definirse como una abreviatura de A → ⊥. Si para todo u tal que w ≤ u , 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 :
- 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 en los elementos de M u ,
- para cada predicado n -ario 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 sólo si se cumple en M w ,
- si y solo si y ,
- si y solo si o ,
- si y sólo si para todos , implica ,
- no ,
- si y sólo si existe un tal que ,
- si y solo si para todos y cada uno , .
Aquí e ( x → a ) es la evaluación que da a x el valor a , y por lo demás concuerda con e . [9]
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 . 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
- f conserva la relación de accesibilidad, es decir, u R v implica f ( u ) R' f ( v ),
- siempre que f ( u ) R' v ', existe una 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 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”:
- 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 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
- f es una sobreyección ,
- f conserva la relación de accesibilidad y (en ambas direcciones) la satisfacción de las variables p ∈ X ,
- si f ( u ) R' f ( v ) y , donde , entonces .
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:
- Rudolf Carnap parece haber sido el primero en tener la idea de que se puede dar una semántica de mundo 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 sobre los mundos posibles leibnizianos. Bayart desarrolla esta idea más a fondo, pero no dio definiciones recursivas de satisfacción en el estilo introducido por Tarski;
- JCC McKinsey y Alfred Tarski desarrollaron un enfoque para modelar la lógica modal que sigue siendo influyente en la investigación moderna, a saber, el enfoque algebraico, en el que se utilizan álgebras de Boole 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 se hubieran puesto en conjunto las dos ideas, el resultado habría sido precisamente modelos de marcos, 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 el trabajo inédito de CA Meredith , desarrolló una traducción de la lógica modal oracional a la lógica predicativa clásica que, si la hubiera combinado con la teoría de modelos habitual para esta última, habría producido una teoría de modelos equivalente a los modelos de Kripke para la primera. Pero su enfoque era decididamente sintáctico y anti-teórico de modelos.
- Stig Kanger propuso un enfoque bastante más complejo para 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 de las relaciones de accesibilidad y los axiomas de estilo Lewis para la lógica modal. Sin embargo, Kanger no logró dar una prueba de completitud para su sistema;
- Jaakko Hintikka, en sus artículos de introducción a la lógica epistémica, propuso una semántica que es una variación simple de la semántica de Kripke, equivalente a la caracterización de las valoraciones por medio de conjuntos máximos consistentes. No ofrece reglas de inferencia para la lógica epistémica y, por lo tanto, no puede ofrecer una prueba de completitud;
- Richard Montague tenía muchas de las ideas clave contenidas en el trabajo de Kripke, pero no las consideró significativas porque no tenía pruebas de su completitud, y por eso no las publicó hasta después de que los artículos de Kripke habían creado sensación en la comunidad lógica;
- Evert Willem Beth presentó una semántica de la lógica intuicionista basada en árboles, que se parece mucho a la semántica de Kripke, excepto que utiliza una definición más engorrosa de satisfacción.
Véase también
Notas
- ^ 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 ]
- ^ 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).
- ^ Según Andrzej Grzegorczyk .
- ^ Boolos, George (1993). La lógica de la demostrabilidad . Cambridge University Press. pp. 148, 149. ISBN 0-521-43342-8.
- ^ Véase una formalización ligeramente diferente en Moschovakis (2022)
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. Vol. 2. Springer. 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.
- Cresswell, MJ ; Hughes, GE (2012) [1996]. Una nueva introducción a la lógica modal. Routledge. ISBN 978-1-134-80028-5.
- 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. Vol. 3. Springer. págs. 225–339. ISBN 978-94-009-5203-4.
- Dummett, Michael AE (2000). Elementos del intuicionismo (2.ª ed.). Clarendon Press. ISBN 978-0-19-850524-2.
- Fitting, Melvin (1969). Lógica intuicionista, teoría de modelos y forzamiento . Holanda del Norte. ISBN 978-0-444-53418-7.
- Gasquet, Olivier; Herzig, Andreas; Dijo, Bilal; Schwarzentruber, François (2013). Los mundos de Kripke: una introducción a la lógica modal a través de Tableaux. Saltador. págs.XV, 198. ISBN 978-3764385033. Recuperado el 24 de diciembre de 2014 .
- Giaquinto, Marcus (2002). La búsqueda de la 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. Oxford University Press. pág. 256. ISBN 019875244X. Recuperado el 24 de diciembre de 2014 .
- Goldblatt, Robert (2006a). "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. Vol. 7. Elsevier. págs. 1–98. ISBN. 978-0-08-046303-2.
- Goldblatt, Robert (2006b). "Una semántica de Kripke-Joyal para la lógica no conmutativa en los cuentos cuánticos" (PDF) . En Governatori, G.; Hodkinson, I.; Venema, Y. (eds.). Avances en lógica modal . Vol. 6. Londres: College Publications. págs. 209–225. ISBN. 1904987206.
- Mac Lane, Saunders ; Moerdijk, Ieke (2012) [1991]. Haces en geometría y lógica: una primera introducción a la teoría de topos. Springer. ISBN 978-1-4612-0927-0.
- Shoham, Yoav; Leyton-Brown, Kevin (2008). Sistemas multiagente: fundamentos algorítmicos, lógicos y de teoría de juegos. Cambridge University Press. pág. 397. ISBN 978-0521899437.
- Simpson, Alex (1994). La teoría de la prueba y la semántica de la lógica modal intuicionista (Tesis). Archivo de Investigación de Edimburgo (ERA) .
- Stokhof, Martin (2008). "La arquitectura del significado: el Tractatus de Wittgenstein y la semántica formal". En Zamuner, Edoardo; Levy, David K. (eds.). Los argumentos perdurables de Wittgenstein . Londres: Routledge. pp. 211–244. ISBN. 9781134107070.
Enlaces externos
Wikimedia Commons alberga una categoría multimedia sobre Modelos Kripke .
- Burgess, John P. "Modelos Kripke". Archivado desde el original el 20 de octubre de 2004.
- 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.
- Garson, James (23 de enero de 2023). "Lógica modal". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
- "Modelos de Kripke", Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
- Moschovakis, Joan (16 de diciembre de 2022). "Lógica intuicionista". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .