В математической логике, арифметика Гейтинга (иногда сокращенно HA ) - это аксиоматизация арифметики в соответствии с философией интуиционизм. Он назван в честь Аренд Хейтинг, который первым предложил его.
Арифметика Гейтинга принимает аксиомы арифметики Пеано (PA), но использует интуиционистскую логику в качестве правил вывода. В частности, закон исключенного третьего в целом не выполняется, хотя аксиома индукции может использоваться для доказательства многих конкретных случаев. Например, можно доказать, что ∀ x, y ∈ N : x = y ∨ x ≠ y является теоремой (любые два натуральных числа либо равны друг другу, либо не равны равны друг другу). Фактически, поскольку "=" является единственным символом предиката в арифметике Гейтинга, отсюда следует, что для любой кванторной формулы p, ∀ x, y, z,… ∈ N : p ∨ ¬p - это теорема (где x, y, z… - свободные переменные в p).
Курт Гёдель изучал взаимосвязь между арифметикой Гейтинга и арифметикой Пеано. Он использовал негативный перевод Гёделя – Гентцена, чтобы доказать в 1933 году, что если HA непротиворечиво, то PA также непротиворечиво.
Арифметику Гейтинга не следует путать с алгебрами Гейтинга, которые являются интуиционистским аналогом булевых алгебр.
.