Lógica/Lógicas Não-clássicas/Lógica 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 ${\displaystyle A\lor B\,\!}$ como "entre ${\displaystyle A\,\!}$ e ${\displaystyle B\,\!}$, ao menos uma é verdadeira", a Intuicionista interpreta como "${\displaystyle A\,\!}$ é passível de prova ou ${\displaystyle B\,\!}$ é passível de prova". Portanto, o princípio de Terceiro Excluído não é verificado na Intuicionista, ou seja:

${\displaystyle \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 ${\displaystyle \neg P\,\!}$ significa que ${\displaystyle P\,\!}$ é falso, na Lógica Intuicionista significa que ${\displaystyle P\,\!}$ é refutável. Portanto, se há uma prova de ${\displaystyle P\,\!}$, então há uma refutação de ${\displaystyle \neg P\,\!}$. Contudo, havendo uma refutação de ${\displaystyle \neg P\,\!}$, não necessariamente há uma prova de ${\displaystyle P\,\!}$. Ou seja:

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

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

Curiosamente, tanto a Lógica Clássica quanto a Intuicionista verificam ${\displaystyle \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.

• Conjunção: provar ${\displaystyle A\land B\,\!}$ é provar ${\displaystyle A\,\!}$ e provar ${\displaystyle B\,\!}$

• Disjunção: provar ${\displaystyle A\lor B\,\!}$ é provar ${\displaystyle A\,\!}$ ou provar ${\displaystyle B\,\!}$

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

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

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

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

• THEN-1: ${\displaystyle \varphi \to \left(\chi \to \varphi \right)}$
• THEN-2: ${\displaystyle \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: ${\displaystyle \left(\varphi \land \chi \right)\to \varphi }$
• AND-2: ${\displaystyle \left(\varphi \land \chi \right)\to \chi }$
• AND-3: ${\displaystyle \varphi \to \left(\chi \to \left(\varphi \land \chi \right)\right)}$
• OR-1: ${\displaystyle \varphi \to \left(\varphi \lor \chi \right)}$
• OR-2: ${\displaystyle \chi \to \left(\varphi \lor \chi \right)}$
• OR-3: ${\displaystyle \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: ${\displaystyle \left(\varphi \to \chi \right)\to \left(\left(\varphi \to \neg \chi \right)\to \neg \varphi \right)}$
• NOT-2: ${\displaystyle \varphi \to \left(\neg \varphi \to \chi \right)}$
• PRED-1: ${\displaystyle \left(\forall xZx\right)\to Zt}$
• PRED-2: ${\displaystyle Zt\to \left(\exists xZx\right)}$
• PRED-3: ${\displaystyle \forall x\left(W\to Zx\right)\to \left(W\to \forall xZx\right)}$
• PRED-4: ${\displaystyle \forall x\left(Zx\to W\right)\to \left(\exists xZx\to W\right)}$

Esta página é um esboço de matemática. Ampliando-a você ajudará a melhorar o Wikilivros.

Esta página é um esboço de Filosofia. Ampliando-a você ajudará a melhorar o Wikilivros.