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 la década de 1950 y principios de la de 1960 por Saul Kripke y André Joyal . Fue concebida inicialmente para lógicas modales y posteriormente adaptada a la lógica intuicionista y otros sistemas no clásicos. El desarrollo de la semántica de Kripke supuso un avance en la teoría de las lógicas no clásicas, ya que la teoría de modelos de dichas lógicas era prácticamente inexistente antes de Kripke (existía la semántica algebraica, pero se consideraba «sintaxis disfrazada»).

Semántica de la lógica modal

El lenguaje de la lógica modal proposicional consiste en un conjunto infinitamente numerable de variables proposicionales , un conjunto de conectores veritativo-funcionales (en este artículo $\to$ y $\neg$ ), y el operador modal $\Box$ ("necesariamente"). El operador modal $\Diamond$ ("posiblemente") es (clásicamente) el dual de $\Box$ y puede definirse en términos de necesidad de la siguiente manera: $\Diamond A:=\neg \Box \neg A$ ("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 $\langle W,R\rangle$ 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 triplete. $\langle W,R,\Vdash \rangle$ , ^{[ 4 ]} donde $\langle W,R\rangle$ es un cuadro Kripke y $\Vdash$ 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 :

$w\Vdash \neg A$ si y solo si $w\nVdash A$ ,
$w\Vdash A\to B$ si y solo si $w\nVdash A$ o $w\Vdash B$ ,
$w\Vdash \Box A$ si y solo si $u\Vdash A$ a pesar de $u$ de tal manera que $w\;R\;u$ .

Leemos $w\Vdash A$ como “ w satisface a A ”, “ A se satisface en w ” o “ w obliga a A ”. La relación $\Vdash$ Se denomina relación de satisfacción , evaluación o relación de forzamiento . La relación de satisfacción está determinada unívocamente por su valor en variables proposicionales.

Una fórmula A es válida en:

un modelo $\langle W,R,\Vdash \rangle$ , si $w\Vdash A$ a pesar de $w\in W$ ,
un marco $\langle W,R\rangle$ , si es válido en $\langle W,R,\Vdash \rangle$ para todas las posibles opciones de $\Vdash$ ,
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 . Recíprocamente, 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 só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 exhaustividad

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 ). ^{[ 5 ]} Es vital saber qué lógicas modales son correctas y completas con respecto a una clase de marcos de Kripke, y determinar también cuál es esa clase.

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 todo modelo de Kripke). Sin embargo, lo contrario no se cumple en general: si bien la mayoría de los sistemas modales estudiados son 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 marcos C si C = Mod( L ). En otras palabras, C es la clase más grande de marcos tal que L es válida con respecto a C. Por lo tanto , L es completa en el sentido de Kripke si y solo si es completa en su clase correspondiente.

Consideremos el esquema T : $\Box A\to A$ T es válido en cualquier marco reflexivo $\langle W,R\rangle$ : si $w\Vdash \Box A$ , entonces $w\Vdash A$ puesto que w R w . Por otro lado, un marco que valida T tiene que ser reflexivo: fijemos w ∈ W y definamos la satisfacción de una variable proposicional p de la siguiente manera: $u\Vdash p$ si y solo si w R u . Entonces $w\Vdash \Box p$ , de este modo $w\Vdash p$ por T , lo que significa w R w usando la definición de $\Vdash$ . T corresponde a la clase de marcos de Kripke reflexivos.

A menudo es mucho más fácil caracterizar la clase correspondiente de L que demostrar 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 ₁ ⊆ L ₂ son lógicas modales normales que corresponden a la misma clase de marcos, pero L ₁ no demuestra todos los teoremas de L _2. Entonces L ₁ es incompleto de Kripke. Por ejemplo, el esquema $\Box (A\leftrightarrow \Box A)\to \Box A$ genera una lógica incompleta, ya que corresponde a la misma clase de marcos que GL (es decir, marcos bien fundados transitivos y recíprocos), pero no prueba la tautología de GL. $\Box A\to \Box \Box A$ .

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 según la numeración de los sistemas de lógica simbólica de CI Lewis .

El axioma K también puede reescribirse como $\Box [(A\to B)\land A]\to \Box B$ , lo que establece lógicamente el modus ponens como una regla de inferencia en todo mundo posible.

