Aritmética de Heyting
 | Este artigo não cita fontes confiáveis. (Novembro de 2011) |
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.
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.
