Lógica intuicionista

Lógica intuicionista, ou lógica construtivista, é o sistema de lógica simbólica desenvolvido por Arend Heyting para prover uma base formal para o intuicionismo de Brouwer. O sistema preserva, também, a justificação, e não apenas a verdade, no processo que leva de hipóteses a proposições derivadas - se as hipóteses são verdadeiras e justificáveis então a conclusão também será verdadeira e justificável. De um ponto de vista prático, há, também, uma forte motivação para usar a lógica intuicionista, já que ela possui a propriedade existencial, tornando-a adequada para outras formas de construtivismo matemático.

Sintaxe

A sintaxe das fórmulas da lógica intuicionista é similar à da lógica proposicional ou da lógica de primeira ordem. No entanto, os conectivos intuicionistas não são interdefiníveis da mesma maneira que na lógica clássica - sendo assim, a escolha de conectivos básicos faz diferença. Na lógica proposicional intuicionista é usual utilizar $\,\rightarrow$ , $\,\land$ , $\,\lor$ , $\,\bot$ como conectivos básicos, tratando $\,\neg$ como a abreviatura $\neg \alpha =(\alpha \rightarrow \bot )$ . Na lógica intuicionista de primeira ordem, ambos os quantificadores $\,\exists$ , $\,\forall$ são necessários.

Muitas tautologias da lógica clássica não podem ser demonstradas pela lógica intuicionista. Alguns dos exemplos são a lei do terceiro excluído $\alpha \lor \neg \alpha$ , também a lei de Peirce $((\alpha \rightarrow \beta )\rightarrow \alpha )\rightarrow \alpha$ e, até mesmo, a eliminação da dupla negação. Na lógica clássica ambos $\alpha \rightarrow \neg \neg \alpha$ e $\neg \neg \alpha \rightarrow \alpha$ são teoremas, mas na lógica intuicionista apenas a primeira é um teorema: a dupla negação pode ser introduzida, mas não pode ser eliminada.

A observação de que muitas tautologias válidas classicamente não são teoremas da lógica intuicionista leva à ideia de enfraquecimento na teoria de demonstrações da lógica clássica.

Cálculo à la Hilbert

A lógica intuicionista pode ser definida utilizando o seguinte sistema dedutivo à la Hilbert.

Na lógica proposicional a regra de inferência é modus ponens

MP: de $\,\phi$ e $\phi \rightarrow \psi$ deriva-se $\,\psi$

e os axiomas são

ENTÃO-1: $\phi \rightarrow (\psi \rightarrow \phi )$
ENTÃO-2: $(\phi \rightarrow (\psi \rightarrow \gamma ))\rightarrow ((\phi \rightarrow \psi )\rightarrow (\phi \rightarrow \gamma ))$
E-1: $\phi \land \psi \rightarrow \phi$
E-2: $\phi \land \psi \rightarrow \psi$
E-3: $\phi \rightarrow (\psi \rightarrow (\phi \land \psi ))$
OU-1: $\phi \rightarrow \phi \lor \psi$
OU-2: $\psi \rightarrow \phi \lor \psi$
OU-3: $(\phi \rightarrow \psi )\rightarrow ((\gamma \rightarrow \psi )\rightarrow (\phi \lor \gamma \rightarrow \psi ))$
ABSURDO: $\bot \rightarrow \phi$

Para fazer disto um sistema de primeira ordem, adicionamos as regras de generalização

GEN-∀: de $\phi \rightarrow \psi$ deriva-se $\phi \rightarrow (\forall x\psi )$ , se x não for variável livre em $\,\phi$
GEN-∃: de $\phi \rightarrow \psi$ deriva-se $(\exists x\phi )\rightarrow \psi$ , se x não for variável livre em $\,\psi$

e os seguintes axiomas

PRED-1: $(\forall x\phi (x))\rightarrow \phi (t)$ , se t é um termo livre pra x em $\,\phi$ , isto é, se as variáveis do termo t não se tornam quantificadas ao substituirmos x por t.
PRED-2: $\phi (t)\rightarrow (\exists x\phi (x))$ , com as mesmas restrições acima

