Quantificador Existencial
$$\Huge \ndEQE \qquad \ndIQE $$
Intuitivamente $\exists x~\fat{Sus}{x}$ é uma disjunção:
$$ \fat{Sus}{\lit{Red}} \lor \fat{Sus}{\lit{Blue}} \lor \fat{Sus}{\lit{Green}} \lor \cdots. $$
Portanto, as regras para o quantificador existencial estão relacionadas com as regras da disjunção: $$ p \vdash p \lor q $$ e $$ \cbr{p \lor q, \sbr{p \vdash r}, \sbr{q \vdash r} } \vdash r. $$
Eliminação do Quantificador Existencial
Eliminação do Quantificador Existencial ($\ndEQE$)
$$\Large \ndEQE: \cbr{\exists x~p\at{x}, \sbr{p\at{a} \vdash q}} \vdash q $$ ou $$\Large \ndrule{ \exists x~p\at{x} & \ndsub{p\at{a}\quad H\cr \vdots \cr q} }{q}{\ndEQE}. $$ desde que $a$ não ocorra fora da sub-prova. Em particular, $a$ não pode ocorrer em $q$.
A sub-prova e a variável $a$ são descartadas com a aplicação da regra.
Exemplo. Aplicação incorreta de $\ndEQE$
Mais à frente é desenvolvido um exemplo de aplicação correta desta regra. O caso seguinte é uma aplicação incorreta.
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\exists x~p\at{x}$ | $H$ | |
| 2 | $p\at{a}$ | $H$ | $(a)~p\subst{x}{a}$ |
| 3 | $p\at{a}$ | $\ndEQE$ | 1, 2 - 2 |
| 4 | $\forall x~p\at{x}$ | $\ndIQU$ | 2 - 3 |
O erro está na linha 3 porque $a$ ocorre fora da sub-prova $2-2$.
Introdução do Quantificador Existencial
Introdução do Quantificador Existencial ($\ndIQE$)
$$\Large \ndIQE: p\at{t} \vdash \exists x~p\subst{t}{x} $$ ou $$\Large \ndrule{ p\at{t} }{\exists x~p\subst{t}{x}}{\ndIQE}. $$ desde que $t$ seja livre para $x$ em $p$ e $x$ não ocorra em $p\at{t}$.
Excecionalmente nesta regra, de $p\at{t}$ para $p\subst{t}{x}$ podem ser substituídas apenas algumas ocorrências de $t$ por $x$, não obrigatoriamente todas.
Exemplo. Substituição parcial
Nem todas as ocorrências do termo $4$ são substituidas por $x$ em $$ \ndrule{2 + 4 > 1 + 4}{\exists x~2 + x > 1 + 4}{\ndIQE} $$
Exemplo. Ilustração intuitiva da regra $\ndIQE$
| Linha | Fórmula | Justificação |
|---|---|---|
| 1 | $\exists x~x+2=6$ | $H$ |
| 2 | $a+2=6$ | Seja $a$ um dos $x$ acima. |
| 3 | $\exists y~ y+2=6$ | Definição de $\exists$ |
Exemplo. Aplicação intuitiva das regras $\ndEQU, \ndEQE, \ndIQU$ e $\ndIQE$
| Linha | Fórmula | Justificação | Linha | Fórmula | Justificação | |
|---|---|---|---|---|---|---|
| 1 | $\exists x~x+2=6$ | Hipótese | 1 | $\forall x~2x~\text{é par.}$ | Hipótese | |
| 2 | $a+2=6$ | Seja $a$ como acima | 2 | $2a~\text{é par.}$ | Para qualquer $a$. | |
| 3 | $\exists y~ y+2=6$ | Definição de $\exists$ | 3 | $\forall y~ 2y~\text{é par.}$ | Definição de $\forall$ |
Exemplo. Introdução de $\exists$
Para qualquer termo fechado $a$, $$ \forall x~ p\at{x} \to q\at{x}, p\at{a} \vdash \exists x~ q\at{x} $$
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~p\at{x}\to q\at{x}$ | $H$ | |
| 2 | $p\at{a}$ | $H$ | |
| 3 | $p\at{a}\to q\at{a}$ | $\ndEQU$ | 1 $\sbr{p\at{x}\to q\at{x}}\subst{x}{a}$ |
| 4 | $q\at{a}$ | $\ndEImpl$ | 2, 3 |
| 5 | $\exists x~ q\at{x}$ | $\ndIQE$ | $a$ fechado |
Na linha 4 a variável $x$ não ocorre em $q\at{a}$ porque esta resulta de $\subst{x}{a}$ e $x$ não ocorre em $a$. Portanto a ocorrência de $x$ na linha 5 está correta.