Sintaxe de Lógica de Primeira Ordem

É composta tanto de símbolos lógicos quanto não-lógicos:

Símbolos lógicos (interpretação “fixa”):
- Pontuação: ”(”, ”)”, ”.”;
- Conectivos: $\neg$ , $\land$ , $\lor$ , $\forall$ , $\exists$ , $=$
  - Definição: $(α \supset β) \leftrightarrow (\neg α \lor β)$ ; $(α \equiv β) \leftrightarrow ((α \supset β) \land (β \supset α))$
- Variáveis: $x, y, z, \dots$
Símbolos não-lógicos (nonlogical symbols; interpretação “variável”):
- Símbolos de função: $f, g, \dots$
  - Funções de aridade 0 são chamadas de constantes.
- Símbolos de predicado: $P, Q, \dots$
  - Predicados de aridade 0 são chamados de símbolos proposicionais.

Termos e Fórmulas (bem-definidas)

O conjunto de termos é o conjunto mínimo que satisfaz as seguintes regras:

Toda variável $x, y, \dots$ é um termo;
Dados $(t_{1}, \dots, t_{n})$ termos, e $f$ uma função $n$ -ária (recebe $n$ termos), então $f (t_{1}, \dots, t_{n})$ é também um termo (funções $0$ -árias também são termos por definição).

O conjunto de fórmulas (bem-definidas) é o conjunto mínimo que satisfaz as seguintes regras:

Dados $(t_{1}, \dots, t_{n})$ termos, e $P$ um predicado $n$ -ário (recebe $n$ termos), então $P (t_{1}, \dots, t_{n})$ é também uma fórmula;
Dados $t_{1}, t_{2}$ , temos que $t_{1} = t_{2}$ é uma fórmula;
(As regras acima definem o que se chamam funções atômicas/átomos.)
Dadas fórmulas $α, β$ e uma variável $x$ , então $\neg α$ , $(α \land β)$ , $(α \lor β)$ , $\forall x . α$ , $\exists x . α$ são também fórmulas.

\forall y . P livre (x) \land \exists Bound x . [P (x) \lor Q (x)]

Qualquer fórmula sem variáveis livres é chamada de sentença.

Por exemplo:

\forall x . P (x) \lor Q (x)

é uma sentença, mas

\forall x . R (y)

não é.

BRACHMAN, Ronald J.; LEVESQUE, Hector J.; REITER, Raymond (Ed.). Knowledge representation. MIT press, 1992.