Semânticas de Kripke

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Wikitext.svg
Este artigo ou seção precisa ser wikificado (desde setembro de 2013).
Por favor ajude a formatar este artigo de acordo com as diretrizes estabelecidas no livro de estilo.

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 intuicionística 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 L1 ⊆ L2 são lógicas modais normais que correspondem à mesma classe de estruturas, mas L1 não prova todos os teoremas de L2. Então L1 é 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−1Id 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 Ri 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 Di ⊆ 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[editar | editar código-fonte]

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,\le,\Vdash\rangle, onde \langle W,\le\rangle é uma estrutura Kripke pré-ordenada, e \Vdash satisfaz as seguintes condições:

  • se p é uma variável proposicional, w\le 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\ge 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 wu, 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[editar | editar código-fonte]

Seja L uma linguagem de primeira ordem. Um modelo de Kripke de L é \langle W,\le,\{M_w\}_{w\in W}\rangle, onde \langle W,\le\rangle é uma estrutura de Kripke intuicionistica, Mw é 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 Mu está incluído no domínio de Mv,
  • realizações de símbolos de função em Mu e Mv concorda com elementos de Mu,
  • para cada predicado n-ário P e elementos a1,…,an ∈ Mu: se P(a1,…,an) tem em Mu, então ele tem em Mv.

Dada uma avaliação e das variáveis ​​por elementos de Mw,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 Mw,
  • 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\ge 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\ge w e cada a\in M_u, u\Vdash A[e(x\to a)].

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

Semântica Kripke–Joyal[editar | editar código-fonte]

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[editar | editar código-fonte]

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(uR’ f(v),
  • sempre que f(uR’ 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 w0 ∈ 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 wi R wi+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(uR’ 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[editar | editar código-fonte]

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 idéias das semânticas algébricas. Isto dá origem à estrutura semântica geral.

Aplicações na Ciência da Computação[editar | editar código-fonte]

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)


Veja Também[editar | editar código-fonte]

Referencias[editar | editar código-fonte]

  • 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[editar | editar código-fonte]

O Commons possui uma categoria contendo imagens e outros ficheiros sobre Semânticas de Kripke