Estrutura de interpretação (lógica)
Na lógica, uma estrutura (ou estrutura de interpretação) é um objeto que dá significado semântico ou interpretação aos símbolos definidos pela assinatura de uma linguagem. Uma estrutura possui diferentes configurações, seja em lógicas de primeira ordem, seja em linguagens lógicas poli-sortidas ou de ordem superior.
Estruturas de primeira ordem
editarUma assinatura Σ de uma linguagem de primeira ordem consiste de um conjunto Cst de símbolos de constantes e de conjuntos Funn e Reln de símbolos de funções e relações n-árias, respectivamente. Uma Σ-estrutura para tal linguagem consiste de um par , no qual DI será o universo (ou domínio) de discurso, e I é uma intepretação para os símbolos da linguagem, na qual vale as definições:
- Os símbolos de constantes são interpretados como "nomes" que se referem a um objeto do universo, são funções 0-árias em DI. Em outras palavras, para cada c ∈ Cst, há um objeto específico cI ∈ DI
- Cada símbolo de função n-ária fn ∈ Funn é interpretado como uma função específica .
- Cada símbolo de relação n-ária Rn ∈ Reln é interpretado como um subconjunto do produto cartesiano , ou seja, o conjunto das n-uplas ordenadas que satisfazem RIn.
Exemplo
editarNa álgebra booleana binária uma assinatura é constituída por:
E uma estrutura para essa assinatura é:
- O símbolo de constante 0 é interpretado como o próprio objeto 0 (valor de verdade falso) e o símbolo 1, como o próprio 1 (verdadeiro).
- : Negação de x;
- : X ou y é verdadeiro (1);
- : X e y são verdadeiros.
Assim, a sentença é verdadeira apenas para uma atribuição ρ tal que ρ(x)=1 e ρ(y)=0.
Algumas definições sobre estruturas
editarSubestrutura
editarUma estrutura é dita subestrutura de outra estrutura para a mesma assinatura, denotado por , se:
- ;
- para toda constante c ∈ Cst;
- para toda função fn ∈ Funn. Assim sendo, ;
- para toda relação Rn ∈ Reln.
Homomorfismo e Isomorfismo
editarDadas duas estruturas e para uma mesma assinatura, um homomorfismo é uma função tal que:
- Para todo c ∈ Cst,
- Para toda fn ∈ Funn e {a1,...,an} ⊆ DI,
- Para toda Rn ∈ Reln e {a1,...,an} ⊆ DI,
Diz-se que h é isomorfismo se a função for bijetiva, ou seja, o homomorfismo também vale.
Relação de satisfação
editarSeja φ uma fórmula bem-formada, uma estrutura, e ρ uma atribuição, a relação de satisfação ou consequência, na qual ρ satisfaz φ em M denotado por , define-se através do esquema-T por:
- ;
- ;
- ;
- ;
- para toda atribuição ρ'=ρ[x:=k], para todo k ∈ DI.
Modelo de teorias de primeira-ordem
editarUma estrutura é dita um modelo de uma teoria quando ambas têm a mesma linguagem e toda sentença consistente da teoria é satisfeita por tal estrutura. Assim, por exemplo, um anel é uma estrutura que satisfaz todos os axiomas da teoria dos anéis, e um modelo para a teoria das ordens parciais é uma estrutura com apenas um símbolo ≤ e que deve satisfazer os axiomas das ordens parciais.
"M é modelo de φ" denota-se por .
Definibilidade em uma estrutura
editarUma relação n-ária R em um universo DI de uma estrutura M é dita definível (ou explicitamente definível) se há uma fórmula φ(x1,...,xn), onde x1,...,xn são as variáveis livres de φ, tal que:
Ou seja,
- .
Um caso especial importante é a definibilidade de elementos específicos. Um elemento a ∈ DI é definível em M sse há uma fórmula φ(x) tal que
- .
Definibilidade com parâmetros
editarUma relação R é dita definível em parâmetros se há uma sentença φ com parâmetros de M tal que R é definível usando φ. Todo elemento da uma estrutura é definível usando ele próprio como parâmetro.
Definibilidade implícita
editarProvém das definições acima que a fórmula φ pode não mencionar R, já que o mesmo pode não estar na linguagem de M. Se há uma fórmula φ na linguagem estendida contendo M e o novo símbolo R, e R é a única relação tal que , então R é dita implicitamente definível em M.
Generalizações
editarEstruturas poli-sortidas
editarUma linguagem poli-sortida inclui mais de um domínio de discurso. Por exemplo, a axiomatização em primeira ordem da lógica de segunda ordem inclui um tipo para números naturais e um tipo para conjuntos de números naturais. A definição de uma estrutura poli-sortida é a convencional, porém ao invés de um único universo de discurso, há vários, um para cada tipo.
Linguagens de ordem superior
editarHá mais de uma semântica possível para lógicas de ordem superior. Uma vez usando a semântica de ordem superior completa, uma estrutura necessita apenas de um universo para predicados, e o Esquema T é expandido para um quantificador sobre um tipo de ordem superior.
Requerimento de domínio não-vazio
editarAfirma-se acima que uma interpretação deve especificar um domínio não-vazio para ser o universo de discurso. Uma razão importante para isto é assim de modo a equivalências como
- ,
onde x não é livre em φ, serem logicamente válidas. Esta equivalência não é logicamente válida quando estruturas vazias são permitidas (por exemplo, assuma que φ seja e ψ seja ). Portanto, a teoria da demonstração da lógica de primeira ordem torna-se muito mais complicada quando estruturas com domínio vazio são permitidas, enquanto que o ganho em permití-las é pequeno, já que tanto as interpretações pretendidas como as interpretações interessantes das teorias que as pessoas estudam possuem domínios não-vazios. A dificuldade com domínios vazios está em certas regras de inferência que permitem que quantificadores sejam externalizados sobre conectivos lógicos. Para um exemplo concreto, considere
Esta estrutura é satisfeita por um domínio vazio. Para colocá-la na forma normal prenex, queremos mover o quantificador existencial para obter
Mas esta nova fórmula não é satisfeita por um domínio vazio, já que não existe nenhum elemento com o qual o quantificador existencial possa ser instanciado. O problema subjacente é que o escopo do quantificador existencial foi modificado para incluir o disjunto mais à esquerda.
As relações vazias, entretanto, não causam este problema, uma vez que não existe um conceito semelhante de externalizar um símbolo de relação sobre um conectivo lógico, alargando seu escopo no processo.
Ver também
editarLigações externas
editar- Um Curso de Teoria dos Modelos(arquivo em .pdf), por Marcelo E. Coniglio.