Quantificador Existencial

$${\exists }^{-}{\exists }^{+}$$

Intuitivamente $\exists x\text{Sus}\left(x\right)$ é uma disjunção:

$$\text{Sus}\left(\text{Red}\right)\vee \text{Sus}\left(\text{Blue}\right)\vee \text{Sus}\left(\text{Green}\right)\vee \cdots .$$

Portanto, as regras para o quantificador existencial estão relacionadas com as regras da disjunção: $p⊢p\vee q$ e $\left\{p\vee q,\left[p⊢r\right],\left[q⊢r\right]\right\}⊢r$.

Eliminação do Quantificador Existencial

Eliminação do Quantificador Existencial (${\exists }^{-}$)

$${\exists }^{-}:\left\{\exists xp\left(x\right),\left[p\left(a\right)⊢q\right]\right\}⊢q$$ ou $$\frac{\begin{array}{cc}\exists xp\left(x\right)& \boxed{\begin{array}{c}p\left(a\right)H\\ ⋮\\ q\end{array}}\end{array}}{q}\left({\exists }^{-}\right).$$ 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 ${\exists }^{-}$

Mais à frente é desenvolvido um exemplo de aplicação correta desta regra. O caso seguinte é uma aplicação incorreta.

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 (${\exists }^{+}$)

$${\exists }^{+}:p\left(t\right)⊢\exists xp\left\{t/x\right\}$$ ou $$\frac{\begin{array}{c}p\left(t\right)\end{array}}{\exists xp\left\{t/x\right\}}\left({\exists }^{+}\right).$$ desde que $t$ seja livre para $x$ em $p$ e $x$ não ocorra em $p\left(t\right)$.

Excecionalmente nesta regra, de $p\left(t\right)$ para $p\left\{t/x\right\}$ 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 $$\frac{\begin{array}{c}2+4>1+4\end{array}}{\exists x2+x>1+4}\left({\exists }^{+}\right)$$

Exemplo. Ilustração intuitiva da regra ${\exists }^{+}$

Exemplo. Aplicação intuitiva das regras ${\forall }^{-},{\exists }^{-},{\forall }^{+}$ e ${\exists }^{+}$

Exemplo. Introdução de $\exists$

Para qualquer termo fechado $a$, $$\forall xp\left(x\right)\to q\left(x\right),p\left(a\right)⊢\exists xq\left(x\right)$$

Na linha 4 a variável $x$ não ocorre em $q\left(a\right)$ porque esta resulta de $\left\{x/a\right\}$ e $x$ não ocorre em $a$. Portanto a ocorrência de $x$ na linha 5 está correta.