Linguagem Formal do Cálculo de Predicados

A linguagem formal do cálculo de predicados consiste em:

Variáveis: u, v, w, x, y, z, ..., e estas letras indexadas.

Constantes: a, b, ...,e, i, j, ..., t, e estas letras indexadas.

Símbolos funcionais: f, g, h, e estas letras indexadas.

Símbolos de predicados: A, B, C, ..., e estas letras indexadas.

Conectivos: .

Quantificadores: .

Parenteses: (, ).

Definição de termo:

1. As constantes e as variáveis são termos.
2. Se é um símbolo de função de n variáveis e são termos, então é um termo.
3. Nada mais é termo.

Se é um símbolo de predicado n-ário e são termos então é uma fórmula atómica.

Definição de fórmula:

1. Uma fórmula atómica é uma fórmula.
2. Se e são fórmulas então

   são fórmulas.

3. Se é uma variável e é uma fórmula então

   são fórmulas.

4. Nada mais é fórmula.

O alcance de um quantificador que ocorre numa fórmula é o próprio quantificador junto com a mais pequena fórmula que o segue.

Uma ocorrência de uma variável, , numa fórmula diz-se muda se estiver no alcance de um quantificador ou . Caso contrário diz-se livre.

Uma variável diz-se muda numa fórmula se tiver pelo menos uma ocorrência muda nessa fórmula. Uma variável diz-se livre numa fórmula se tiver pelo menos uma ocorrência livre nessa fórmula.

Uma fórmula sem variáveis livres é uma proposição (ou sentença). Caso contrário é uma expressão proposicioal (ou condição).