Semânticas de Kripke

Uma semântica de Kripke - também conhecida como semântica relacional ou semântica de estruturas, e muitas vezes confundida com semântica de mundos possíveis - é uma semântica formal para sistemas lógicos não-clássicos criados no final dos anos 1950 e início dos anos 1960 por Saul Kripke. Ela foi feita primeiro para lógicas modais e, mais tarde adaptado para a lógica intuicionista e outros sistemas não-clássicos. A descoberta da semântica de Kripke foi um avanço na teoria das lógicas não-clássicas, pois a teoria dos modelos de tais lógicas era inexistente antes de Kripke.

A semântica da lógica modal

Ver artigo principal: Lógica Modal

A linguagem da lógica modal proposicional consiste em um conjunto infinito contável de variáveis ​​proposicionais , um conjunto de verdades funcionais conectivas(nesse artigo ${\displaystyle \to }$ e ${\displaystyle \neg }$), e o operador modal ${\displaystyle \Box }$ ("necessariamente"). O operador modal ${\displaystyle \Diamond }$ ("possivelmente") é o dual de ${\displaystyle \Box }$ e pode ser definido em termos dele assim: ${\displaystyle \Diamond A:=\neg \Box \neg A}$ ("possivelmente A" é definido como equivalente a "não necessariamente não A").

Definições básicas

Um estrutura de Kripke ou um estrutura modal é um par ${\displaystyle \langle W,R\rangle }$, onde W' 'é um conjunto não-vazio, e R é uma relação binária sobre W. Elementos de W são denominados nós ou mundos, e R é conhecido como relação de acessibilidade.

Um Modelo de Kripke é um conjunto ${\displaystyle \langle W,R,\Vdash \rangle }$, onde ${\displaystyle \langle W,R\rangle }$ é um estrutura de Kripke, e ${\displaystyle \Vdash }$ é uma relação entre os nós de W e fórmulas modais, de tal forma que :

• ${\displaystyle w\Vdash \neg A}$ se e somente se ${\displaystyle w\nVdash A}$,
• ${\displaystyle w\Vdash A\to B}$ se e somente se ${\displaystyle w\nVdash A}$ ou ${\displaystyle w\Vdash B}$,
• ${\displaystyle w\Vdash \Box A}$ se e somente se ${\displaystyle u\Vdash A}$ para todos os ${\displaystyle u}$ tal que ${\displaystyle w\;R\;u}$.

Lemos ${\displaystyle w\Vdash A}$ como “w satisfaz A”, “A é satisfeito em w”, ou “w força A”. A relação ${\displaystyle \Vdash }$ é chamada a relação de satisfação, de avaliação, ou de forçação. A relação de satisfação é determinada exclusivamente pelo seu valor em variáveis ​​proposicionais.

Uma fórmula A é válida em:

• um modelo ${\displaystyle \langle W,R,\Vdash \rangle }$, se ${\displaystyle w\Vdash A}$ para todo w ∈ W,
• um quadro ${\displaystyle \langle W,R\rangle }$, se ele é válido em ${\displaystyle \langle W,R,\Vdash \rangle }$ para todas as opções possíveis de ${\displaystyle \Vdash }$,
• uma classe C de estruturas ou de modelos , se é válido em cada membro de C.

Definimos Thm(C) como sendo o conjunto de todas as fórmulas que são válidas em C. Por outro lado, se X é um conjunto de fórmulas, seja Mod(X) a classe de todas as estruturas que validam cada fórmula de X.

Uma lógica modal (isto é, um conjunto de fórmulas) L é interpretado com respeito a uma classe de estruturas C , se L' ⊆ Thm(C). L é completa com C se L ⊇ Thm(C).

Correspondência e integridade

Semântica é útil para investigar a lógica (ou seja, um sistema de derivação) somente se a relação da conseqüência semântica reflete sua contraparte sintática, a relação de conseqüência sintática (derivabilidade). É vital saber quais lógicas modais são corretas e completas com relação a uma classe de estruturas de Kripke, e também para determinar qual a classe que é .

Para qualquer classe C de estruturas de Kripke, Thm(C) é uma lógica normal modal (em particular, os teoremas da lógica modal normal minimal , K, são válidos em todos os modelos de Kripke). No entanto, o inverso não se sustenta em geral. Existem lógicas modais normais Kripke-incompletas, o que não é um problema , porque a maioria dos sistemas modais estudados são classes completas de estruturas descritas por condições simples.

