Sintaxe da Lógica de Primeira Ordem

A sintaxe da Lógica de Primeira Ordem mantém os conectivos da Lógica Proposicional e adiciona termos para designar objetos e fórmulas para representar relações entre esses objetos.

$$ \Huge p(a) \quad \forall x~p(x) \qquad \exists y~g(x) = h(x,a) $$

A sintaxe e as regras da Dedução Natural Proposicional continuam válidas.

São acrescentados termos: constantes, funções e variáveis.
As fórmulas acrescentam relações e quantificadores às proposições.

Por enquanto definem-se todos estes conceitos novos. Mais tarde são tratadas as regras de dedução e da semântica para a Lógica de Primeira Ordem.

Termos e Fórmulas

$$\large \begin{gathered} 2, \lit{Lua}, \lit{Lógica e Computação}, \lit{Aragorn}, \lit{Ariadne} \cr 2 > 3, \fat{Primo}{21}, \fat{Satélite}{\lit{Lua}, \lit{Terra}}, \fat{Humano}{\lit{Legolas}} \cr \forall x~\fat{Anão}{x} \to \exists y~\fat{Elfo}{y} \land \fat{Amigo}{x, y} \cr \forall p~\fat{Brisa}{p}\to \exists y~\fat{Adjacente}{p, y}\land\fat{Poço}{y} \end{gathered} $$

Os termos são definidos por constantes, funções e por variáveis; Identificam objetos.
As fórmulas são definidas por relações, conectivos e expressões com quantificadores. Tal como as proposições da Lógica Proposicional, descrevem factos.

Termos

Definição (Termo)

Sejam $\cat{V}, \cat{C}, \cat{F}$ conjuntos de símbolos (para as variáveis, as constantes e as funções, respetivamente). São termos:

Átomos. Qualquer constante de $\cat{C}$ e qualquer variável de $\cat{V}$.
Funções. Se $f_n\in \cat{F}$ e $t_1, \ldots, t_n$ forem termos então $f\at{t_1, \ldots, t_n}$ é um termo.

Um termo em que não ocorrem variáveis diz-se fechado. Caso contrário diz-se aberto.

Em geral, a aridade faz parte da especificação de cada símbolo funcional $f \in \cat{F}$ (e a seguir de cada $r \in \cat{R}$). Quando necessário indica-se a aridade com um indice — $f_2$ é binária, $g_7$ é $7$-ária, etc.

Exemplos. Termos

Átomos: $2$, $\lit{Lua}$, $\lit{Aragorn}$, $\lit{Ariadne}$, $x$.
Funções: $1+1$, $\fat{Satélite}{\lit{Terra}}$, $\sin\at{\frac{\pi}{2}} + e^{i \pi}$, $a + x$, $f\at{}$.

Não são termos:

$1 + \frac{1}{2} + \frac{1}{4} + \cdots~$ é uma expressão infinita.
$\fat{Par}{2}$ é uma proposição (verdade/falso).
$x > y$ é uma proposição.
$\sin$ é um símbolo funcional mas a expressão não está completa.

Fórmulas

Definição (Fórmula)

Sejam $\cat{V}, \cat{C}, \cat{F}$ como na definição de termos e $\cat{R}$ um conjunto de símbolos de relações. São fórmulas:

Igualdade. Se $a, b$ forem termos, $a = b$ é uma fórmula.
Conectivos. Se $p, q$ forem fórmulas, $\neg p, p \land q, p \lor q, p \to q$ são fórmulas.
Relações. Se $t_1, \ldots, t_n$ forem termos e $r_n \in \cat{R}$ então $r\at{t_1, \ldots, t_n}$ é uma fórmula.
Quantificadores. Se $x$ for uma variável e $p$ uma fórmula, $\forall x~p$ e $\exists x~p$ são fórmulas.

Exemplos. Fórmulas

Igualdade. $2 = 2$, $2 = 1$, $\lit{Lua} = \fat{Satélite}{\lit{Terra}}$.
Conectivos. $\lit{Lua} = \fat{Satélite}{\lit{Terra}} \land \fat{Massa}{\lit{Lua}} < \fat{Massa}{\lit{Terra}}$.
Relações. $\fat{Par}{2} \lor x > 3$.
Quantificadores. $\del{\forall x~\fat{Par}{x}}\to 2 < 1$.

Não são fórmulas:

$2$, $\lit{Lua}$, $x$, $0+1+2+y$ porque são termos.
$=$, $<$, $\lit{Par}$ são símbolos relacionais mas as expressões estão incompletas.
$\fat{Par}{2} > 4$ é um erro de sintaxe. Se quisermos dizer “Dois é um número par maior que quarto” devemos escrever $\fat{Par}{2} \land 2 > 4$.
$\fat{Par}{0} \land \fat{Par}{2} \land \fat{Par}{4} \land \cdots~$ é uma expressão infinita.

Sobre a Igualdade

Um uso da igualdade é nas formação de fórmulas, por exemplo, $2 + 2 = 4$.
Outro uso é quando comparamos as expressões “$2 + 2$” e “$4$” que são, obviamente, diferentes.
Quando for necessário distinguir o primeiro caso do segundo, usa-se a notação $==$ (dois “$=$”) para indicar a igualdade de expressões.

Escrita natural e Escrita formal

A escrita natural de termos e fórmulas comuns é diferente, mas equivalente, à sua escrita formal.

Nesta tabela estão várias expressões apresentadas na escrita natural usadas no dia-a-dia e a respetiva notação formal que segue as definições de termo e de fórmula.

$$ \begin{array}{ll|lr} \text{Escrita~}\textit{natural} & \text{Escrita~}\textit{formal} & \text{Tipo} & \text{Resultado} \cr \hline 2 + 3 & \fat{Soma}{2, 3} & \text{função} & \text{termo} \cr n < 3 & \fat{Menor}{n,3} & \text{relação} & \text{fórmula} \cr e^x & \fat{Exp}{x} & \text{função} & \text{termo} \cr \sin\at{z} & \fat{Sin}{z} & \text{função} & \text{termo} \cr 4 = 5 \dfrac{4}{5} & 4 = \fat{Mult}{5, \fat{Div}{4, 5}} & \text{relação} & \text{fórmula} \cr \pi \not= 3 & \neg \del{\pi = 3} & \text{relação} & \text{fórmula} \cr 2 + 3 \times 4 & \fat{Soma}{2, \fat{Mult}{3,4}} & \text{função} & \text{termo} \cr \del{2 + 3} \times 4 & \fat{Mult}{\fat{Soma}{2, 3}, 4} & \text{função} & \text{termo} \cr 2 + 3 \lor 4 + 1 & & \end{array} $$