Negação e Contradição

$$\Huge \ndINeg \qquad \ndIContr \qquad \ndEContr $$

A contradição ($\bot$) está relacionada com a negação ($\neg$) pois $\bot$ é definida como $q \land \neg q$.

A contratição, $\bot$, é o primeiro conectivo derivado dos quatro iniciais, $\land, \lor, \to$ e $\neg$.

Informalmente, $\bot$ pode ser lido como “falso”.

Introdução da Negação

Introdução da Negação ($\ndINeg$)

$$\Large \ndINeg: \cbr{\sbr{p \vdash q \land \neg q}} \vdash \neg p $$ ou $$ \Large \ndrule{\ndsub{p & H\cr \vdots\cr q \land \neg q} }{\neg p}{\ndINeg}. $$

Esta regra pode ser lida da seguinte forma:

Se a hipótese $p$ leva a uma contradição, $q \land \neg q$, é porque essa hipótese é “falsa”. Portanto, a sua negação, $\neg p$, tem de ser “verdadeira”.

• Esta regra tem como hipótese apenas uma sub-prova, que é descartada juntamente com a respetiva hipótese, na aplicação.
• Na conclusão da sub-prova o predicado $q$ não ocorre (necessariamente) na hipótese $p$.

Contradição

Definição (Contradição, $\bot$)

• Qualquer proposição da forma $p \land \neg p$ é uma contradição.

• Usa-se o símbolo $\bot$ para representar contradições.

Não é evidente (por enquanto) que esta definição de $\bot$ seja legítima!

• Porque é que não depende de $p$?
• O $\bot$ de $p \land \neg p$ é o mesmo de $q \land \neg q$?

Com esta definição a regra $\ndINeg$ pode ser re-escrita da seguinte forma:

Introdução da Negação ($\ndINeg$) (versão alternativa)

$$\Large \ndINeg: \cbr{\sbr{p \vdash \bot}} \vdash \neg p $$ ou $$ \Large \ndrule{ \ndsub{p & H \cr \vdots \cr \bot} }{\neg p}{\ndINeg}. $$

Numa prova pode ser usada qualquer uma das versões da regra $\ndINeg$.

Introdução da Contradição

Este novo conectivo tem as respetivas regras de dedução.

Introdução da Contradição ($\ndIContr$)

$$ \Large \ndIContr: \cbr{p, \neg p} \vdash \bot $$ ou $$ \Large \ndrule{p & \neg p}{\bot}{\ndIContr} $$

Esta regra tem duas hipóteses contraditórias $p$ e $\neg p$ e a conclusão é $\bot$.

Eliminação da Contradição

Eliminação da Contradição ($\ndEContr$)

$$ \Large \ndEContr: \bot \vdash p $$ ou $$ \Large \ndrule{\bot}{p}{\ndEContr} $$

Pode ser escolhida qualquer proposição $p$ na conclusão esta regra.