Um lógica modal normal L corresponde a uma classe de estruturas C , se C = Mod(L). Em outras palavras, C é a maior classe de estruturas tais que L é interpretado wrt C. Daqui resulta que L é Kripke completa, se e somente se estiver completa da sua classe correspondente.

Considere o esquema T : ${\displaystyle \Box A\to A}$. T é válido em qualquer estrutura reflexiva ${\displaystyle \langle W,R\rangle }$: se ${\displaystyle w\Vdash \Box A}$, então ${\displaystyle w\Vdash A}$ uma vez que w R w. Por outro lado , uma estrutura que valida T tem de ser reflexiva : correção w ∈ W, e definem a satisfação de uma variável p proposicional como se segue: ${\displaystyle u\Vdash p}$ se e somente se w R u. Então ${\displaystyle w\Vdash \Box p}$, thus ${\displaystyle w\Vdash p}$ por T, o que significa que w R w usando a definição de ${\displaystyle \Vdash }$. T corresponde à classe das estruturas de Kripke reflexivas.

Muitas vezes, é muito mais fácil de caracterizar a classe correspondente de L do que provar a sua corretude, assim correspondência serve como um guia para as provas de completude. A correspondência também é usada para mostrar a incompletude de lógicas modais : suponha L₁ ⊆ L₂ são lógicas modais normais que correspondem à mesma classe de estruturas, mas L₁ não prova todos os teoremas de L₂. Então L₁ é Kripke incompleto. Por exemplo , o esquema ${\displaystyle \Box (A\equiv \Box A)\to \Box A}$ gera uma lógica incompleta, uma vez que corresponde à mesma classe de estruturas como GL (ou seja, estruturas transitivas e conversas bem formadas), mas não prova a tautologia-GL ${\displaystyle \Box A\to \Box \Box A}$.

A tabela abaixo é uma lista de axiomas modais comuns , juntamente com suas classes correspondentes. A nomeação dos axiomas, muitas vezes varia.

Esquemas axioma modais comuns

Nome	Axioma	Estruturas Condicionais
K	${\displaystyle \Box (A\to B)\to (\Box A\to \Box B)}$	N/A
T	${\displaystyle \Box A\to A}$	Reflexiva: ${\displaystyle w\,R\,w}$
4	${\displaystyle \Box A\to \Box \Box A}$	Transitiva: ${\displaystyle w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u}$
	${\displaystyle \Box \Box A\to \Box A}$	Densa: ${\displaystyle w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)}$
D	${\displaystyle \Box A\to \Diamond A}$ or ${\displaystyle \Diamond \top }$	Em Série: ${\displaystyle \forall w\,\exists v\,(w\,R\,v)}$
B	${\displaystyle A\to \Box \Diamond A}$	Simétrica: ${\displaystyle w\,R\,v\Rightarrow v\,R\,w}$
5	${\displaystyle \Diamond A\to \Box \Diamond A}$	Euclidiana: ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v}$
GL	${\displaystyle \Box (\Box A\to A)\to \Box A}$	R transitivo, R^−1 bem formado
Grz	${\displaystyle \Box (\Box (A\to \Box A)\to A)\to A}$	R reflexivo e transitivo, R^−1−Id bem formado
H	${\displaystyle \Box (\Box A\to B)\lor \Box (\Box B\to A)}$	${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u}$
M	${\displaystyle \Box \Diamond A\to \Diamond \Box A}$	(uma propriedade complicada de segunda ordem)
G	${\displaystyle \Diamond \Box A\to \Box \Diamond A}$	${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)}$
	${\displaystyle A\to \Box A}$	${\displaystyle w\,R\,v\Rightarrow w=v}$
	${\displaystyle \Diamond A\to \Box A}$	Função parcial: ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u=v}$
	${\displaystyle \Diamond A\leftrightarrow \Box A}$	função: ${\displaystyle \forall w\,\exists !u\,w\,R\,u}$
	${\displaystyle \Box A}$ or ${\displaystyle \Box \bot }$	vazio: ${\displaystyle \forall w\,\forall u\,\neg (w\,R\,u)}$

Aqui está uma lista de vários sistemas modais comuns. Foram simplificadas as condições de estruturas para alguns deles: as lógicas são completas com respeito às classes de estruturas dadas na tabela, mas pode corresponder a uma classe maior de estruturas.

Lógicas modais normais comuns

