Quantificador Universal
$$\Huge \ndEQU \qquad \ndIQU $$
Intuitivamente $\forall x~\fat{Par}{x}$ é uma conjunção:
$$ \fat{Par}{0} \land \fat{Par}{1}\land \fat{Par}{2} \land \cdots $$
Analogamente, $\sum_{i} \fat{Exp}{i}$ é uma soma: $$ \fat{Exp}{0} + \fat{Exp}{1} + \fat{Exp}{2} + \cdots $$
Portanto, as regras para o quantificador universal estão relacionadas com as regras da conjunção: $\cbr{p, q} \vdash p \land q$ e $p \land q \vdash p$.
Eliminação do Quantificador Universal
Eliminação do Quantificador Universal ($\ndEQU$)
$$\Large \ndEQU: \forall x ~p\at{x} \vdash p\at{t} $$ ou $$\Large \ndrule{ \forall x ~p\at{x} }{p(t)}{\ndEQU}. $$ desde de que $t$ seja livre para $x$ em $p$.
Notas sobre a regra $\ndEQU$
- A regra $\ndEQU$ generaliza as duas regras $\ndEConjL$ e $\ndEConjR$.
- O termo $t$ tem de ser livre para $x$ em $p$.
Exemplo. Eliminação do Quantificador Universal
Para qualquer termo fechado $a$, $\forall x~p\at{x}\to q\at{x}, p\at{a} \vdash q\at{a}$.
| 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$ | $\sbr{p\at{x}\to q\at{x}}\subst{x}{a}$ e $a$ fechado |
| 4 | $q\at{a}$ | $\ndEImpl$ | 2, 3 |
- Como $a$ é fechado não ocorrem variáveis em $a$ logo este é livre para $x$ em $p\at{x} \to q\at{x}$.
- A regra $\ndEQU$ permite $\subst{x}{a}$ na linha 3.
Analogia
Se “Todos os alentejanos são portugueses” e “O João é alentejano” então “O João é português”.
Exemplo. Eliminação do Quantificador Universal
Se $x$ não ocorre em $p$ então $\forall x~p \vdash p$.
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~p$ | $H$ | |
| 2 | $p$ | $\ndEQU$ | $p\subst{x}{t}$ e $t$ fechado |
- A regra $\ndEQU$ permite escolher qualquer termo fechado, onde não ocorrem variáveis.
- Na linha 2, $p\subst{x}{t}$ é $p$ porque $x$ não ocorre em $p$
Introdução do Quantificador Universal
Introdução do Quantificador Universal ($\ndIQU$)
$$\Large \ndIQU: \sbr{\del{a} \cdots \vdash p\at{a}} \vdash \forall x~p\at{x} $$ ou $$\Large \ndrule{\ndsub{& \del{a} \cr \vdots \cr p\at{a}} }{\forall x~p\at{x}}{\ndIQU}. $$ desde que a variável $a$ não ocorra fora da sub-prova nem em hipóteses ativas.
A sub-prova e a variável $a$ são descartadas com a aplicação da regra.
Exemplo. Introdução do Quantificador Universal
Se $x$ não ocorre em $p$ então $p \vdash \forall x~p$.
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p$ | $H$ | (2) $a$ nova |
| 2 | $\forall x~p\at{x}$ | $\ndIQU$ | 1 - 1 |
O truque está em escolher uma variável “nova”, $a$. Portanto essa variável não ocorre em $p$. Além disso, também $$ p\at{x} == p == p\subst{a}{x}. $$
Analogias
- Se $\fat{Minotauro}{32}$ então também $\forall x~\fat{Minotauro}{32}$.
- Como $a$ não ocorre em $2t$, substituir $a$ por $x$ em $2t$ resulta em $2t$.
Exemplo. Aplicação incorreta de $\ndIQU$
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~x = x$ | $H$ | |
| 2 | $a = a$ | $\ndEQU$ | 1 $\del{x = x}\subst{x}{a}~(a)$ |
| 3 | $\forall y~ a = y$ | $\ndIQU$ | 2 - 2 |
| 4 | $\forall x~ \forall y~ x = y$ | $\ndIQU$ | 3 - 3 |
Nesta falsa demonstração o erro está na linha 3 porque $a$ ocorre fora da sub-prova 2 - 2.
Analogia: Ilustração intuitiva de $\ndIQU$
| Linha | Fórmula | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\forall x~2x~\text{é par.}$ | $H$ | |
| 2 | $2a~\text{é par.}$ | $\ndEQU$ | Para qualquer $a$ |
| 3 | $\forall y~ 2y~\text{é par.}$ | Definição de $\forall$ |