Aritmética de Heyting
Da Wikipédia, a enciclopédia livre
Na lógica matemática, aritmética de Heyting (às vezes abreviada como HA -sigla inglesa) é uma axiomatização de aritmética de acordo com a filosofia do intuicionismo.
 | Este artigo não cita fontes confiáveis. (Novembro de 2011) |
Recebeu o nome de Arend Heyting, que a propôs primeiro.
A aritmética de Heyting adota o axioma da aritmética de Peano (PA -sigla inglesa), mas usa a lógica intuicionista como suas regras de inferência. Em particular, a lei do meio excluído não se contém em geral, embora um axioma de indução possa ser usado para provar muitos casos específicos. Por exemplo, é possível provar que ∀ x, y ∈ N : x = y &ou; x ≠ y é um teorema (quaisquer dois números naturais são ou igual um ao outro, ou não igual um ao outro). De fato, desde que o "=" é apenas símbolo de predicado na matemática de Heyting, ele então tem que, para qualquer fórmula livre de quantificador p, ∀ x, y, z, … ∈ N : p &ou; ¬p é um teorema (onde x,y,z… são variáveis livres em p).
Kurt Gödel estudou o relacionamento entre a aritmética de Heyting e a de Peano. Usou a tradução negativa de Gödel–Gentzen para provar em 1933 que se a HA é consistente, então a PA também é.
Aritmética Heyting não deveria ser confundida com as álgebra de Heyting, que são as análogas intuicionísticas da Álgebra booleana.
- Fórmula Harrop
- Interpretação BHK
- Stanford Encyclopedia of Philosophy: "Teoria Intuicionística do Número" de Joan Moschovakis.
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
