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

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 satisfazA”, “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

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−1−Id 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

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

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

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