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 $\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₁ ⊆ 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 $\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₁,…,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 $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₀ ∈ 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

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