Exemplos de Derivações
Provas com Quantificadores $\forall$
Exemplo 1
Demonstrar que se $x$ não ocorre em $q$ então
$$ \forall x~\del{q \land p\at{x}} \vdash q \land \forall x~p\at{x}. $$
Uma prova possível é:
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | |
| ? | $q \land \forall x~p\at{x}$ |
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | ||
| 2 | $\qquad q \land p\at{a}$ | $\ndEQU$ | 1 | $a$ variável nova portanto livre para $x$ em $q \land p\at{x}$; $\subst{x}{a}$. |
| ? | $q \land \forall x~p\at{x}$ |
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | |
| 2 | $\qquad q \land p\at{a}$ | $\ndEQU$ | 1 |
| 3 | $\qquad p\at{a}$ | $\ndEConjR$ | 2 |
| ? | $q \land \forall x~p\at{x}$ |
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | ||
| 2 | $\qquad q \land p\at{a}$ | $\ndEQU$ | 1 (4) | Descarte de $a$. |
| 3 | $\qquad p\at{a}$ | $\ndEConjR$ | 2 | |
| 4 | $\forall x~p\at{x}$ | $\ndIQU$ | 2 - 3 | |
| ? | $q \land \forall x~p\at{x}$ |
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | ||
| 2 | $\qquad q \land p\at{a}$ | $\ndEQU$ | 1 (4) | |
| 3 | $\qquad p\at{a}$ | $\ndEConjR$ | 2 | |
| 4 | $\forall x~p\at{x}$ | $\ndIQU$ | 2 - 3 | |
| 5 | $q \land p\at{b}$ | $\ndEQU$ | 1 | $b$ nova portanto livre para $x$ em $q \land p\at{x}$; $\subst{x}{b}$. |
| ? | $q \land \forall x~p\at{x}$ |
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | |
| 2 | $\qquad q \land p\at{a}$ | $\ndEQU$ | 1 (4) |
| 3 | $\qquad p\at{a}$ | $\ndEConjR$ | 2 |
| 4 | $\forall x~p\at{x}$ | $\ndIQU$ | 2 - 3 |
| 5 | $q \land p\at{b}$ | $\ndEQU$ | 1 |
| 6 | $q$ | $\ndEConjL$ | 5 |
| ? | $q \land \forall x~p\at{x}$ |
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~\del{q \land p\at{x}}$ | $H$ | |
| 2 | $\qquad q \land p\at{a}$ | $\ndEQU$ | 1 (4) |
| 3 | $\qquad p\at{a}$ | $\ndEConjR$ | 2 |
| 4 | $\forall x~p\at{x}$ | $\ndIQU$ | 2 - 3 |
| 5 | $q \land p\at{b}$ | $\ndEQU$ | 1 |
| 6 | $q$ | $\ndEConjL$ | 5 |
| 7 | $q \land \forall x~p\at{x}$ | $\ndIConj$ | 6, 4 |
Exemplo 2
Demonstrar que se $x$ não ocorre em $q$ então
$$ q \land \forall x~p\at{x} \vdash \forall x\del{q \land p\at{x}}. $$
Uma prova possível é:
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $q \land \forall x~p\at{x}$ | $H$ | ||
| 2 | $q$ | $\ndEConjL$ | 1 | |
| 3 | $\forall x~p\at{x}$ | $\ndEConjR$ | 1 | |
| 4 | $\quad p\at{a}$ | $\ndEQU$ | 3 | $a$ nova; $\subst{x}{a}$. |
| 5 | $\quad q \land p\at{a}$ | $\ndIConj$ | 2, 4 | |
| 6 | $\forall x~\del{q \land p\at{x}}$ | $\ndIQU$ | 2 - 5 | $\subst{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\at{x} \vdash \exists x\del{q \lor p\at{x}}. $$
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $q \lor \exists x~p\at{x}$ | $H$ | ||
| Caso 1 de 1. | ||||
| 2 | $\quad q$ | $H$ | (10) | |
| 3 | $\quad q \lor p\at{a}$ | $\ndIDisjL$ | 2 | $a$ nova. |
| 4 | $\quad \exists x~\del{q \lor p\at{x}}$ | $\ndIQE$ | 3 | $a$ livre para $x$ em $p$; $\subst{a}{x}$. |
| Caso 2 de 1. | ||||
| 5 | $\quad \exists x~p\at{x}$ | $H$ | (10) | |
| Caso genérico de 5. | ||||
| 6 | $\qquad p\at{b}$ | $H$ | (9) | $b$ nova logo livre para $x$ em $p$; $\subst{x}{b}$. |
| 7 | $\qquad q \lor p\at{b}$ | $\ndIDisjR$ | 6 | |
| 8 | $\qquad \exists x~\del{q \lor p\at{x}} $ | $\ndIQE$ | 7 | $\subst{b}{x}$; $b$ não ocorre aqui. |
| 9 | $\quad \exists x~\del{q \lor p\at{x}}$ | $\ndEQE$ | 5, 6 - 8 | $b$ não ocorre aqui. |
| 10 | $\exists x\del{q \lor p\at{x}}$ | $\ndEDisj$ | 1, 2-4, 5-9 |
Exemplo 4
Demonstrar que se $x$ não ocorre em $q$ então
$$ \exists x~\del{q \lor p\at{x}} \vdash q \lor \exists x~p\at{x}. $$
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $\exists x~\del{q \lor p\at{x}}$ | $H$ | ||
| 2 | $\quad q \lor p\at{a}$ | $\ndEQE$ | 1 | $a$ nova; $\subst{x}{a}$; descarte $a$: (9) |
| 3 | $\qquad q$ | $H$ | (8) | Caso 1 de 2. |
| 4 | $\qquad q \lor \exists x~p\at{x}$ | $\ndIDisjL$ | 3 | $a$ não ocorre aqui. |
| 5 | $\qquad p\at{a}$ | $H$ | (8) | Caso 2 de 2. |
| $a$ livre para $x$ em $p$; | ||||
| 6 | $\qquad \exists x~p\at{x}$ | $\ndIQE$ | 5 | $\subst{a}{x}$; $a$ não ocorre aqui. |
| 7 | $\qquad q \lor \exists x~p\at{x}$ | $\ndIDisjR$ | 6 | |
| 8 | $\quad q \lor \exists x~p\at{x}$ | $\ndEDisj$ | 2, 3 - 4, 5 - 7 | |
| 9 | $q \lor \exists x~p\at{x}$ | $\ndEQE$ | 1, 2 - 8 |
Provas com Igualdade
Exemplo 5
Se $t$ é um termo fechado, $\vdash \exists x~x = t$.
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $t = t$ | $\ndIEqual$ | $t$ é fechado | |
| 2 | $\exists x~x = t$ | $\ndIQE$ | 1 | $\subst{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 $\ndIQE$.
- 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 $\ndIEqual$, que não tem hipóteses.
Exemplo 6
Demonstrar que $\vdash \forall x\forall y~x = y \to y = x$ (simetria).
| Linha | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|
| 1 | $\quad\quad \quad a = b$ | $H$ | $a,b$ novas; ($H$:4 $b$:5 $a$:6) | |
| Seja $p$ a fórmula $x = a$. | ||||
| 2 | $\quad\quad \quad a = a$ | $\ndIEqual$ | $p\subst{x}{a}$ | |
| 3 | $\quad\quad \quad b = a$ | $\ndEEqual$ | 2, 1 | $p\subst{x}{b}$ |
| 4 | $\quad\quad a = b \to b = a$ | $\ndIImpl$ | $a, b$ não descartadas. | |
| 5 | $\quad \forall y~a = y \to y = a$ | $\ndIQU$ | 4 $\subst{b}{y}$ | $y$ não ocorre em 4; $b$ descartada. |
| 6 | $\forall x \forall y~x = y \to y = x$ | $\ndIQU$ | 5 $\subst{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$) $$ \ndrule{a = b & p\subst{x}{a}}{p\subst{x}{b}}{\ndEEqual} $$ desde que $a, b$ sejam livres para $x$ em $p$
A fórmula $p$ usada nesta prova é $\alert{x = a}$. Porquê?
- A substituição $p\subst{x}{b}$, na linha 3, tem de ser $\alert{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”: $$ \text{A substituição}~\sbr{b = a}\subst{b}{x}~\text{resulta na fórmula}~ x = a. $$
- Agora $p\subst{x}{a}$ é $\alert{a = a}$ que resulta da regra $\ndIEqual$ 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 $\ndEEqual$.
- Na linha 2 fica $a = a$ que é $p\subst{x}{a}$, a segunda hipótese da regra $\ndEEqual$.
- Na linha 3 fica $b = a$ que é $p\subst{x}{b}$, a conclusão da regra $\ndEEqual$ com hipóteses em 1 e 2.