Semântica de Lógica de Primeira Ordem

Semântica em Lógica de Primeira Ordem

A principal ideia é de que, dados símbolos em uma lógica de primeira ordem, assinamos sentido a eles mediante mapas de interpretação.

Definição: Lookup Table/Variable Assignment

Dada uma interpretação , temos uma função (lookup table em Huth)

que é um mapa indo do (conjunto das variáveis da linguagem) até o (domínio da interpretação ).

Tal mapa pode ser considerado como uma realização das variáveis (que são só símbolos) em objetos interpretáveis no domínio .

Definição: Denotação de Termos

Dada uma interpretação e uma lookup table , definimos a denotação de termos como

como

• Caso seja uma variável, só aplicamos a função :
• Dados termos e um símbolo de função -ária , então

Note-se que tais termos denotados serão sempre elementos do domínio de discurso .

Definição: Satisfação/Entailment/Consequência Lógica

Dada uma interpretação e uma lookup table , dizemos que uma fórmula é satisfeita na interpretação — e que escrevemos como segundo Levesque, e segundo Huth — de acordo com as seguintes regras:

• Dados termos e predicado -ário , então

• for falso que ;
• e
• ou
• para alguma lookup table que difira de em no máximo
• para qualquer lookup table que difira de em no máximo

Caso particular: satisfação de sentenças

Como sentenças são fórmulas sem variáveis livres, elas são invariantes a variable assignments . Por isso, escrevemos que