Heyting arithmetic (HA) is a first-order, formal theory of arithmetic.
It is the system obtained if one removes all classical reasoning principles from Peano arithmetic. As such, it is, conceptually, the simplest intuitonistic theory of arithmetic. For that reason, it is also sometimes called intuitionistic number theory.