Conectivos opcionais

Negação

Para incluir o conectivo $\,\neg$ para negação, no lugar de utilizá-la como abreviatura para $\phi \rightarrow \bot$ , é suficiente adicionar os axiomas

NÃO-1′: $(\phi \rightarrow \bot )\rightarrow \neg \phi$
NÃO-2′: $\neg \phi \rightarrow (\phi \rightarrow \bot )$

Há um grande número de alternativas para omitir o conectivo $\,\bot$ (absurdo). Por exemplo, pode-se substituir os axiomas ABSURDO, NÃO-1′, e NÃO-2′ por

NÃO-1: $(\phi \rightarrow \psi )\rightarrow ((\phi \rightarrow \neg \psi )\rightarrow \neg \phi )$
NÃO-2: $\phi \rightarrow (\neg \phi \rightarrow \psi )$

alternativas para o NÃO-1 são $(\phi \rightarrow \neg \psi )\rightarrow (\psi \rightarrow \neg \phi )$ ou $(\phi \rightarrow \neg \phi )\rightarrow \neg \phi$ .

Equivalência

O conectivo $\,\leftrightarrow$ (bi-implicação) para equivalência pode ser tratado como abreviatura, com $\phi \leftrightarrow \psi$ significando $(\phi \rightarrow \psi )\land (\psi \rightarrow \phi )$ . Como alternativa, pode-se adicionar os axiomas

SSE-1: $(\phi \leftrightarrow \psi )\rightarrow (\phi \rightarrow \psi )$
SSE-2: $(\phi \leftrightarrow \psi )\rightarrow (\psi \rightarrow \phi )$
SSE-3: $(\phi \rightarrow \psi )\rightarrow ((\psi \rightarrow \phi )\rightarrow (\phi \leftrightarrow \psi ))$

SSE-1 e SSE-2 podem ser combinados, utilizando a conjunção, em um só axioma $(\phi \leftrightarrow \psi )\rightarrow ((\phi \rightarrow \psi )\land (\psi \rightarrow \phi ))$ .

Dedução Natural

Há um sistema de Dedução Natural que pode ser utilizado para tratar da lógica intuicionista, com a adição de uma regra, conhecida como regra do absurdo clássico, podemos utilizá-lo para a lógica clássica. Esse sistema é melhor explicado no artigo em Sistema intuitivo.

Cálculo de seqüentes

Gentzen descobriu que uma pequena restrição no seu sistema LK (seu sistema de cálculo de seqüentes para a lógica clássica) resulta em um sistema correto e completo em relação à lógica intuicionista, e denominou esse sistema LJ.

Relação com a lógica clássica

A lógica clássica pode ser obtida a partir da lógica intuicionista com a adição de um dos seguintes axiomas

$\alpha \lor \neg \alpha$ (Lei do terceiro excluído)
$(\alpha \rightarrow \beta )\rightarrow ((\neg \alpha \rightarrow \beta )\rightarrow \beta )$ (Outra formulação para a lei do terceiro excluído)
$\neg \neg \alpha \rightarrow \alpha$ (Eliminação da dupla negação)
$((\alpha \rightarrow \beta )\rightarrow \alpha )\rightarrow \alpha$ (Lei de Peirce)

Outro relacionamento é dado pela tradução negativa de Gödel-Gentzen, que apresenta uma forma de traduzir sentenças da lógica clássica de primeira ordem para a lógica intuicionista: uma fórmula em primeira ordem pode ser demonstrada se e somente se sua tradução Gödel-Gentzen puder ser demonstrada intuicionisticamente. Por isso, a lógica intuicionista também pode ser vista como uma forma de estender a lógica clássica com uma semântica construtivista.

Tomemos g(A) como tradução negativa de Gödel-Gentzen da fórmula clássica A, assim as fórmulas clássicas são traduzidas da seguinte forma:

$\,g(\alpha )$ traduz-se como $\neg \neg \alpha$ , se $\,\alpha$ é um átomo ou predicado 0-ário.
$g(\mathrm {A} \land \mathrm {B} )$ traduz-se como $g(\mathrm {A} )\land g(\mathrm {B} )$ .
$g(\mathrm {A} \lor \mathrm {B} )$ traduz-se como $\neg (\neg g(\mathrm {A} )\land \neg g(\mathrm {B} ))$ .
$g(\mathrm {A} \rightarrow \mathrm {B} )$ traduz-se como $g(\mathrm {A} )\rightarrow g(\mathrm {B} )$ .
$g(\neg \mathrm {A} )$ traduz-se como $\neg g(\mathrm {A} )$ .
$g(\forall xP(x))$ traduz-se como $\forall xg(P(x))$ .
$g(\exists xP(x))$ traduz-se como $\neg \forall x\neg g(P(x))$ .

Não-interdefinibilidade de operadores

Na lógica clássica proposicional, é possível tomar um dos conectivos: conjunção, disjunção, ou implicação como primitivo, e definir os outros dois a partir dele, em conjunto com a negação. De forma parecida, na lógica clássica de primeira ordem, pode-se definir um quantificador a partir do outro em conjunto com a negação.

Essas são consequências fundamentais da lei do terceiro excluído, que faz com que todos os conectivos sejam apenas funções booleanas. Essa lei não é preservada na lógica intuicionista, apenas a lei da não-contradição, e como resultado nenhum dos conectivos básicos podem ser dispensados e todos os axiomas são necessários, pois não há como definir um conectivo básico a partir de outro. Com isso, na maioria dos casos, apenas um dos lados das equivalências clássicas se mantêm. Os teoremas que valem intuicionisticamente são os seguintes:

Conjunção $\times$ disjunção:

$(\phi \wedge \psi )\to \neg (\neg \phi \vee \neg \psi )$
$(\phi \vee \psi )\to \neg (\neg \phi \wedge \neg \psi )$
$(\neg \phi \vee \neg \psi )\to \neg (\phi \wedge \psi )$
$(\neg \phi \wedge \neg \psi )\leftrightarrow \neg (\phi \vee \psi )$

Conjunçao $\times$ implicação

$(\phi \wedge \psi )\to \neg (\phi \to \neg \psi )$
$(\phi \to \psi )\to \neg (\phi \wedge \neg \psi )$
$(\phi \wedge \neg \psi )\to \neg (\phi \to \psi )$
$(\phi \to \neg \psi )\leftrightarrow \neg (\phi \wedge \psi )$

Disjunção $\times$ implicação

$(\phi \vee \psi )\to (\neg \phi \to \psi )$
$(\neg \phi \vee \psi )\to (\phi \to \psi )$
$\neg (\phi \to \psi )\to \neg (\neg \phi \vee \psi )$
$\neg (\phi \vee \psi )\leftrightarrow \neg (\neg \phi \to \psi )$

Quantificação universal $\times$ existencial:

$(\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))$
$(\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))$
$(\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))$
$(\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))$

Podemos ver, então, que uma afirmação do tipo "a ou b" é mais forte que "se a não for o caso, então b o é", enquanto elas são equivalentes na lógica clássica, e que, por outro lado, "não é o caso que a ou b" é equivalente a "nem a, nem b", assim como na lógica clássica.

Semântica

A semântica da lógica intuicionista é mais complicada que a da lógica clássica, pois ela não trabalha apenas com função sobre os valores verdadeiro e falso. Uma teoria de modelos para a lógica intuicionista pode ser dada através de álgebras de Heyting ou, equivalentemente, pela semântica de Kripke.

Semântica da álgebra de Heyting

Na lógica clássica, a fórmula deve possuir um valor de verdade, usualmente os valores são membros da álgebra booleana. Assim, nós temos o teorema que diz que a fórmula é uma tautologia na lógica clássica se para qualquer valoração de seus átomos, o valor final da fórmula for 1 (verdadeiro).

