Abstrakt
Heyting arithmetic HA is a well established intuitionistic theory. As a counterpart to Peano arithmetic PA, it forms the theory of constructive arithmetic.
Its induction-less variant, the intuitionistic Robinson arithmetic iQ, is not as well understood though. One of the problems with iQ is that there is no true agreement among logicians what iQ is.
Looking at the literature one finds two distinct non-equivalent axiomatics of iQ. We'll look at the differences and compare these two axiomatics with respect to provability strength, models, and translations.