nome	axiomas	estruturas condicionais
K	—	todas estruturas
T	T	reflexivas
K4	4	transitivas
S4	T, 4	pré-ordem
S5	T, 5 or D, B, 4	relação de equivalência
S4.3	T, 4, H	pré-ordem total
S4.1	T, 4, M	pré-ordem, ${\displaystyle \forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))}$
S4.2	T, 4, G	pré-ordem direcionada
GL	GL or 4, GL	finita ordem parcial estrita
Grz, S4Grz	Grz or T, 4, Grz	finite ordem parcial
D	D	em série
D45	D, 4, 5	transitive, serial, and Euclidean

Modelos canônicos

Para qualquer lógica modal normal L, um modelo de Kripke (o chamado modelo canônico) pode ser construído, o que valida precisamente os teoremas de L , ou uma adaptação da técnica padrão de utilização de conjuntos maximalmente consistentes como modelos. Modelos canônicos de Kripke desempenham um papel semelhante ao Lindenbaum - Álgebra Tarski de construção em semânticas algébricas.

Um conjunto de fórmulas é a L-consistente se qualquer contradição pode ser derivada a partir dele utilizando os teoremas de L , e Modus Ponens. Um conjunto máximo L-consistente (uma L-MCS para abreviar) é um conjunto L-consistente que não tem supraconjunto L-consistente adequado.

Um modelo canônico de L é um modelo de Kripke ${\displaystyle \langle W,R,\Vdash \rangle }$, onde W é um conjunto de todos L-MCS, e as relações R e ${\displaystyle \Vdash }$ são as seguintes:

${\displaystyle X\;R\;Y}$ se e somente se para toda fórmula ${\displaystyle A}$, se ${\displaystyle \Box A\in X}$ então ${\displaystyle A\in Y}$,

${\displaystyle X\Vdash A}$ if and only if ${\displaystyle A\in X}$.

O modelo canônico é um modelo de L, como todos os L-MCS contém todos os teoremas de L. pelo Lema de Zorn, cada conjunto L-consistente está contido em um L-MCS, em particular, cada fórmula indemonstrável em L tem um contra-exemplo no modelo canônico.

A principal aplicação de modelos canônicos é nas provas de completude. Propriedades do modelo canónico de K implica imediatamente completude de K em relação à classe de todos as estruturas de Kripke. Este argumento não funciona para L arbitrário, porque não há nenhuma garantia de que a estrutura subjacente do modelo canônico satisfaz as condições de estrutura de L.

Dizemos que uma fórmula ou um conjunto X de fórmulas é canônico com respeito a uma propriedade P de estruturas de Kripke, se

• X é válida em todos as estruturas que satisfaz P,
• para qualquer lógica modal L normal, que contém X, a estrutura subjacente ao modelo canônico de L satisfaz P.

A união dos conjuntos canônicos de fórmulas é a própria canônica. Segue-se a partir da discussão anterior de que qualquer lógica axiomatizada por um conjunto canônico de fórmulas é Kripke completo e compacto.

Os axiomas T , 4, D , B, 5 , H , G ​​(e, portanto, qualquer combinação de ambos) são canónicos . GL e Grz não são canônicos , porque eles não são compactos. O axioma M por si só não é canônico (Goldblatt, 1991), mas a lógica combinada S4.1 (na verdade , mesmo K4.1) é canônica.

Em geral, é indecidível se um determinado axioma é canônico. Sabemos uma condição suficiente agradável: H. Sahlqvist identificou uma ampla classe de fórmulas (agora chamado de fórmulas Sahlqvist) tal que

• uma fórmula Sahlqvist é canônica,
• a classe das estruturas correspondentes a uma fórmula Sahlqvist é definível em primeira ordem,
• existe um algoritmo que calcula a condição de estrutura correspondente a uma determinada fórmula Sahlqvist.

Este é um critério poderoso: por exemplo, todos os axiomas listados acima são canônicos como (equivalente a) as fórmulas Sahlqvist.

Propriedade de modelo finito

Uma lógica tem a propriedade de modelo finito (FMP), se ela for completa no que diz respeito a uma classe de estruturas finitas. Uma aplicação deste conceito é a questão da decidibilidade: segue-se do teorema de Post que a lógica modal L recursivamente axiomatizada que tem FMP é decidível, desde que seja decidível se um determinada estrutura finita é um modelo de L. Em particular, cada lógica finitamente axiomatizável com FMP é decidível.

