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

editar
 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   e  ), e o operador modal   ("necessariamente"). O operador modal   ("possivelmente") é o dual de   e pode ser definido em termos dele assim:   ("possivelmente A" é definido como equivalente a "não necessariamente não A").

Definições básicas

editar

Um estrutura de Kripke ou um estrutura modal é um par  , 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  , onde   é um estrutura de Kripke, e   é uma relação entre os nós de W e fórmulas modais, de tal forma que :

  •   se e somente se  ,
  •   se e somente se   ou  ,
  •   se e somente se   para todos os   tal que  .

Lemos   como “w satisfaz A”, “A é satisfeito em w”, ou “w força A”. A relação   é 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  , se   para todo w ∈ W,
  • um quadro  , se ele é válido em   para todas as opções possíveis de  ,
  • 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

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 :  . T é válido em qualquer estrutura reflexiva  : se  , então   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:   se e somente se w R u. Então  , thus   por T, o que significa que w R w usando a definição de  . 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   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  .

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   N/A
T   Reflexiva:  
4   Transitiva:  
  Densa:  
D   or   Em Série:  
B   Simétrica:  
5   Euclidiana:  
GL   R transitivo, R−1 bem formado
Grz   R reflexivo e transitivo, R−1Id bem formado
H    
M   (uma propriedade complicada de segunda ordem)
G    
   
  Função parcial:  
  função:  
  or   vazio:  

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,  
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

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  , onde W é um conjunto de todos L-MCS, e as relações R e   são as seguintes:

  se e somente se para toda fórmula  , se   então  ,
  if and only if  .

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

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

Kripke semântica tem uma generalização simples de lógica com mais de uma modalidade. Uma estrutura de Kripke para uma linguagem com   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:

  se e somente se  

A semântica simplificada, descoberta por Tim Carlson , é muitas vezes utilizada para lógicas demonstravelmente polimodais. Um modelo de Carlson é uma estrutura   com um único relação de acessibilidade R, e subconjuntos Di ⊆ W para cada modalidade. A satisfação é definida como

  se e somente se  

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

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

  • se p é uma variável proposicional,  , and  , então   (condição de persistência),
  •   se e somente se   e  ,
  •   se e somente se   or  ,
  •   se e somente se para todos  ,   implica  ,
  • não  .

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

Seja L uma linguagem de primeira ordem. Um modelo de Kripke de L é  , onde   é 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  :

  •   se e somente se   tem em Mw,
  •   se e somente se   e  ,
  •   se e somente se   ou  ,
  •   se e somente se para todo  ,   implica  ,
  • não  ,
  •   se e somente se existe um   such that  ,
  •   se e somente se para cada   e cada  ,  .

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

Semântica Kripke–Joyal

editar

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

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   e   é um mapeamento   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   e   é um p-morfismo de suas estruturas subjacentes  , que satisfaz:   se e somente se  , para qualquer variável proposicional p.

P-morfismos são um tipo especial de bisimulações. Em geral, uma bisimulação entre as estruturas   e   é 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   se e somente se  , 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   e um nó fixo w0 ∈ W, definimos um modelo  , onde W’ é o conjunto de todas as sequências finitas   tal que wi R wi+1 para todo i < n, e   se e somente se   para uma variável proposicional p. A definição de uma relação de acessibilidade R’ varia; no caso mais simples colocamos

 ,

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   é um mapeamento f de W para um modelo   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  , onde  , então  .

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,   se e somente se  . Tal como no caso de desembaraçamento, a definição da relação de acessibilidade no quociente varia.

Estruturas semânticas gerais

editar

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

editar

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

editar

Referencias

editar
  • 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
 
O Commons possui uma categoria com imagens e outros ficheiros sobre Semânticas de Kripke