Nótese que para el axioma D , $\Diamond A$ implica implícitamente $\Diamond \top$ , 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 $\Diamond A\rightarrow \Diamond \top$ 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 correcta y completa con respecto a las clases de marco indicadas en la tabla, pero pueden corresponder a una clase de marco más amplia.

Modelos canónicos

Para cualquier lógica modal normal, L , se puede construir un modelo de Kripke (denominado modelo canónico ) que refuta precisamente los no teoremas de L , mediante una adaptación de la técnica estándar de usar conjuntos consistentes máximos como modelos. Los modelos canónicos de Kripke desempeñan un papel similar al de 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 maximal (un L - MCS , por sus siglas en inglés) es un conjunto L -consistente que no tiene un superconjunto L -consistente propio.

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

X\;R\;Y

si y solo si para cada fórmula

A

, si

\Box A\in X

entonces

A\in Y

,

X\Vdash A

si y solo si

A\in X

.

El modelo canónico es un modelo de L , ya que todo L - MCS contiene todos los teoremas de L. Según el lema de Zorn , todo conjunto L -consistente está contenido en un L - MCS ; en particular, toda 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 , ya que 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ónico con respecto a una propiedad P de los marcos de Kripke, si

X es válido en cada marco que satisface 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 deduce que cualquier lógica axiomatizada por un conjunto canónico de fórmulas es completa en el sentido de Kripke y compacta .

Los axiomas T, 4, D, B, 5, H, G (y por lo 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í lo es.

En general, es indecidible si un axioma dado es canónico. Conocemos una condición suficiente conveniente: 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 dada.

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

Propiedad de modelo finito

Una lógica posee la propiedad de modelo finito (PMF) si es completa 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 posee PMF es decidible, siempre que sea decidible si un marco finito dado es un modelo de L. En particular, toda lógica finitamente axiomatizable con PMF es decidible.

Existen diversos métodos para establecer 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 desenrollamiento . Como otra posibilidad, las pruebas de completitud basadas en cálculos de secuencias sin cortes generalmente producen modelos finitos directamente.

La mayoría de los sistemas modales utilizados en la práctica (incluidos todos los mencionados 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 puede transformarse 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 en Kripke.

lógicas multimodales

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 $\{\Box _{i}\mid \,i\in I\}$ ya que 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:

w\Vdash \Box _{i}A

si y solo si

\forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).

Una semántica simplificada, descubierta por Tim Carlson, se usa a menudo para lógicas de demostrabilidad polimodales . Un modelo de Carlson es una estructura $\langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle$ con una única relación de accesibilidad R y subconjuntos D _i ⊆ W para cada modalidad. La satisfacción se define como

w\Vdash \Box _{i}A

si y solo si

\forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).

Los modelos de Carlson son más fáciles de visualizar y de usar que los modelos polimodales de Kripke habituales; sin embargo, existen lógicas polimodales completas de Kripke que son incompletas según el modelo 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. ^{[ 8 ]}

Un modelo de Kripke intuicionista es un modelo triple $\langle W,\leq ,\Vdash \rangle$ , dónde $\langle W,\leq \rangle$ es un cuadro Kripke preordenado , y $\Vdash$ satisface las siguientes condiciones: ^{[ 9 ]}

si p es una variable proposicional, $w\leq u$ , y $w\Vdash p$ , entonces $u\Vdash p$ ( condición de persistencia (cf. monotonicidad )),
$w\Vdash A\land B$ si y solo si $w\Vdash A$ y $w\Vdash B$ ,
$w\Vdash A\lor B$ si y solo si $w\Vdash A$ o $w\Vdash B$ ,
$w\Vdash A\to B$ si y solo si para todos $u\geq w$ , $u\Vdash A$ implica $u\Vdash B$ ,
no $w\Vdash \bot$ .

Intuitivamente, el requisito adicional de $w\Vdash A\to B$ es asegurar la monotinidad incluso para proposiciones compuestas, es decir, para cualquier proposición A , si $w\leq u$ y $w\Vdash A$ , entonces $u\Vdash A$ . 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 trivialmente 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 de modelo finito .

Lógica intuicionista de primer orden

