Inferência na lógica de predicados

Para provar argumentos na lógica de predicados utilizamos as mesmas técnicas dedutivas da lógica proposicional, nos baseando nas regras de inferência e leis de equivalência. Devemos levar em conta também as relações de consequência e equivalência específicas à lógica de predicados.
Além das regras já citadas, é necessário introduzir novas regras para lidar especificamente com os quantificadores presentes na lógica de predicados.

Eliminação (particularização ou instanciação)

A eliminação consiste em, a partir de uma fórmula quantificada, remover o quantificador instanciando (particularizando) a variável que está sendo quantificada.

Eliminação universal

$$\forall Xp(X)\therefore p(c)$$

Eliminação existencial

$$\exists Xp(X)\therefore p(c)$$

Introdução (generalização)

A introdução consiste em, a partir de uma fórmula não quantificada, introduzir um quantificador generalizando o predicado.

Introdução universal

$$p(c)\therefore \forall Xp(X)$$

Introdução existencial

$$p(c)\therefore \exists Xp(X)$$