Heyting arithmetic

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.

References

• More details can be found on the Stanford encyclopedia page on intuitionistic logic.