Tukukkk

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 →{displaystyle ,rightarrow }, ∧{displaystyle ,land }, ∨{displaystyle ,lor }, ⊥{displaystyle ,bot } como conectivos básicos, tratando ¬{displaystyle ,neg } como a abreviatura ¬α=(α→⊥){displaystyle neg alpha =(alpha rightarrow bot )}. Na lógica intuicionista de primeira ordem, ambos os quantificadores ∃{displaystyle ,exists }, ∀{displaystyle ,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 α∨¬α{displaystyle alpha lor neg alpha }, também a lei de Peirce ((α→β)→α)→α{displaystyle ((alpha rightarrow beta )rightarrow alpha )rightarrow alpha } e, até mesmo, a eliminação da dupla negação. Na lógica clássica ambos α→¬¬α{displaystyle alpha rightarrow neg neg alpha } e ¬¬α→α{displaystyle 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 |

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 ϕ→(∀xψ){displaystyle phi rightarrow (forall xpsi )}, se x não for variável livre em ϕ{displaystyle ,phi }
  


• GEN-∃: de ϕ→ψ{displaystyle phi rightarrow psi } deriva-se (∃xϕ)→ψ{displaystyle (exists xphi )rightarrow psi }, se x não for variável livre em ψ{displaystyle ,psi }
  

e os seguintes axiomas

• PRED-1: (∀xϕ(x))→ϕ(t){displaystyle (forall xphi (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: ϕ(t)→(∃xϕ(x)){displaystyle phi (t)rightarrow (exists xphi (x))}, com as mesmas restrições acima

Conectivos opcionais |

Negação |

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

Equivalência |

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 ))}.

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

• 
  α∨¬α{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:

• 
  g(α){displaystyle ,g(alpha )} traduz-se como ¬¬α{displaystyle neg neg alpha }, se α{displaystyle ,alpha } é um átomo ou predicado 0-ário.


• 
  g(A∧B){displaystyle g(mathrm {A} land mathrm {B} )} traduz-se como g(A)∧g(B){displaystyle g(mathrm {A} )land g(mathrm {B} )}.


• 
  g(A∨B){displaystyle g(mathrm {A} lor mathrm {B} )} traduz-se como ¬(¬g(A)∧¬g(B)){displaystyle neg (neg g(mathrm {A} )land neg g(mathrm {B} ))}.


• 
  g(A→B){displaystyle g(mathrm {A} rightarrow mathrm {B} )} traduz-se como g(A)→g(B){displaystyle g(mathrm {A} )rightarrow g(mathrm {B} )}.


• 
  g(¬A){displaystyle g(neg mathrm {A} )} traduz-se como ¬g(A){displaystyle neg g(mathrm {A} )}.


• 
  g(∀xP(x)){displaystyle g(forall xP(x))} traduz-se como ∀xg(P(x)){displaystyle forall xg(P(x))}.


• 
  g(∃xP(x)){displaystyle g(exists xP(x))} traduz-se como ¬∀x¬g(P(x)){displaystyle neg forall xneg 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 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 ×{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:

• (∀x ϕ(x))→¬(∃x ¬ϕ(x)){displaystyle (forall x phi (x))to neg (exists x neg phi (x))}


• (∃x ϕ(x))→¬(∀x ¬ϕ(x)){displaystyle (exists x phi (x))to neg (forall x neg phi (x))}


• (∃x ¬ϕ(x))→¬(∀x ϕ(x)){displaystyle (exists x neg phi (x))to neg (forall x phi (x))}


• (∀x ¬ϕ(x))↔¬(∃x ϕ(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.

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 R{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 v(ϕ)c∪v(ψ){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 (v{displaystyle ,v} representa uma valoração):

v((¬ϕ∧ϕ)→ψ)={displaystyle v((neg phi land phi )rightarrow psi )=}

=int(v(¬ϕ∧ϕ)c∪v(ψ)){displaystyle =int(v(neg phi land phi )^{c},cup ,v(psi ))}

=int((v(¬ϕ)∩v(ϕ))c∪v(ψ)){displaystyle =int((v(neg phi ),cap ,v(phi ))^{c},cup ,v(psi ))}

=int((int(v(ϕ)c)∩v(ϕ))c∪v(ψ)){displaystyle =int((int(v(phi )^{c}),cap ,v(phi ))^{c},cup ,v(psi ))}

=int(∅c∪v(ψ)){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.

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

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

Então, v((¬ϕ∧ϕ)→ψ)=R{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 {x:x>13}{displaystyle ,{x:x>13}}, temos que o valor de ¬ϕ{displaystyle neg phi } é {x:x<13}{displaystyle ,{x:x<13}} e a união de ambos é {x:x≠13}{displaystyle ,{x:xneq 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′{displaystyle ,k'} for posterior a k{displaystyle ,k} então D(k)⊆D(k′){displaystyle D(k)subseteq D(k')}. Considere também uma função f, associada a cada nó k{displaystyle ,k}, que recebe predicados 0-ários e retorna o valor de verdade do predicado, naquele nó - f(P,k)=verdade{displaystyle ,f(P,k)=verdade}, no caso de o predicado ser verdadeiro naquele nó, e f(P,k)=desconhecido{displaystyle ,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){displaystyle ,T(Q,k)}, associada, também, a cada nó k{displaystyle ,k}, que recebe predicados (n+1)-ários Q, com n∈N{displaystyle nin mathbb {N} }, tal que ela retorna o conjunto de (n+1)-tuplas de elementos do domínio D(k){displaystyle ,D(k)} se essa tupla pertencer a relação Q. A função f se propaga de forma que se k′{displaystyle ,k'} for posterior a k{displaystyle ,k} então se f(P,k)=verdade{displaystyle ,f(P,k)=verdade}, f(P,k′)=verdade{displaystyle ,f(P,k')=verdade} e a função T se propaga de forma que se k′{displaystyle ,k'} for posterior a k{displaystyle ,k} então T(Q,k)⊆T(Q,k′){displaystyle ,T(Q,k)subseteq T(Q,k')}.

As seguintes regras são definidas:

• 
  k⊨P{displaystyle kvDash P}, para o caso de α{displaystyle ,alpha } ser um predicado 0-ário, sse f(P,k)=verdade{displaystyle ,f(P,k)=verdade}.


• 
  k⊨Q(a0,a1,a2,...an){displaystyle kvDash Q(a0,a1,a2,...an)}, para o caso de Q ser um predicado (n+1)-ário, sse (a0,a1,a2,...,an)∈T(Q,k){displaystyle ,(a0,a1,a2,...,an)in T(Q,k)}.


• 
  k⊨(A∧B){displaystyle kvDash (mathrm {A} land mathrm {B} )}, se k⊨A{displaystyle kvDash mathrm {A} } e k⊨B{displaystyle kvDash mathrm {B} }.


• 
  k⊨(A∨B){displaystyle kvDash (mathrm {A} lor mathrm {B} )}, se k⊨A{displaystyle kvDash mathrm {A} } ou k⊨B{displaystyle kvDash mathrm {B} }.


• 
  k⊨(A→B){displaystyle kvDash (mathrm {A} rightarrow mathrm {B} )}, para todo k′{displaystyle ,k'} posterior a k{displaystyle ,k}, se k′⊨A{displaystyle k'vDash mathrm {A} } então k′⊨B{displaystyle k'vDash mathrm {B} }.


• 
  k⊨(¬A){displaystyle kvDash (neg mathrm {A} )} se, para nenhum k′{displaystyle ,k'} posterior a k{displaystyle ,k}, k′⊨A{displaystyle k'vDash mathrm {A} }.


• 
  k⊨(∀x(A(x))){displaystyle kvDash (forall x(mathrm {A} (x)))} se, para todo k′{displaystyle ,k'} posterior a k{displaystyle ,k} e todo d∈D(k′){displaystyle din D(k')}, k′⊨(A(d)){displaystyle k'vDash (A(d))} é o caso.


• 
  k⊨(∃x(A(x))){displaystyle kvDash (exists x(mathrm {A} (x)))} se existe algum d{displaystyle ,d} tal que d∈D(k){displaystyle din D(k)} e k⊨A(d){displaystyle kvDash mathrm {A} (d)}.

Também vale ressaltar que:

• Não é possível k⊨(A∧¬A){displaystyle kvDash (mathrm {A} land neg mathrm {A} )} para qualquer sentença A{displaystyle ,mathrm {A} } e qualquer nó k{displaystyle ,k}.


• Se um nó k′{displaystyle ,k'} é posterior a um nó k{displaystyle ,k} então se k⊨A{displaystyle kvDash mathrm {A} } então k′⊨A{displaystyle k'vDash mathrm {A} } para qualquer sentença A{displaystyle ,mathrm {A} }.


• Uma sentença A{displaystyle ,mathrm {A} } só pode ser uma tautologia se, para todo k{displaystyle ,k} em todas as estruturas Kripke possíveis, k⊨A{displaystyle kvDash mathrm {A} }.

Exemplo |

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) k⊨(¬ϕ∧ϕ)→ψ{displaystyle kvDash (neg phi land phi )rightarrow psi } para todo k∈K{displaystyle kin K}. Pela definição de →{displaystyle rightarrow } e (1), temos que (2) se k′⊨(¬ϕ∧ϕ){displaystyle k'vDash (neg phi land phi )} então (3) k′⊨ψ{displaystyle k'vDash psi }, para todo k′{displaystyle ,k'} posterior a k{displaystyle ,k}. De (2), por definição, temos que k′⊭(¬ϕ∧ϕ){displaystyle k'nvDash (neg phi land phi )} para qualquer k′{displaystyle ,k'}. Logo, ⊨(¬ϕ∧ϕ)→ψ{displaystyle vDash (neg phi land phi )rightarrow psi } é uma tautologia na lógica intuicionista.

Propriedade existencial |

Na lógica intuicionista, uma fórmula do tipo ∃xA(x){displaystyle 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 α∧β{displaystyle alpha land beta } são tautologias apenas se α{displaystyle ,alpha } e β{displaystyle ,beta } forem tautologias, assim como α∨β{displaystyle alpha lor beta } apenas é tautologia se α{displaystyle ,alpha } ou β{displaystyle ,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: α∨¬α{displaystyle alpha lor neg alpha }, pois não é verdade, em geral, que α{displaystyle ,alpha } seja uma tautologia, ou que ¬α{displaystyle neg alpha } 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 |

Ligações externas |

Logic

• 
  Stanford Encyclopedia of Philosophy: "Intuitionistic Logic" -- by Joan Moschovakis.


• Intuitionistic Logic