Relative interpretations in constructive arithmetic

In this paper, we show that the predicate logics of consistent extensions of Heyting’s Arithmetic plus Church’s Thesis with uniqueness condition are complete II0/2. Similarly, we show that the predicate logic of HA*, i.e. Heyting’s Arithmetic plus the Completeness Principle (for HA*) is complete II0/2. These results extend the known results due to Valery Plisko. To prove the results we adapt Plisko’s method to use Tennenbaum’s Theorem to prove ‘categoricity of interpretations’ under certain assumptions