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 é 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, é 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.
Ver também Fórmula Harrop Interpretação BHK
Ligações externas Stanford Encyclopedia of Philosophy: "Teoria Intuicionística do Número" de Joan Moschovakis.
Categoria:Construtivismo matemático Categoria:Intuicionismo