Lógica intuicionista

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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[editar | editar código-fonte]

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

Cálculo à la Hilbert[editar | editar código-fonte]

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\and\psi\rightarrow\phi
  • E-2: \phi\and\psi\rightarrow\psi
  • E-3: \phi\rightarrow(\psi\rightarrow(\phi\and\psi))
  • OU-1: \phi\rightarrow\phi\or\psi
  • OU-2: \psi\rightarrow\phi\or\psi
  • OU-3: (\phi\rightarrow\psi)\rightarrow((\gamma\rightarrow\psi)\rightarrow(\phi\or\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\psideriva-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[editar | editar código-fonte]

Negação[editar | editar código-fonte]

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[editar | editar código-fonte]

O conectivo \,\leftrightarrow (bi-implicação) para equivalência pode ser tratado como abreviatura, com \phi\leftrightarrow\psi significando (\phi\rightarrow\psi)\and(\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)\and(\psi\rightarrow\phi)).


Dedução Natural[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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

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(\Alpha\and\Beta) traduz-se como g(\Alpha)\and g(\Beta).
  • g(\Alpha\or\Beta) traduz-se como \neg(\neg g(\Alpha)\and\neg g(\Beta)).
  • g(\Alpha\rightarrow\Beta) traduz-se como g(\Alpha)\rightarrow g(\Beta).
  • g(\neg\Alpha) traduz-se como \neg g(\Alpha).
  • g(\forall xP(x)) traduz-se como \forall x g(P(x)).
  • g(\exists xP(x)) traduz-se como \neg\forall x\neg g(P(x)).

Não-interdefinibilidade de operadores[editar | editar código-fonte]

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 \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 (\exist x \ \neg \phi(x))
  • (\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))
  • (\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))
  • (\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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\and\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\and\phi)\rightarrow\psi)=

=int(v(\neg\phi\and\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\and\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\or\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 \ne 13 \}.

Semântica de Kripke[editar | editar código-fonte]

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\isin\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)\isin T(Q,k).
  • k\vDash(\Alpha\and\Beta), se k\vDash\Alpha e k\vDash\Beta.
  • k\vDash(\Alpha\or\Beta), se k\vDash\Alpha ou k\vDash\Beta.
  • k\vDash(\Alpha\rightarrow\Beta), para todo \, k' posterior a \, k, se k'\vDash\Alpha então k'\vDash\Beta.
  • k\vDash(\neg\Alpha) se, para nenhum \, k' posterior a \, k, k'\vDash\Alpha.
  • k\vDash(\forall x(\Alpha (x))) se, para todo \, k' posterior a \, k e todo d\isin D(k'), k'\vDash(A(d)) é o caso.
  • k\vDash(\exists x(\Alpha (x))) se existe algum \, d tal que d\isin D(k) e k\vDash\Alpha(d).


Também vale ressaltar que:

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


Exemplo[editar | editar código-fonte]

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

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


Propriedade existencial[editar | editar código-fonte]

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\and\beta são tautologias apenas se \,\alpha e \,\beta forem tautologias, assim como \alpha\or\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\or\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.

Relação com outras lógicas[editar | editar código-fonte]

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


Ver também[editar | editar código-fonte]

Notas[editar | editar código-fonte]

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

Ligações externas[editar | editar código-fonte]