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.
Albert Visser. "Predicate logics of constructive arithmetical theories." J. Symbolic Logic 71 (4) 1311 - 1326, December 2006. https://doi.org/10.2178/jsl/1164060457
Information