Lógica intuicionista

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 ${\displaystyle \,\phi }$ e ${\displaystyle \phi \rightarrow \psi }$ deriva-se ${\displaystyle \,\psi }$

e os axiomas são

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

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

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

e os seguintes axiomas

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

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

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

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

• NÃO-1: ${\displaystyle (\phi \rightarrow \psi )\rightarrow ((\phi \rightarrow \neg \psi )\rightarrow \neg \phi )}$
• NÃO-2: ${\displaystyle \phi \rightarrow (\neg \phi \rightarrow \psi )}$

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

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

• SSE-1: ${\displaystyle (\phi \leftrightarrow \psi )\rightarrow (\phi \rightarrow \psi )}$
• SSE-2: ${\displaystyle (\phi \leftrightarrow \psi )\rightarrow (\psi \rightarrow \phi )}$
• SSE-3: ${\displaystyle (\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 ${\displaystyle (\phi \leftrightarrow \psi )\rightarrow ((\phi \rightarrow \psi )\land (\psi \rightarrow \phi ))}$.

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.

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.

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

• ${\displaystyle \alpha \lor \neg \alpha }$ (Lei do terceiro excluído)
• ${\displaystyle (\alpha \rightarrow \beta )\rightarrow ((\neg \alpha \rightarrow \beta )\rightarrow \beta )}$ (Outra formulação para a lei do terceiro excluído)
• ${\displaystyle \neg \neg \alpha \rightarrow \alpha }$ (Eliminação da dupla negação)
• ${\displaystyle ((\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:

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

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 ${\displaystyle \times }$ disjunção:

• ${\displaystyle (\phi \wedge \psi )\to \neg (\neg \phi \vee \neg \psi )}$
• ${\displaystyle (\phi \vee \psi )\to \neg (\neg \phi \wedge \neg \psi )}$
• ${\displaystyle (\neg \phi \vee \neg \psi )\to \neg (\phi \wedge \psi )}$
• ${\displaystyle (\neg \phi \wedge \neg \psi )\leftrightarrow \neg (\phi \vee \psi )}$

Conjunçao ${\displaystyle \times }$ implicação

• ${\displaystyle (\phi \wedge \psi )\to \neg (\phi \to \neg \psi )}$
• ${\displaystyle (\phi \to \psi )\to \neg (\phi \wedge \neg \psi )}$
• ${\displaystyle (\phi \wedge \neg \psi )\to \neg (\phi \to \psi )}$
• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \wedge \psi )}$

Disjunção ${\displaystyle \times }$ implicação

• ${\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}$
• ${\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}$
• ${\displaystyle \neg (\phi \to \psi )\to \neg (\neg \phi \vee \psi )}$
• ${\displaystyle \neg (\phi \vee \psi )\leftrightarrow \neg (\neg \phi \to \psi )}$

Quantificação universal ${\displaystyle \times }$ existencial:

• ${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$
• ${\displaystyle (\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.

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 ${\displaystyle \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 ${\displaystyle \,\phi \rightarrow \psi }$ é tratado como o interior de ${\displaystyle 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: ${\displaystyle (\neg \phi \land \phi )\rightarrow \psi }$; essa fórmula é válida, pois, independentemente do valor atribuído a ${\displaystyle \,\phi }$ e a ${\displaystyle \,\psi }$ teremos a linha inteira dos reais (${\displaystyle \,v}$ representa uma valoração):

${\displaystyle v((\neg \phi \land \phi )\rightarrow \psi )=}$

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

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

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

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

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

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

Então, ${\displaystyle 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 (${\displaystyle \phi \lor \neg \phi }$) é inválida, pois atribuindo a ${\displaystyle \,\phi }$ o valor ${\displaystyle \,\{x:x>13\}}$, temos que o valor de ${\displaystyle \neg \phi }$ é ${\displaystyle \,\{x:x<13\}}$ e a união de ambos é ${\displaystyle \,\{x:x\neq 13\}}$.

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 ${\displaystyle \,k'}$ for posterior a ${\displaystyle \,k}$ então ${\displaystyle D(k)\subseteq D(k')}$. Considere também uma função f, associada a cada nó ${\displaystyle \,k}$, que recebe predicados 0-ários e retorna o valor de verdade do predicado, naquele nó - ${\displaystyle \,f(P,k)=verdade}$, no caso de o predicado ser verdadeiro naquele nó, e ${\displaystyle \,f(P,k)=desconhecido}$, no caso de o predicado não ser verdadeiro naquele nó - e uma função T no formato ${\displaystyle \,T(Q,k)}$, associada, também, a cada nó ${\displaystyle \,k}$, que recebe predicados (n+1)-ários Q, com ${\displaystyle n\in \mathbb {N} }$, tal que ela retorna o conjunto de (n+1)-tuplas de elementos do domínio ${\displaystyle \,D(k)}$ se essa tupla pertencer a relação Q. A função f se propaga de forma que se ${\displaystyle \,k'}$ for posterior a ${\displaystyle \,k}$ então se ${\displaystyle \,f(P,k)=verdade}$, ${\displaystyle \,f(P,k')=verdade}$ e a função T se propaga de forma que se ${\displaystyle \,k'}$ for posterior a ${\displaystyle \,k}$ então ${\displaystyle \,T(Q,k)\subseteq T(Q,k')}$.

As seguintes regras são definidas:

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

Também vale ressaltar que:

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

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

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