Aritmética de Heyting - Heyting arithmetic
Na lógica matemática , a aritmética de Heyting (às vezes abreviada como HA ) é uma axiomatização da aritmética de acordo com a filosofia do intuicionismo . Tem o nome de Arend Heyting , que o propôs pela primeira vez.
Introdução
A aritmética de Heyting adota os axiomas da aritmética de Peano (PA), mas usa a lógica intuicionista como suas regras de inferência. Em particular, a lei do terceiro excluído não se aplica em geral, embora o axioma da indução possa ser usado para provar muitos casos específicos. Por exemplo, pode-se provar que ∀ x , y ∈ N : x = y ∨ x ≠ y é um teorema (quaisquer dois números naturais são iguais um ao outro ou não iguais um ao outro). Na verdade, uma vez que "=" é o único símbolo predicado na aritmética de Heyting, segue-se que, para qualquer quantificador - fórmula livre φ , ∀ x , y , z , ... ∈ N : φ ∨ ¬ φ é um teorema ( onde x , y , z ... são as variáveis livres em φ ).
História
Kurt Gödel estudou a relação entre a aritmética de Heyting e a aritmética de Peano. Ele usou a tradução negativa de Gödel-Gentzen para provar em 1933 que se HA é consistente, então PA também é consistente.
Conceitos relacionados
A aritmética de Heyting não deve ser confundida com as álgebras de Heyting , que são o análogo intuicionista das álgebras booleanas .
Veja também
Referências
- Ulrich Kohlenbach (2008), teoria da prova aplicada , Springer.
- Anne S. Troelstra , ed. (1973), Metamathematical research of intuitionistic arithmetic and analysis , Springer, 1973.
links externos
- Stanford Encyclopedia of Philosophy : " Intuitionistic Number Theory " por Joan Moschovakis .
- Fragments of Heyting Arithmetic de Wolfgang Burr
 |
Este artigo relacionado à lógica matemática é um esboço . Você pode ajudar a Wikipedia expandindo-a . |