Sea L un lenguaje de primer orden . Un modelo de Kripke de L es una tripleta $\langle W,\leq ,\{M_{w}\}_{w\in W}\rangle$ , dónde $\langle W,\leq \rangle$ es un marco de Kripke intuicionista, M _w es una estructura L (clásica) para cada nodo w ∈ W , y se cumplen las siguientes condiciones de compatibilidad 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 coinciden en los elementos de M _u ,
para cada predicado n -ario P y elementos a ₁ ,..., a _n ∈ M _u : si P ( a ₁ ,..., 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 $w\Vdash A[e]$ :

$w\Vdash P(t_{1},\dots ,t_{n})[e]$ si y solo si $P(t_{1}[e],\dots ,t_{n}[e])$ se mantiene en M _w ,
$w\Vdash (A\land B)[e]$ si y solo si $w\Vdash A[e]$ y $w\Vdash B[e]$ ,
$w\Vdash (A\lor B)[e]$ si y solo si $w\Vdash A[e]$ o $w\Vdash B[e]$ ,
$w\Vdash (A\to B)[e]$ si y solo si para todos $u\geq w$ , $u\Vdash A[e]$ implica $u\Vdash B[e]$ ,
no $w\Vdash \bot [e]$ ,
$w\Vdash (\exists x\,A)[e]$ si y solo si existe un $a\in M_{w}$ de tal manera que $w\Vdash A[e(x\to a)]$ ,
$w\Vdash (\forall x\,A)[e]$ si y solo si para cada $u\geq w$ y cada $a\in M_{u}$ , $u\Vdash A[e(x\to a)]$ .

Aquí e ( x → a ) es la evaluación que le da a x el valor a y, por lo demás, coincide con e . ^{[ 10 ]}

Semántica de Kripke-Joyal

Como parte del desarrollo independiente de la teoría de haces , se comprendió alrededor de 1965 que la semántica de Kripke estaba íntimamente relacionada con el tratamiento de la cuantificación existencial en la teoría de topos . ^{[ 11 ]} Es decir, el aspecto «local» de la existencia para secciones de un haz era una especie de lógica de lo «posible». Si bien este desarrollo fue obra de varias personas, a menudo se utiliza el nombre de semántica de Kripke-Joyal o simplemente semántica de haces en este contexto.

La semántica de haces unifica la semántica de Kripke y la similar semántica de Beth , además de extenderla desde los casos irrelevantes para la prueba (proposicionales) a los casos relevantes para la prueba, en el caso de la relación de accesibilidad. $R$ es reflexivo y transitivo .

Construcciones de modelos

Al igual que 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 (abreviatura de pseudoepimorfismo , aunque este último término se usa con poca frecuencia). Un p-morfismo de marcos de Kripke $\langle W,R\rangle$ y $\langle W',R'\rangle$ es un mapeo $f\colon W\to W'$ de tal manera 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 un v ∈ W tal que u R v y f ( v ) = v '.

Un p-morfismo de modelos de Kripke $\langle W,R,\Vdash \rangle$ y $\langle W',R',\Vdash '\rangle$ es un p-morfismo de sus marcos subyacentes $f\colon W\to W'$ , lo cual satisface

w\Vdash p

si y solo si

f(w)\Vdash 'p

, para cualquier variable proposicional p .

Los P-morfismos son un tipo especial de bisimulaciones . En general, una bisimulación entre marcos $\langle W,R\rangle$ y $\langle W',R'\rangle$ es una relación B ⊆ W × W' , que satisface la siguiente propiedad “en 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 la forzante de las fórmulas atómicas :

si w B w' , entonces

w\Vdash p

si y solo si

w'\Vdash 'p

, para cualquier variable proposicional p .

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

Podemos transformar un modelo de Kripke en un árbol usando el desenrollado . Dado un modelo $\langle W,R,\Vdash \rangle$ y un nodo fijo w ₀ ∈ W , definimos un modelo $\langle W',R',\Vdash '\rangle$ donde W' es el conjunto de todas las secuencias finitas $s=\langle w_{0},w_{1},\dots ,w_{n}\rangle$ de tal manera que w _i R w _i+1 para todo i < n , y $s\Vdash 'p$ si y solo si $w_{n}\Vdash p$ para una variable proposicional p . La definición de la relación de accesibilidad R' varía; en el caso más simple ponemos

\langle w_{0},w_{1},\dots ,w_{n}\rangle \;R'\;\langle w_{0},w_{1},\dots ,w_{n},w_{n+1}\rangle

,

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 puede usar para demostrar FMP para muchas lógicas. Sea X un conjunto de fórmulas cerrado bajo la toma de subfórmulas. Una X -filtración de un modelo $\langle W,R,\Vdash \rangle$ es una aplicación f de W a un modelo $\langle W',R',\Vdash '\rangle$ de tal manera 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 $u\Vdash \Box A$ , dónde $\Box A\in X$ , entonces $v\Vdash A$ .

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 ,

u\Vdash A

si y solo si

v\Vdash A

.

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

semántica de marco general

El principal defecto de la semántica de Kripke reside en la existencia de lógicas incompletas de Kripke y lógicas completas pero no compactas. Esto se puede solucionar dotando a los marcos de Kripke de una estructura adicional que restrinja el conjunto de valoraciones posibles, utilizando ideas de la semántica algebraica. De este modo, surge la semántica general de marcos .

Aplicaciones de la informática

Blackburn et al. (2001) argumentan que, dado que una estructura relacional es simplemente un conjunto junto con una colección de relaciones sobre ese conjunto, no sorprende que las estructuras relacionales se encuentren con frecuencia. Como ejemplo de la informática teórica , presentan los sistemas de transición etiquetados , que modelan la ejecución de programas . Por lo tanto, Blackburn et al. afirman que, debido a esta conexión, los lenguajes modales son idóneos para proporcionar una "perspectiva interna y local sobre las estructuras relacionales" (p. xii).

Historia y terminología

Trabajos similares que precedieron a los revolucionarios avances semánticos de Kripke: ^{[ 12 ]}

Rudolf Carnap parece haber sido el primero en concebir la idea de que se puede dotar a la función de valoración de una semántica de mundos posibles para las modalidades de necesidad y posibilidad, mediante la incorporación de un parámetro que recorra los mundos posibles leibnizianos. Bayart desarrolla esta idea con mayor profundidad, pero ninguno de los dos proporcionó definiciones recursivas de satisfacción al estilo introducido por Tarski.
JCC McKinsey y Alfred Tarski desarrollaron un enfoque para modelar lógicas modales que aún influye en la investigación moderna: 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 booleanas con operadores en términos de marcos. Si ambas ideas se hubieran combinado, el resultado habría sido precisamente modelos de marcos, es decir, modelos de Kripke, años antes que Kripke. Pero nadie (ni siquiera Tarski) percibió la conexión en aquel momento.
Arthur Prior , basándose en trabajos inéditos de C. A. Meredith , desarrolló una traducción de la lógica modal sentencial a la lógica de predicados clásica que, de haberla 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 contrario a la teoría de modelos.
Stig Kanger propuso un enfoque 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 observó la relación entre las condiciones de las relaciones de accesibilidad y los axiomas de Lewis para la lógica modal. Sin embargo, Kanger no logró demostrar la completitud de su sistema.
En sus artículos sobre lógica epistémica, Jaakko Hintikka presentó una semántica que constituye una simple variación de la semántica de Kripke, equivalente a la caracterización de las valoraciones mediante conjuntos consistentes máximos. Sin embargo, no proporciona reglas de inferencia para la lógica epistémica, por lo que no puede ofrecer una prueba de completitud.
Richard Montague ya conocía muchas de las ideas clave contenidas en la obra de Kripke, pero no las consideró significativas porque carecía de una prueba de completitud, por lo que no publicó hasta que los trabajos de Kripke causaron sensación en la comunidad lógica.
Evert Willem Beth presentó una semántica de la lógica intuicionista basada en árboles, que se asemeja mucho a la semántica de Kripke, salvo por el uso de una definición de satisfacción más engorrosa.

Véase también

Notas

↑ La semántica de mundos posibles es un término más amplio que abarca diversos 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 maneras de modelar los 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.
↑ Shoham y Leyton-Brown 2008 .
^ Gasquet y col. 2013 , págs. 14-16.
↑ Nótese 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 las lógicas clásicas no modales: En las lógicas clásicas decimos que una 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 de 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 de Kripke, un «modelo» debe entenderse más bien como un universo de discurso más amplio dentro del cual cualquier fórmula modal puede ser «entendida» de manera significativa. Así pues: mientras que la noción de «tiene un modelo» en la lógica clásica no modal 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, todo el sistema de sus axiomas y reglas de deducción).
↑ Giaquinto 2002 .
↑ Según Andrzej Grzegorczyk .
↑ Boolos, George (1993). La lógica de la demostrabilidad . Cambridge University Press. págs. 148, 149. ISBN 0-521-43342-8.
^ Troelstra y van Dalen 1988 , págs. 75–87, 5. Semántica de Kripke.
↑ Simpson 1994 , pág. 20, 2.2 La semántica de la lógica intuicionista.
↑ Véase una formalización ligeramente diferente en Moschovakis (2022).
↑ Goldblatt 2006b .
↑ Stokhof 2008 , Véanse los dos últimos párrafos de 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. Vol. 2. Springer. pp. 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. pp. 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 . North-Holland. 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-3764385033Consultado el 24 de diciembre de 2014 .
Giaquinto, Marcus (2002). La búsqueda de la certeza : una reflexión filosófica sobre los fundamentos de las matemáticas . Oxford University Press. p. 256. ISBN 019875244XConsultado 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. pp. 1–98 . ISBN 978-0-08-046303-2.
Goldblatt, Robert (2006b). «Una semántica de Kripke-Joyal para la lógica no conmutativa en cuantos» (PDF) . En Governatori, G.; Hodkinson, I.; Venema, Y. (eds.). Avances en lógica modal . Vol. 6. Londres: College Publications. pp. 209–225 . ISBN 1904987206.
Mac Lane, Saunders ; Moerdijk, Ieke (2012) [1991]. Haz 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, de teoría de juegos y lógicos . Cambridge University Press. pág. 397. ISBN 978-0521899437.
Simpson, Alex K. (1994). La teoría de la demostración y la semántica de la lógica modal intuicionista (tesis). Archivo de Investigación de Edimburgo (ERA) . hdl : 1842/407 .
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.
Troelstra, AS ; van Dalen, D. (1988). Constructivismo en matemáticas: una introducción, volumen 1. Estudios en lógica y fundamentos de las matemáticas. Vol. 121. Ámsterdam: North-Holland. ISBN 9780444702661.