Na lógica intuicionista, não existem apenas dois valores possíveis para um átomo, e em geral o mesmo ocorre com fórmulas mais complexas. Uma das formas de dar conta disso é utilizando uma álgebra de Heyting, da qual a álgebra booleana é um caso especial. Para a lógica intuicionista, pode-se usar uma álgebra de Heyting em que os elementos são os subconjuntos abertos da linha real $\mathbb {R}$ para demonstrar fórmulas válidas.

Nesta álgebra, a conjunção é tratada como uma operação de interseção, a disjunção como uma operação de união e a implicação como o interior do conjunto resultante de uma operação do tipo: complemento do primeiro união com segundo $\,\phi \rightarrow \psi$ é tratado como o interior de $v(\phi )^{c}\,\cup \,v(\psi )$ ). O absurdo é tratado como conjunto vazio, sendo assim, a negação de um elemento é o interior do complemento do conjunto de valoração deste elemento.

Tome como exemplo: $(\neg \phi \land \phi )\rightarrow \psi$ ; essa fórmula é válida, pois, independentemente do valor atribuído a $\,\phi$ e a $\,\psi$ teremos a linha inteira dos reais ( $\,v$ representa uma valoração):

$v((\neg \phi \land \phi )\rightarrow \psi )=$

$=int(v(\neg \phi \land \phi )^{c}\,\cup \,v(\psi ))$

$=int((v(\neg \phi )\,\cap \,v(\phi ))^{c}\,\cup \,v(\psi ))$

$=int((int(v(\phi )^{c})\,\cap \,v(\phi ))^{c}\,\cup \,v(\psi ))$

$=int(\varnothing ^{c}\,\cup \,v(\psi ))$ - pois, graças a um teorema topológico, sabemos que o interior do complemento é um subconjunto do complemento.

$=int(\mathbb {R} \,\cup \,v(\psi ))$ - pois, nessa situação, o complemento de vazio é todo o conjunto dos reais.

$=int(\mathbb {R} )$ - pois um conjunto unido com algum subconjunto dele tem como resultado ele mesmo.

Então, $v((\neg \phi \land \phi )\rightarrow \psi )=\mathbb {R}$ - pois o interior do conjunto dos reais tem como resultado o próprio conjunto dos reais.

Também é fácil ver que a lei do terceiro excluído ( $\phi \lor \neg \phi$ ) é inválida, pois atribuindo a $\,\phi$ o valor $\,\{x:x>13\}$ , temos que o valor de $\neg \phi$ é $\,\{x:x<13\}$ e a união de ambos é $\,\{x:x\neq 13\}$ .

Semântica de Kripke

Feita com base em seu trabalho na semântica de lógicas modais, Saul Kripke criou outra semântica para a lógica intuicionista, conhecida como semântica de Kripke ou semântica relacional.^[1] Ela se baseia na hipótese que também vem do intuicionismo de que o conhecimento não é destruído, apenas construído.

A aplicação dessa semântica na lógica intuicionista parece bastante com a aplicação da semântica de mundos na lógica modal.

Uma estrutura de Kripke K para a linguagem L consiste de um conjunto parcialmente ordenado de nós e uma função domínio D que recebe um nó e retorna o conjunto de átomos válidos naquele nó, de forma que se um $\,k'$ for posterior a $\,k$ então $D(k)\subseteq D(k')$ . Considere também uma função f, associada a cada nó $\,k$ , que recebe predicados 0-ários e retorna o valor de verdade do predicado, naquele nó - $\,f(P,k)=verdade$ , no caso de o predicado ser verdadeiro naquele nó, e $\,f(P,k)=desconhecido$ , no caso de o predicado não ser verdadeiro naquele nó - e uma função T no formato $\,T(Q,k)$ , associada, também, a cada nó $\,k$ , que recebe predicados (n 1)-ários Q, com $n\in \mathbb {N}$ , tal que ela retorna o conjunto de (n 1)-tuplas de elementos do domínio $\,D(k)$ se essa tupla pertencer a relação Q. A função f se propaga de forma que se $\,k'$ for posterior a $\,k$ então se $\,f(P,k)=verdade$ , $\,f(P,k')=verdade$ e a função T se propaga de forma que se $\,k'$ for posterior a $\,k$ então $\,T(Q,k)\subseteq T(Q,k')$ .

