Exemplos de Derivações

Provas com Quantificadores $\forall$

Exemplo 1

Demonstrar que se $x$ não ocorre em $q$ então

$\forall x (q \land p (x)) ⊢ q \land \forall x p (x) .$

Uma prova possível é:

Linha	Fórmula	Regra
1	$\forall x (q \land p (x))$	$H$

?	$q \land \forall x p (x)$

Linha	Fórmula	Regra	Hipóteses	Observação
1	$\forall x (q \land p (x))$	$H$
2	$q \land p (a)$	$\forall^{-}$	1	$a$ variável nova portanto livre para $x$ em $q \land p (x)$ ; ${x / a}$ .

?	$q \land \forall x p (x)$

Linha	Fórmula	Regra	Hipóteses
1	$\forall x (q \land p (x))$	$H$
2	$q \land p (a)$	$\forall^{-}$	1
3	$p (a)$	$\land_{2}^{-}$	2

?	$q \land \forall x p (x)$

Linha	Fórmula	Regra	Hipóteses	Observação
1	$\forall x (q \land p (x))$	$H$
2	$q \land p (a)$	$\forall^{-}$	1 (4)	Descarte de $a$ .
3	$p (a)$	$\land_{2}^{-}$	2
4	$\forall x p (x)$	$\forall^{+}$	2 - 3

?	$q \land \forall x p (x)$

Linha	Fórmula	Regra	Hipóteses	Observação
1	$\forall x (q \land p (x))$	$H$
2	$q \land p (a)$	$\forall^{-}$	1 (4)
3	$p (a)$	$\land_{2}^{-}$	2
4	$\forall x p (x)$	$\forall^{+}$	2 - 3
5	$q \land p (b)$	$\forall^{-}$	1	$b$ nova portanto livre para $x$ em $q \land p (x)$ ; ${x / b}$ .

?	$q \land \forall x p (x)$

Linha	Fórmula	Regra	Hipóteses
1	$\forall x (q \land p (x))$	$H$
2	$q \land p (a)$	$\forall^{-}$	1 (4)
3	$p (a)$	$\land_{2}^{-}$	2
4	$\forall x p (x)$	$\forall^{+}$	2 - 3
5	$q \land p (b)$	$\forall^{-}$	1
6	$q$	$\land_{1}^{-}$	5

?	$q \land \forall x p (x)$

Linha	Fórmula	Regra	Hipóteses
1	$\forall x (q \land p (x))$	$H$
2	$q \land p (a)$	$\forall^{-}$	1 (4)
3	$p (a)$	$\land_{2}^{-}$	2
4	$\forall x p (x)$	$\forall^{+}$	2 - 3
5	$q \land p (b)$	$\forall^{-}$	1
6	$q$	$\land_{1}^{-}$	5
7	$q \land \forall x p (x)$	$\land^{+}$	6, 4

Exemplo 2

Demonstrar que se $x$ não ocorre em $q$ então

$q \land \forall x p (x) ⊢ \forall x (q \land p (x)) .$

Uma prova possível é:

Linha	Fórmula	Regra	Hipóteses	Observação
1	$q \land \forall x p (x)$	$H$
2	$q$	$\land_{1}^{-}$	1
3	$\forall x p (x)$	$\land_{2}^{-}$	1
4	$p (a)$	$\forall^{-}$	3	$a$ nova; ${x / a}$ .
5	$q \land p (a)$	$\land^{+}$	2, 4
6	$\forall x (q \land p (x))$	$\forall^{+}$	2 - 5	${a / x}$ ; $a$ não ocorre aqui.

Provas com Quantificadores $\exists$

Exemplo 3

Demonstrar que se $x$ não ocorre em $q$ então

$q \lor \exists x p (x) ⊢ \exists x (q \lor p (x)) .$

Linha	Fórmula	Regra	Hipóteses	Observação
1	$q \lor \exists x p (x)$	$H$
	Caso 1 de 1.
2	$q$	$H$	(10)
3	$q \lor p (a)$	$\lor_{1}^{+}$	2	$a$ nova.
4	$\exists x (q \lor p (x))$	$\exists^{+}$	3	$a$ livre para $x$ em $p$ ; ${a / x}$ .
	Caso 2 de 1.
5	$\exists x p (x)$	$H$	(10)
	Caso genérico de 5.
6	$p (b)$	$H$	(9)	$b$ nova logo livre para $x$ em $p$ ; ${x / b}$ .
7	$q \lor p (b)$	$\lor_{2}^{+}$	6
8	$\exists x (q \lor p (x))$	$\exists^{+}$	7	${b / x}$ ; $b$ não ocorre aqui.

