Negação e Contradição

$${\neg }^{+}{\perp }^{+}{\perp }^{-}$$

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

A contratição, $\perp$, é o primeiro conectivo derivado dos quatro iniciais, $\wedge ,\vee ,\to$ e $\neg$.

Informalmente, $\perp$ pode ser lido como "falso".

Introdução da Negação

Introdução da Negação (${\neg }^{+}$)

$${\neg }^{+}:\left\{\left[p⊢q\wedge \neg q\right]\right\}⊢\neg p$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}p& H\\ ⋮& \\ q\wedge \neg q& \end{array}}\end{array}}{\neg p}\left({\neg }^{+}\right).$$

Esta regra pode ser lida da seguinte forma:

Se a hipótese $p$ leva a uma contradição, $q\wedge \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, $\perp$)

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

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

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

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

Com esta definição a regra ${\neg }^{+}$ pode ser re-escrita da seguinte forma:

Introdução da Negação (${\neg }^{+}$) (versão alternativa)

$${\neg }^{+}:\left\{\left[p⊢\perp \right]\right\}⊢\neg p$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}p& H\\ ⋮& \\ \perp & \end{array}}\end{array}}{\neg p}\left({\neg }^{+}\right).$$

Numa prova pode ser usada qualquer uma das versões da regra ${\neg }^{+}$.

Introdução da Contradição

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

Introdução da Contradição (${\perp }^{+}$)

$${\perp }^{+}:\left\{p,\neg p\right\}⊢\perp$$ ou $$\frac{\begin{array}{cc}p& \neg p\end{array}}{\perp }\left({\perp }^{+}\right)$$

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

Eliminação da Contradição

Eliminação da Contradição (${\perp }^{-}$)

$${\perp }^{-}:\perp ⊢p$$ ou $$\frac{\begin{array}{c}\perp \end{array}}{p}\left({\perp }^{-}\right)$$

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