Enlaces externos

Burgess, John P. "Modelos Kripke" . Archivado del 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.Nota: Constructivo = intuicionista.
Garson, James (23 de enero de 2023). "Lógica modal" . En Zalta, Edward N. (ed.). Enciclopedia de filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .
"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 ( edición de invierno de 2022). ISSN 1095-5054 . OCLC 429049174 .

[1] La semántica de mundos posibles es un término más amplio que abarca diversos 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 maneras de modelar los 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.

[FOOTNOTEShohamLeyton-Brown2008-2] Shoham y Leyton-Brown 2008 .

[FOOTNOTEGasquetHerzigSaidSchwarzentruber201314–16-3] Gasquet y col. 2013 , págs. 14-16.

[4] Nótese 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 las lógicas clásicas no modales: En las lógicas clásicas decimos que una 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 de 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 de Kripke, un «modelo» debe entenderse más bien como un universo de discurso más amplio dentro del cual cualquier fórmula modal puede ser «entendida» de manera significativa. Así pues: mientras que la noción de «tiene un modelo» en la lógica clásica no modal 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, todo el sistema de sus axiomas y reglas de deducción).

[FOOTNOTEGiaquinto2002-5] Giaquinto 2002 .

[6] Según Andrzej Grzegorczyk .

[7] Boolos, George (1993). La lógica de la demostrabilidad . Cambridge University Press. págs. 148, 149. ISBN 0-521-43342-8.

[FOOTNOTETroelstravan_Dalen198875–875._Kripke_semantics-8] Troelstra y van Dalen 1988 , págs. 75–87, 5. Semántica de Kripke.

[FOOTNOTESimpson1994202.2_The_semantics_of_intuitionistic_logic-9] Simpson 1994 , pág. 20, 2.2 La semántica de la lógica intuicionista.

[10] Véase una formalización ligeramente diferente en Moschovakis (2022).

[FOOTNOTEGoldblatt2006b-11] Goldblatt 2006b .

[FOOTNOTEStokhof2008See_the_last_two_paragraphs_in_Section_3_'''Quasi-historical_Interlude:_the_Road_from_Vienna_to_Los_Angeles'''.-12] Stokhof 2008 , Véanse los dos últimos párrafos de la Sección 3 Interludio cuasi histórico: el camino de Viena a Los Ángeles .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]