9	$\exists x (q \lor p (x))$	$\exists^{-}$	5, 6 - 8	$b$ não ocorre aqui.
10	$\exists x (q \lor p (x))$	$\lor^{-}$	1, 2-4, 5-9

Exemplo 4

Demonstrar que se $x$ não ocorre em $q$ então

$\exists x (q \lor p (x)) ⊢ q \lor \exists x p (x) .$

Linha	Fórmula	Regra	Hipóteses	Observação
1	$\exists x (q \lor p (x))$	$H$
2	$q \lor p (a)$	$\exists^{-}$	1	$a$ nova; ${x / a}$ ; descarte $a$ : (9)
3	$q$	$H$	(8)	Caso 1 de 2.
4	$q \lor \exists x p (x)$	$\lor_{1}^{+}$	3	$a$ não ocorre aqui.
5	$p (a)$	$H$	(8)	Caso 2 de 2.
				$a$ livre para $x$ em $p$ ;
6	$\exists x p (x)$	$\exists^{+}$	5	${a / x}$ ; $a$ não ocorre aqui.
7	$q \lor \exists x p (x)$	$\lor_{2}^{+}$	6
8	$q \lor \exists x p (x)$	$\lor^{-}$	2, 3 - 4, 5 - 7
9	$q \lor \exists x p (x)$	$\exists^{-}$	1, 2 - 8

Provas com Igualdade

Exemplo 5

Se $t$ é um termo fechado, $⊢ \exists x x = t$ .

Linha	Fórmula	Regra	Hipóteses	Observação
1	$t = t$	$=^{+}$		$t$ é fechado
2	$\exists x x = t$	$\exists^{+}$	1	${t / x}$ parcial.

Na linha 1, o termo $t$ é fechado, isto é, não tem variáveis. Além disso: seja $p (t)$ a fórmula $t = t$ . O termo $t$ é livre para $x$ em $p (t)$ e $x$ não ocorre em $p (t)$ . Estas são as condições para a regra $\exists^{+}$ .
A linha 2 resulta de substituir parcialmente $t$ por $x$ , de $t = t$ em $x = t$ .

Além disso, nesta prova não surgem hipóteses. A primeira linha resulta da regra $=^{+}$ , que não tem hipóteses.

Exemplo 6

Demonstrar que $⊢ \forall x \forall y x = y \to y = x$ (simetria).

Linha	Fórmula	Regra	Hipóteses	Observação
1	$a = b$	$H$		$a, b$ novas; ( $H$ :4 $b$ :5 $a$ :6)
				Seja $p$ a fórmula $x = a$ .
2	$a = a$	$=^{+}$		$p {x / a}$
3	$b = a$	$=^{-}$	2, 1	$p {x / b}$
4	$a = b \to b = a$	$\to^{+}$		$a, b$ não descartadas.
5	$\forall y a = y \to y = a$	$\forall^{+}$	4 ${b / y}$	$y$ não ocorre em 4; $b$ descartada.
6	$\forall x \forall y x = y \to y = x$	$\forall^{+}$	5 ${a / x}$	$x$ não ocorre em 5; $a$ descartada.

Vejamos, na linha 3, a aplicação da regra (usando $a, b$ em vez de $t_{1}, t_{2}$ ) $\frac{a = b p { x / a }}{p { x / b }} (=^{-})$ desde que $a, b$ sejam livres para $x$ em $p$

A fórmula $p$ usada nesta prova é $x = a$ . Porquê?

A substituição $p {x / b}$ , na linha 3, tem de ser $b = a$ para ficar $a = b \to b = a$ na linha 4.
Portanto, escolhe-se $p$ fazendo a substituição "inversa" na fórmula "alvo": $A substitui \overset{c}{¸} \overset{a}{˜} o [b = a] {b / x} resulta na f \overset{o}{ˊ} rmula x = a .$
Agora $p {x / a}$ é $a = a$ que resulta da regra $=^{+}$ na linha 2.

Portanto, fazendo $p$ a fórmula $x = a$ :

A hipótese $a = b$ na linha 1 é a hipótese $a = b$ da regra $=^{-}$ .
Na linha 2 fica $a = a$ que é $p {x / a}$ , a segunda hipótese da regra $=^{-}$ .
Na linha 3 fica $b = a$ que é $p {x / b}$ , a conclusão da regra $=^{-}$ com hipóteses em 1 e 2.

Lógica e Computação

Exemplos de Derivações

Provas com Quantificadores ∀

Provas com Quantificadores ∃

Provas com Igualdade

Provas com Quantificadores $\forall$

Provas com Quantificadores $\exists$