Existem vários métodos para a criação de um determinado FMP lógico. Refinamentos e extensões da construção do modelo canônico, muitas vezes o trabalho, utilizando ferramentas como filtração ou investigação. Como outra possibilidade, as provas de completude com base em cálculos subseqüentes de corte-livre costumam produzir modelos finitos diretamente.

A maioria dos sistemas modais usados ​​na prática (incluindo todos os listados acima) têm FMP .

Em alguns casos, pode-se utilizar FMP para provar a Kripke-completude de uma lógica: cada lógica modal normal é completa com respeito a uma classe de álgebra modal , e uma álgebra modal finita pode ser transformada numa estrutura Kripke. Como um exemplo, Robert Bull provou usando este método que cada extensão normal de S4.3 tem FMP , e é Kripke completa.

Lógicas Multimodais

Kripke semântica tem uma generalização simples de lógica com mais de uma modalidade. Uma estrutura de Kripke para uma linguagem com ${\displaystyle \{\Box _{i}\mid \,i\in I\}}$ como o conjunto de suas necessidades de operadores consiste em um W equipado com relações binárias R_i para cada i ∈ I. A definição de uma relação de satisfação é alterada da seguinte forma:

${\displaystyle w\Vdash \Box _{i}A}$ se e somente se ${\displaystyle \forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).}$

A semântica simplificada, descoberta por Tim Carlson , é muitas vezes utilizada para lógicas demonstravelmente polimodais. Um modelo de Carlson é uma estrutura ${\displaystyle \langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle }$ com um único relação de acessibilidade R, e subconjuntos D_i ⊆ W para cada modalidade. A satisfação é definida como

${\displaystyle w\Vdash \Box _{i}A}$ se e somente se ${\displaystyle \forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).}$

Carlson modelos são mais fáceis de visualizar do que os usuais modelos de Kripke polomodais, há , no entanto, lógicas polimodais Kripke-completas que são Carlson-incompletas.

A semântica da lógica intuicionística

A Semantica Kripke para a lógica intuicionística segue os mesmos princípios que a semântica da lógica modal, mas ela usa uma definição diferente de satisfação.

Um modelo intuicionista de Kripke is ${\displaystyle \langle W,\leq ,\Vdash \rangle }$, onde ${\displaystyle \langle W,\leq \rangle }$ é uma estrutura Kripke pré-ordenada, e ${\displaystyle \Vdash }$ satisfaz as seguintes condições:

• se p é uma variável proposicional, ${\displaystyle w\leq u}$, and ${\displaystyle w\Vdash p}$, então ${\displaystyle u\Vdash p}$ (condição de persistência),
• ${\displaystyle w\Vdash A\land B}$ se e somente se ${\displaystyle w\Vdash A}$ e ${\displaystyle w\Vdash B}$,
• ${\displaystyle w\Vdash A\lor B}$ se e somente se ${\displaystyle w\Vdash A}$ or ${\displaystyle w\Vdash B}$,
• ${\displaystyle w\Vdash A\to B}$ se e somente se para todos ${\displaystyle u\geq w}$, ${\displaystyle u\Vdash A}$ implica ${\displaystyle u\Vdash B}$,
• não ${\displaystyle w\Vdash \bot }$.

A negação de A, ¬A, pode ser definida como uma abreviação para A → ⊥. Se para todos os u tal que w ≤ u, não u ⊩ A, então w ⊩ A → ⊥ é uma verdade vazia, então w ⊩ ¬A.

A Lógica intuicionística é correta e completa em relação às semânticas Kripke, e tem FMP.

Lógica primeira ordem intuicionista

Seja L uma linguagem de primeira ordem. Um modelo de Kripke de L é ${\displaystyle \langle W,\leq ,\{M_{w}\}_{w\in W}\rangle }$, onde ${\displaystyle \langle W,\leq \rangle }$ é uma estrutura de Kripke intuicionistica, M_w é uma (clássica) L-estrutura para cada nó w ∈ W, e as seguintes condições de compatibilidade mantêm sempre u ≤ v:

• o domínio de M_u está incluído no domínio de M_v,
• realizações de símbolos de função em M_u e M_v concorda com elementos de M_u,
• para cada predicado n-ário P e elementos a₁,…,a_n ∈ M_u: se P(a₁,…,a_n) tem em M_u, então ele tem em M_v.

Dada uma avaliação e das variáveis ​​por elementos de M_w,definimos a relação satisfação ${\displaystyle w\Vdash A[e]}$:

