# 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

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 $\to$ e $\neg$), e o operador modal $\Box$ ("necessariamente"). O operador modal $\Diamond$ ("possivelmente") é o dual de $\Box$ e pode ser definido em termos dele assim: $\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 $\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 $\langle W,R,\Vdash \rangle$, onde $\langle W,R\rangle$ é um estrutura de Kripke, e $\Vdash$ é uma relação entre os nós de W e fórmulas modais, de tal forma que :
* $w\Vdash \neg A$ se e somente se $w\nVdash A$,
* $w\Vdash A\to B$ se e somente se $w\nVdash A$ ou $w\Vdash B$,
* $w\Vdash \Box A$ se e somente se $u\Vdash A$ para todos os $u$ tal que $w\;R\;u$.
Lemos $w\Vdash A$ como “w satisfaz A”, “A é satisfeito em w”, ou “w força A”. A relação $\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 $\langle W,R,\Vdash \rangle$, se $w\Vdash A$ para todo w ∈ W,
* um quadro $\langle W,R\rangle$, se ele é válido em $\langle W,R,\Vdash \rangle$ para todas as opções possíveis de $\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 : $\Box A\to A$. T é válido em qualquer estrutura reflexiva $\langle W,R\rangle$: se $w\Vdash \Box A$, então $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: $u\Vdash p$ se e somente se w R u. Então $w\Vdash \Box p$, thus $w\Vdash p$ por T, o que significa que w R w usando a definição de $\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$_1$ ⊆ L$_2$ são lógicas modais normais que correspondem à mesma classe de estruturas, mas L$_1$ não prova todos os teoremas de L$_2$. Então L$_1$ é Kripke incompleto. Por exemplo , o esquema $\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 $\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 | $\Box (A\to B)\to (\Box A\to \Box B)$ | N/A |
| T | $\Box A\to A$ | Reflexiva: $w\,R\,w$ |
| 4 | $\Box A\to \Box \Box A$ | Transitiva: $w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u$ |
| | $\Box \Box A\to \Box A$ | Densa: $w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)$ |
| D | $\Box A\to \Diamond A$ or $\Diamond \top$ | Em Série: $\forall w\,\exists v\,(w\,R\,v)$ |
| B | $A\to \Box \Diamond A$ | Simétrica: $w\,R\,v\Rightarrow v\,R\,w$ |
| 5 | $\Diamond A\to \Box \Diamond A$ | Euclidiana: $w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v$ |
| GL | $\Box (\Box A\to A)\to \Box A$ | R transitivo, R$^{−1}$ bem formado |
| Grz | $\Box (\Box (A\to \Box A)\to A)\to A$ | R reflexivo e transitivo, R$^{−1}$−Id bem formado |
| H | $\Box (\Box A\to B)\lor \Box (\Box B\to A)$ | $w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u$ |
| M | $\Box \Diamond A\to \Diamond \Box A$ | (uma propriedade complicada de segunda ordem) |
| G | $\Diamond \Box A\to \Box \Diamond A$ | $w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)$ |
| | $A\to \Box A$ | $w\,R\,v\Rightarrow w=v$ |
| | $\Diamond A\to \Box A$ | Função parcial: $w\,R\,u\land w\,R\,v\Rightarrow u=v$ |
| | $\Diamond A\leftrightarrow \Box A$ | função: $\forall w\,\exists !u\,w\,R\,u$ |
| | $\Box A$ or $\Box \bot$ | vazio: $\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, $\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 $\langle W,R,\Vdash \rangle$, onde W é um conjunto de todos L-MCS, e as relações R e $\Vdash$ são as seguintes:
    $X\;R\;Y$ se e somente se para toda fórmula $A$, se $\Box A\in X$ então $A\in Y$,
    $X\Vdash A$ if and only if $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 $\{\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:
    $w\Vdash \Box _{i}A$ se e somente se $\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 $\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
    $w\Vdash \Box _{i}A$ se e somente se $\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 $\langle W,\leq ,\Vdash \rangle$, onde $\langle W,\leq \rangle$ é uma estrutura Kripke pré-ordenada, e $\Vdash$ satisfaz as seguintes condições:
* se p é uma variável proposicional, $w\leq u$, and $w\Vdash p$, então $u\Vdash p$ (condição de persistência),
* $w\Vdash A\land B$ se e somente se $w\Vdash A$ e $w\Vdash B$,
* $w\Vdash A\lor B$ se e somente se $w\Vdash A$ or $w\Vdash B$,
* $w\Vdash A\to B$ se e somente se para todos $u\geq w$, $u\Vdash A$ implica $u\Vdash B$,
* não $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 é $\langle W,\leq ,\{M_{w}\}_{w\in W}\rangle$, onde $\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$_1$,…,a$_n$ ∈ M$_u$: se P(a$_1$,…,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 $w\Vdash A[e]$:
* $w\Vdash P(t_{1},\dots ,t_{n})[e]$ se e somente se $P(t_{1}[e],\dots ,t_{n}[e])$ tem em M$_w$,
* $w\Vdash (A\land B)[e]$ se e somente se $w\Vdash A[e]$ e $w\Vdash B[e]$,
* $w\Vdash (A\lor B)[e]$ se e somente se $w\Vdash A[e]$ ou $w\Vdash B[e]$,
* $w\Vdash (A\to B)[e]$ se e somente se para todo $u\geq w$, $u\Vdash A[e]$ implica $u\Vdash B[e]$,
* não $w\Vdash \bot [e]$,
* $w\Vdash (\exists x\,A)[e]$ se e somente se existe um $a\in M_{w}$ such that $w\Vdash A[e(x\to a)]$,
* $w\Vdash (\forall x\,A)[e]$ se e somente se para cada $u\geq w$ e cada $a\in M_{u}$, $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 $\langle W,R\rangle$ e $\langle W',R'\rangle$ é um mapeamento $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 $\langle W,R,\Vdash \rangle$ e $\langle W',R',\Vdash '\rangle$ é um p-morfismo de suas estruturas subjacentes $f\colon W\to W'$, que satisfaz: $w\Vdash p$ se e somente se $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 $\langle W,R\rangle$ e $\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 $w\Vdash p$ se e somente se $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 $\langle W,R,\Vdash \rangle$ e um nó fixo w$_0$ ∈ W, definimos um modelo $\langle W',R',\Vdash '\rangle$, onde W’ é o conjunto de todas as sequências finitas $s=\langle w_{0},w_{1},\dots ,w_{n}\rangle$ tal que w$_i$ R w$_{i+1}$ para todo i < n, e $s\Vdash p$ se e somente se $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
    $\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 $\langle W,R,\Vdash \rangle$ é um mapeamento f de W para um modelo $\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 $u\Vdash \Box A$, onde $\Box A\in X$, então $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, $u\Vdash A$ se e somente se $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

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)