Lógica/Lógicas Não-clássicas/Lógica Intuicionista

Introdução

Motivações Filosóficas da Lógica Intuicionista

Discrepâncias entre a Lógica Clássica e a Intuicionista

A interpretação que a Lógica Intuicionista faz dos operadores (o que falaremos melhor abaixo) a leva a não verificar certos princípios da Lógica Clássica. Por exemplo, enquanto a Clássica interpreta $A\lor B\,\!$ como "entre $A\,\!$ e $B\,\!$ , ao menos uma é verdadeira", a Intuicionista interpreta como " $A\,\!$ é passível de prova ou $B\,\!$ é passível de prova". Portanto, o princípio de Terceiro Excluído não é verificado na Intuicionista, ou seja:

$\nvdash _{\mathbf {I} }A\lor \neg A$

Afinal, para algumas proposições pode não haver prova para a sua afirmação ou negação.

E ainda, enquanto na Lógica Clássica $\neg P\,\!$ significa que $P\,\!$ é falso, na Lógica Intuicionista significa que $P\,\!$ é refutável. Portanto, se há uma prova de $P\,\!$ , então há uma refutação de $\neg P\,\!$ . Contudo, havendo uma refutação de $\neg P\,\!$ , não necessariamente há uma prova de $P\,\!$ . Ou seja:

$\vdash _{\mathbf {I} }P\to \neg \neg P$

$\nvdash _{\mathbf {I} }\neg \neg P\to P$

Curiosamente, tanto a Lógica Clássica quanto a Intuicionista verificam $\left(P\lor \neg P\right)\to \left(\neg \neg P\to P\right)$ . O que na Clássica é um resultado óbvio, pois tanto o antecedente quanto o conseqüente são, nela, fórmulas válidas; na Intuicionista revela a relação meta-lógica de ambos princípios.

Interpretação dos símbolos lógicos

Conjunção: provar $A\land B\,\!$ é provar $A\,\!$ e provar $B\,\!$

Disjunção: provar $A\lor B\,\!$ é provar $A\,\!$ ou provar $B\,\!$

Implicação: provar $A\to B\,\!$ é aplicar um algoritmo numa prova de $A\,\!$ que leve a uma prova de $B\,\!$

Negação: provar $\neg A\,\!$ é provar que $A\to \perp \,\!$ , ou seja, que $A\,\!$ implica em uma falsidade

Quantificador Existencial: provar $\exists xPx\,\!$ é construir um objeto $x\,\!$ e provar que $Px\,\!$ é verificado

Quantificador Universal: provar $\forall xPx\,\!$ é aplicar um algoritmo em qualquer objeto $x\,\!$ , sendo que esse prove que $Px\,\!$ é verificado

Sintaxe

Axiomas

THEN-1: $\varphi \to \left(\chi \to \varphi \right)$
THEN-2: $\left(\varphi \to \left(\chi \to \psi \right)\right)\to \left(\left(\varphi \to \chi \right)\to \left(\varphi \to \psi \right)\right)$
AND-1: $\left(\varphi \land \chi \right)\to \varphi$
AND-2: $\left(\varphi \land \chi \right)\to \chi$
AND-3: $\varphi \to \left(\chi \to \left(\varphi \land \chi \right)\right)$
OR-1: $\varphi \to \left(\varphi \lor \chi \right)$
OR-2: $\chi \to \left(\varphi \lor \chi \right)$
OR-3: $\left(\varphi \to \psi \right)\to \left(\left(\chi \to \psi \right)\to \left(\left(\varphi \lor \chi \right)\to \psi \right)\right)$
NOT-1: $\left(\varphi \to \chi \right)\to \left(\left(\varphi \to \neg \chi \right)\to \neg \varphi \right)$
NOT-2: $\varphi \to \left(\neg \varphi \to \chi \right)$
PRED-1: $\left(\forall xZx\right)\to Zt$
PRED-2: $Zt\to \left(\exists xZx\right)$
PRED-3: $\forall x\left(W\to Zx\right)\to \left(W\to \forall xZx\right)$
PRED-4: $\forall x\left(Zx\to W\right)\to \left(\exists xZx\to W\right)$