Aritmética de Heyting

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 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 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 , que são as análogas intuicionísticas da Álgebra booleana.