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

Origem: Wikilivros, livros abertos por um mundo aberto.

Índice

1 Introdução
- 1.1 Motivações Filosóficas da Lógica Intuicionista
- 1.2 Discrepâncias entre a Lógica Clássica e a Intuicionista
2 Interpretação dos símbolos lógicos
3 Sintaxe
- 3.1 Axiomas
4 Semântica
- 4.1 Álgebra de Heyting
- 4.2 Semântica de Kripke

[editar] Introdução

[editar] Motivações Filosóficas da Lógica Intuicionista

[editar] 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.

[editar] 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 x Px\,\!$ é construir um objeto $x\,\!$ e provar que $Px\,\!$ é verificado

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

[editar] Sintaxe

[editar] 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 x Zx\right)\to Zt$
PRED-2: $Zt\to\left(\exists x Zx\right)$
PRED-3: $\forall x \left( W\to Zx\right)\to \left(W \to \forall x Zx\right)$
PRED-4: $\forall x \left( Zx \to W\right)\to \left(\exists x Zx \to W\right)$