Formal semantics for non-classical logic systems
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").
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 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 todo w ∈ W y fórmulas modales A y B :
- si y sólo si ,
- si y sólo si o ,
- si y sólo si por todo eso .
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:
- un modelo , si para todo w ∈ W ,
- un marco , si es válido para todas las opciones posibles de ,
- una clase C de cuadros 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á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 ). 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 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 máximo L-consistente (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 sólo 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
- X es válido en todo cuadro 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 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
- una fórmula de Sahlqvist es canónica,
- la clase de marcos correspondientes a una fórmula de Sahlqvist es definible de primer orden ,
- Existe un algoritmo que calcula la condición de marco correspondiente a una fórmula de Sahlqvist determinada.
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:
- si p es una variable proposicional, y , entonces ( condición de persistencia (cf. monotonicidad )),
- si y sólo si y ,
- si y sólo 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 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 :
- el dominio de M u está incluido en el dominio de M v ,
- las realizaciones de símbolos de funciones en M u y M v concuerdan en 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 sólo si y ,
- si y sólo si o ,
- si y sólo si para todos , implica ,
- no ,
- si y sólo si existe tal que ,
- si y sólo si para todos y cada uno , .
Aquí e ( x → a ) 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 . 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
- f preserva 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 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 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
- 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 , 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 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:
- Rudolf Carnap parece haber sido el primero en tener la idea de que se puede dar una semántica de mundo posible a las modalidades de necesidad y posibilidad dando a la función de valoración un parámetro que abarque los mundos posibles leibnizianos. Bayart desarrolla más esta idea, 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 de Boole con operadores como modelos. Bjarni Jónsson y Tarski establecieron la representabilidad de las álgebras booleanas con operadores en términos de marcos. Si se hubieran unido las dos ideas, 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 de modelos habitual para esta última, habría producido una teoría de modelos equivalente a los modelos de Kripke para la última. 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 de las relaciones de accesibilidad y los axiomas de lógica modal al estilo de Lewis . Kanger, sin embargo, no pudo demostrar la integridad de su sistema;
- Jaakko Hintikka dio una semántica en sus artículos introduciendo la lógica epistémica que es una variación simple de la semántica de Kripke, equivalente a la caracterización de valoraciones mediante conjuntos máximos consistentes. No da reglas de inferencia para la lógica epistémica y, por tanto, 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 su integridad, por lo que no las publicó hasta 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 de satisfacción más complicada.
Ver también
Notas
- ^ 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 ]
- ^ 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: la totalidad sistema de sus axiomas y reglas de deducción).
- ^ Después de Andrzej Grzegorczyk .
- ^ Vea 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.
- Toro, 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. 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.
- Cresswell, MJ ; Hughes, GE (2012) [1996]. Una nueva introducción a la lógica modal. Rutledge. 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. Saltador. págs. 225–339. ISBN 978-94-009-5203-4.
- Dummett, Michael AE (2000). Elementos del intuicionismo (2ª ed.). Prensa de Clarendon. ISBN 978-0-19-850524-2.
- Ajuste, 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. Consultado el 24 de diciembre de 2014 .
- Giaquinto, Marco (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. Prensa de la Universidad de Oxford. pag. 256.ISBN 019875244X. Consultado 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.; Bosques, 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 Quantales" (PDF) . En Governatori, G.; Hodkinson, I.; Venema, Y. (eds.). Avances en lógica modal . vol. 6. Londres: Publicaciones universitarias. págs. 209–225. ISBN 1904987206.
- Mac Lane, Saunders ; Moerdijk, Ieke (2012) [1991]. Gavillas en geometría y lógica: una primera introducción a la teoría del topos. Saltador. ISBN 978-1-4612-0927-0.
- Shoham, Yoav; Leyton-Brown, Kevin (2008). Sistemas multiagente: fundamentos lógicos, algorítmicos y de teoría de juegos. Prensa de la Universidad de Cambridge. pag. 397.ISBN 978-0521899437.
- Simpson, Álex (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, Martín (2008). "La arquitectura del significado: el Tractatus de Wittgenstein y la semántica formal". En Zamuner, Eduardo; Levy, David K. (eds.). Los argumentos duraderos de Wittgenstein . Londres: Routledge. págs. 211–244. ISBN 9781134107070.
Enlaces externos
Wikimedia Commons tiene medios relacionados con los 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.). Enciclopedia de Filosofía de Stanford .
- "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.). Enciclopedia de Filosofía de Stanford .