Provas em lógica de primeira ordem

Igualdade

As regras proposicionais continuam a valer. A esta camada juntam-se a igualdade e os quantificadores.

• A regra $=I$ dá $t=t$ para qualquer termo.
• A regra $=E$ substitui iguais por iguais sem captura. De $a=b$ e $P(a)$ obténs $P(b)$.
• De $a=b$ obténs $f(a)=f(b)$. A inversa exige que $f$ seja injetiva.

Quantificadores

Regra	Operação	Condição guardada
$\forall E$	de $\forall x\varphi$ obtém $\varphi[x\mapsto t]$	$t$ está livre para $x$
$\exists I$	de $\varphi[x\mapsto t]$ obtém $\exists x\varphi$	a substituição é admissível
$\forall I$	prova $\varphi(u)$ e generaliza	$u$ é nova e arbitrária, sem dependência especial
$\exists E$	abre $\varphi(u)$, deduz $\theta$ e fecha a caixa	$u$ fica fora da conclusão e das hipóteses exteriores

• Instancia a fórmula inteira: de $\forall x(P(x)\to Q(x))$ obténs $P(t)\to Q(t)$, não $Q(t)$ sozinho.
• Para $\exists x(P(x)\land Q(x))$, ambas as propriedades têm de valer para a mesma testemunha. $P(a)$ com $Q(b)$ não chegam sem $a=b$.

A testemunha de $\exists xP(x)$ tem uma propriedade especial; por isso não serve como objeto arbitrário para provar $\forall xP(x)$.

1  ∀x(P(x) → Q(x))      premissa
2  ∃xP(x)               premissa
3  | u, P(u)            testemunha nova e hipótese
4  | P(u) → Q(u)        ∀E, 1
5  | Q(u)               →E, 4, 3
6  | ∃xQ(x)             ∃I, 5
7  ∃xQ(x)               ∃E, 2, 3 a 6

A linha 6 remove a referência à testemunha antes de sair da caixa. A fórmula $Q(u)$ não poderia sair diretamente. De um $P(a)$ particular não concluis $\forall xP(x)$.

Rever uma prova

$\neg\forall xP(x)\Leftrightarrow\exists x\neg P(x)$ vale semanticamente. Numa dedução com as regras de base, justifica cada direção. Para obter $\neg\forall xP(x)$ a partir de uma testemunha de $\neg P$, assume o universal, instancia-o nessa testemunha e deriva $F$.

Confere uma dedução em Fitch:

1. Todas as linhas citadas estão acessíveis na caixa atual.
2. $\forall E$ e $\exists I$ aplicam-se só a ocorrências livres, sem captura.
3. $\forall I$ exige um objeto arbitrário, sem hipóteses especiais abertas.
4. $\exists E$ cita a existência e a caixa inteira; a testemunha fica fora da conclusão.
5. As caixas fecham por ordem e a fórmula final só tem dependências permitidas.

A dedução natural de primeira ordem é correta e completa: $\Gamma\vdash\varphi$ se e só se $\Gamma\models\varphi$. Testar uma estrutura finita não prova a consequência em todas as estruturas.

Provas quantificadas com caixas encaixadas.