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

Introdução

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\vee 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:

${⊬}_{𝐈}A\vee \mathrm{\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 $\mathrm{\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 $\mathrm{\neg }P$. Contudo, havendo uma refutação de $\mathrm{\neg }P$, não necessariamente há uma prova de $P$. Ou seja:

${⊢}_{𝐈}P\to \mathrm{\neg }\mathrm{\neg }P$

${⊬}_{𝐈}\mathrm{\neg }\mathrm{\neg }P\to P$

Curiosamente, tanto a Lógica Clássica quanto a Intuicionista verificam $(P\vee \mathrm{\neg }P)\to (\mathrm{\neg }\mathrm{\neg }P\to P)$. 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\wedge B$ é provar $A$ e provar $B$

• Disjunção: provar $A\vee 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 $\mathrm{\neg }A$ é provar que $A\to \perp$, ou seja, que $A$ implica em uma falsidade

• Quantificador Existencial: provar $\mathrm{\exists }xPx$ é construir um objeto $x$ e provar que $Px$ é verificado

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

Sintaxe

Axiomas

• THEN-1: $\phi \to (\chi \to \phi )$
• THEN-2: $(\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))$
• AND-1: $(\phi \wedge \chi )\to \phi$
• AND-2: $(\phi \wedge \chi )\to \chi$
• AND-3: $\phi \to (\chi \to (\phi \wedge \chi ))$
• OR-1: $\phi \to (\phi \vee \chi )$
• OR-2: $\chi \to (\phi \vee \chi )$
• OR-3: $(\phi \to \psi )\to ((\chi \to \psi )\to ((\phi \vee \chi )\to \psi ))$
• NOT-1: $(\phi \to \chi )\to ((\phi \to \mathrm{\neg }\chi )\to \mathrm{\neg }\phi )$
• NOT-2: $\phi \to (\mathrm{\neg }\phi \to \chi )$
• PRED-1: $\left(\mathrm{\forall }xZx\right)\to Zt$
• PRED-2: $Zt\to \left(\mathrm{\exists }xZx\right)$
• PRED-3: $\mathrm{\forall }x(W\to Zx)\to (W\to \mathrm{\forall }xZx)$
• PRED-4: $\mathrm{\forall }x(Zx\to W)\to (\mathrm{\exists }xZx\to W)$