Abrir menu principal

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.

SintaxeEditar

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 à idéia de enfraquecimento na teoria de demonstrações da lógica clássica.

Cálculo à la HilbertEditar

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 opcionaisEditar

NegaçãoEditar

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ênciaEditar

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 NaturalEditar

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üentesEditar

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ássicaEditar

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 operadoresEditar

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 conseqüê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ânticaEditar

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 HeytingEditar

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 KripkeEditar

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,  .


ExemploEditar

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 existencialEditar

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ógicasEditar

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


Ver tambémEditar

NotasEditar

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

Ligações externasEditar