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 , , , como conectivos básicos, tratando como a abreviatura . Na lógica intuicionista de primeira ordem, ambos os quantificadores , 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 , também a lei de Peirce e, até mesmo, a eliminação da dupla negação. Na lógica clássica ambos e 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 e deriva-se

e os axiomas são

  • ENTÃO-1:
  • ENTÃO-2:
  • E-1:
  • E-2:
  • E-3:
  • OU-1:
  • OU-2:
  • OU-3:
  • ABSURDO:

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

  • GEN-∀: de deriva-se , se x não for variável livre em
  • GEN-∃: de deriva-se , se x não for variável livre em

e os seguintes axiomas

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

Conectivos opcionais

Negação

Para incluir o conectivo para negação, no lugar de utilizá-la como abreviatura para , é suficiente adicionar os axiomas

  • NÃO-1′:
  • NÃO-2′:

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

  • NÃO-1:
  • NÃO-2:

alternativas para o NÃO-1 são ou .

Equivalência

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

  • SSE-1:
  • SSE-2:
  • SSE-3:

SSE-1 e SSE-2 podem ser combinados, utilizando a conjunção, em um só axioma .


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

  • (Lei do terceiro excluído)
  • (Outra formulação para a lei do terceiro excluído)
  • (Eliminação da dupla negação)
  • (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:

  • traduz-se como , se é um átomo ou predicado 0-ário.
  • traduz-se como .
  • traduz-se como .
  • traduz-se como .
  • traduz-se como .
  • traduz-se como .
  • traduz-se como .

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 disjunção:

Conjunçao implicação

Disjunção implicação

Quantificação universal existencial:

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

- pois, graças a um teorema topológico, sabemos que o interior do complemento é um subconjunto do complemento.

- pois, nessa situação, o complemento de vazio é todo o conjunto dos reais.

- pois um conjunto unido com algum subconjunto dele tem como resultado ele mesmo.

Então, - 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 () é inválida, pois atribuindo a o valor , temos que o valor de é e a união de ambos é .

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

As seguintes regras são definidas:

  • , para o caso de ser um predicado 0-ário, sse .
  • , para o caso de Q ser um predicado (n+1)-ário, sse .
  • , se e .
  • , se ou .
  • , para todo posterior a , se então .
  • se, para nenhum posterior a , .
  • se, para todo posterior a e todo , é o caso.
  • se existe algum tal que e .


Também vale ressaltar que:

  • Não é possível para qualquer sentença e qualquer nó .
  • Se um nó é posterior a um nó então se então para qualquer sentença .
  • Uma sentença só pode ser uma tautologia se, para todo em todas as estruturas Kripke possíveis, .


Exemplo

Veremos se é uma tautologia na lógica intuicionista.

Por definição, temos que em todos as estruturas K (1) para todo . Pela definição de e (1), temos que (2) se então (3) , para todo posterior a . De (2), por definição, temos que para qualquer . Logo, é uma tautologia na lógica intuicionista.


Propriedade existencial

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

Relação com outras lógicas

A lógica intuicionista é um tipo de lógica paracompleta, dual às lógicas paraconsistentes.


Ver também

Notas

  1. Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

Ligações externas