Predicate Logics of Constructive Arithmetical Theories
Albert Visser · Journal of Symbolic Logic · 2006
Abstract 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 . Similarly, we show that the predicate logic of HA*. i.e. Heyting's Arithmetic plus the Completeness Principle (for HA*) is complete . 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.