• ${\displaystyle w\Vdash P(t_{1},\dots ,t_{n})[e]}$ se e somente se ${\displaystyle P(t_{1}[e],\dots ,t_{n}[e])}$ tem em M_w,
• ${\displaystyle w\Vdash (A\land B)[e]}$ se e somente se ${\displaystyle w\Vdash A[e]}$ e ${\displaystyle w\Vdash B[e]}$,
• ${\displaystyle w\Vdash (A\lor B)[e]}$ se e somente se ${\displaystyle w\Vdash A[e]}$ ou ${\displaystyle w\Vdash B[e]}$,
• ${\displaystyle w\Vdash (A\to B)[e]}$ se e somente se para todo ${\displaystyle u\geq w}$, ${\displaystyle u\Vdash A[e]}$ implica ${\displaystyle u\Vdash B[e]}$,
• não ${\displaystyle w\Vdash \bot [e]}$,
• ${\displaystyle w\Vdash (\exists x\,A)[e]}$ se e somente se existe um ${\displaystyle a\in M_{w}}$ such that ${\displaystyle w\Vdash A[e(x\to a)]}$,
• ${\displaystyle w\Vdash (\forall x\,A)[e]}$ se e somente se para cada ${\displaystyle u\geq w}$ e cada ${\displaystyle a\in M_{u}}$, ${\displaystyle u\Vdash A[e(x\to a)]}$.

Esse e(x→a) é a avaliação que dá x o valor a, de outra forma concorda com e.

Semântica Kripke–Joyal

Como parte do desenvolvimento independente da teoria dos feixes, foi realizada por volta de 1965 que a semântica de Kripke estava intimamente relacionada ao tratamento de quantificação existencial, em teoria de topos.

Ou seja, o aspecto 'local' da existência de seções de um feixe era uma espécie de lógica do 'possível'. Embora este desenvolvimento foi o trabalho de um número de pessoas, o nome semântica de Kripke-Joyal é frequentemente utilizado neste contexto.

Construções de Modelos

Tal como na teoria de modelos clássica, existem métodos para a construção de um novo modelo de Kripke a partir de outros modelos .