As seguintes regras são definidas:

$k\vDash P$ , para o caso de $\,\alpha$ ser um predicado 0-ário, sse $\,f(P,k)=verdade$ .
$k\vDash Q(a0,a1,a2,...an)$ , para o caso de Q ser um predicado (n 1)-ário, sse $\,(a0,a1,a2,...,an)\in T(Q,k)$ .
$k\vDash (\mathrm {A} \land \mathrm {B} )$ , se $k\vDash \mathrm {A}$ e $k\vDash \mathrm {B}$ .
$k\vDash (\mathrm {A} \lor \mathrm {B} )$ , se $k\vDash \mathrm {A}$ ou $k\vDash \mathrm {B}$ .
$k\vDash (\mathrm {A} \rightarrow \mathrm {B} )$ , para todo $\,k'$ posterior a $\,k$ , se $k'\vDash \mathrm {A}$ então $k'\vDash \mathrm {B}$ .
$k\vDash (\neg \mathrm {A} )$ se, para nenhum $\,k'$ posterior a $\,k$ , $k'\vDash \mathrm {A}$ .
$k\vDash (\forall x(\mathrm {A} (x)))$ se, para todo $\,k'$ posterior a $\,k$ e todo $d\in D(k')$ , $k'\vDash (A(d))$ é o caso.
$k\vDash (\exists x(\mathrm {A} (x)))$ se existe algum $\,d$ tal que $d\in D(k)$ e $k\vDash \mathrm {A} (d)$ .

Também vale ressaltar que:

Não é possível $k\vDash (\mathrm {A} \land \neg \mathrm {A} )$ para qualquer sentença $\,\mathrm {A}$ e qualquer nó $\,k$ .
Se um nó $\,k'$ é posterior a um nó $\,k$ então se $k\vDash \mathrm {A}$ então $k'\vDash \mathrm {A}$ para qualquer sentença $\,\mathrm {A}$ .
Uma sentença $\,\mathrm {A}$ só pode ser uma tautologia se, para todo $\,k$ em todas as estruturas Kripke possíveis, $k\vDash \mathrm {A}$ .

Exemplo

Veremos se $\vDash (\neg \phi \land \phi )\rightarrow \psi$ é uma tautologia na lógica intuicionista.

Por definição, temos que em todos as estruturas K (1) $k\vDash (\neg \phi \land \phi )\rightarrow \psi$ para todo $k\in K$ . Pela definição de $\rightarrow$ e (1), temos que (2) se $k'\vDash (\neg \phi \land \phi )$ então (3) $k'\vDash \psi$ , para todo $\,k'$ posterior a $\,k$ . De (2), por definição, temos que $k'\nvDash (\neg \phi \land \phi )$ para qualquer $\,k'$ . Logo, $\vDash (\neg \phi \land \phi )\rightarrow \psi$ é uma tautologia na lógica intuicionista.

Propriedade existencial

Na lógica intuicionista, uma fórmula do tipo $\exists x\,A(x)$ só é demonstrável se for possível mostrar esse x. Outra coisa que deve-se notar é que, nessa lógica, fórmulas como $\alpha \land \beta$ são tautologias apenas se $\,\alpha$ e $\,\beta$ forem tautologias, assim como $\alpha \lor \beta$ apenas é tautologia se $\,\alpha$ ou $\,\beta$ for tautologia. Na lógica clássica é fácil de perceber que isso não se aplica utilizando a lei do terceiro excluído: $\alpha \lor \neg \alpha$ , pois não é verdade, em geral, que $\,\alpha$ seja uma tautologia, ou que $\neg \alpha$ o seja. Essa propriedade é chamada de propriedade existencial/disjuntiva.