Os homomorfismos naturais na semântica Kripke são chamados p-morfismos (que é abreviação para pseudo-epimorfismo, mas este último termo é raramente usado). Um p-morfismo das estruturas Kripke ${\displaystyle \langle W,R\rangle }$ e ${\displaystyle \langle W',R'\rangle }$ é um mapeamento ${\displaystyle f\colon W\to W'}$ de tal forma que

• f preserva a relação de acessibilidade, ou seja, u R v implica f(u) R’ f(v),
• sempre que f(u) R’ v’, existe um v ∈ W de tal forma que u R v e f(v) = v’.

Um p-morfismo de modelos de Kripke ${\displaystyle \langle W,R,\Vdash \rangle }$ e ${\displaystyle \langle W',R',\Vdash '\rangle }$ é um p-morfismo de suas estruturas subjacentes ${\displaystyle f\colon W\to W'}$, que satisfaz: ${\displaystyle w\Vdash p}$ se e somente se ${\displaystyle f(w)\Vdash 'p}$, para qualquer variável proposicional p.

P-morfismos são um tipo especial de bisimulações. Em geral, uma bisimulação entre as estruturas ${\displaystyle \langle W,R\rangle }$ e ${\displaystyle \langle W',R'\rangle }$ é uma relação B ⊆ W × W’, que satisfaz o seguinte propriedade “zig-zag”:

• se u B u’ e u R v, existe v’ ∈ W’ tal que v B v’ e u’ R’ v’,
• se u B u’ e u’ R’ v’, existe v ∈ W tal que v B v’ e u R v.

Uma bisimulação de modelos é adicionalmente necessário para preservar a força de fórmulas atômicas:

se w B w’, então ${\displaystyle w\Vdash p}$ se e somente se ${\displaystyle w'\Vdash 'p}$, para qualquer variável proposicional p.

A propriedade fundamental que decorre desta definição é que bisimulações (daí também p-morfismo) de modelos de preservam a satisfação de todas as fórmulas, não apenas variáveis ​​proposicionais.

Podemos transformar um modelo de Kripke em uma árvore usando Desembaraçamento. Dado um modelo ${\displaystyle \langle W,R,\Vdash \rangle }$ e um nó fixo w₀ ∈ W, definimos um modelo ${\displaystyle \langle W',R',\Vdash '\rangle }$, onde W’ é o conjunto de todas as sequências finitas ${\displaystyle s=\langle w_{0},w_{1},\dots ,w_{n}\rangle }$ tal que w_i R w_i+1 para todo i < n, e ${\displaystyle s\Vdash p}$ se e somente se ${\displaystyle w_{n}\Vdash p}$ para uma variável proposicional p. A definição de uma relação de acessibilidade R’ varia; no caso mais simples colocamos

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

mas muitas aplicações necessitam o fechamento reflexivo e/ou transitiva desta relação , ou modificações semelhantes.

Filtração é uma construção útil que usa para provar FMP para muitas lógicas . Seja X um conjunto de fórmulas fechadas sob subformulas. Uma X'-filtração de um modelo ${\displaystyle \langle W,R,\Vdash \rangle }$ é um mapeamento f de W para um modelo ${\displaystyle \langle W',R',\Vdash '\rangle }$ tal que

• f é uma surjeção,
• f preserva a relação de acessibilidade, e ( nos dois sentidos) satisfação das variáveis p ∈ X,
• se f(u) R’ f(v) e ${\displaystyle u\Vdash \Box A}$, onde ${\displaystyle \Box A\in X}$, então ${\displaystyle v\Vdash A}$.

Segue-se que f preserva a satisfação de todas as fórmulas de X. Em aplicações típicas , tomamos f como a projeção para o quociente de W sobre a relação: u ≡_X v se e somente se para todo A ∈ X, ${\displaystyle u\Vdash A}$ se e somente se ${\displaystyle v\Vdash A}$. Tal como no caso de desembaraçamento, a definição da relação de acessibilidade no quociente varia.

Estruturas semânticas gerais

O principal defeito da semântica de Kripke é a existência de lógicas Kripke-incompletas e lógicas que são completas, mas não compactas. Isso pode ser sanado equipando quadros de Kripke com estrutura adicional que restringe o conjunto de possíveis valorações, usando ideias das semânticas algébricas. Isto dá origem à estrutura semântica geral.

Aplicações na Ciência da Computação

Ver artigos principais: Kripke structure, state transition system, e model checking

Blackburn et al. (2001) apontam que, por que uma estrutura relacional é simplesmente um conjunto juntamente com um conjunto de relações sobre o conjunto, não é surpreendente que as estruturas relacionais podem ser encontradas em praticamente qualquer lugar. Como um exemplo de ciência da computação teórica, eles dão os sistemas de transição rotulados, que a execução do programa do modelo. Blackburn et ai. assim reivindicam por causa dessa conexão que as linguagens modais são ideais no fornecimento de uma perspectiva "interna, local em estruturas relacionais. " (p. xii)

Ver também

• Lógica modal e normal

Referencias

• Blackburn, P., M. de Rijke, and Y. Venema, 2001. Modal Logic. Cambridge University Press.
• Bull, Robert. A., and K. Segerberg, 1984, "Basic Modal Logic" in The Handbook of Philosophical Logic, vol. 2. Kluwer: 1–88.
• Chagrov, A, and Zakharyaschev, M., 1997. Modal Logic. Oxford University Press.
• Michael Dummett, 1977. Elements of Intuitionism. Oxford Univ. Press.
• Fitting, Melvin, 1969. Intuitionistic Logic, Model Theory and Forcing. North Holland.
• Robert Goldblatt (link), 2003, "Mathematical Modal Logic: a View of its Evolution", In Logic & the Modalities in the Twentieth Century, volume 7 of the Handbook of the History of Logic, edited by Dov M. Gabbay and John Woods, Elsevier, 2006, 1-98.
• Hughes, G. E., and M. J. Cresswell, 1996. A New Introduction to Modal Logic. Routledge.
• Saunders Mac Lane and Moerdijk, I., 1991. Sheaves in Geometry and Logic. Springer-Verlag.
• van Dalen, Dirk, 1986, "Intuitionistic Logic" in The Handbook of Philosophical Logic, vol. 3. Reidel: 225–339.

Ligações externas

• The Stanford Encyclopedia of Philosophy: "Modal Logic" — by James Garson.
• Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.
• Detlovs and Podnieks, K., "Constructive Propositional Logic — Kripke Semantics." Chapter 4.4 of Introduction to Mathematical Logic. N.B: Constructive = intuitionistic.
• Burgess, John P., "Kripke Models."
• Hazewinkel, Michiel, ed. (2001), «Kripke models», Enciclopédia de Matemática, ISBN 978-1-55608-010-4 (em inglês), Springer