Predicate logics of constructive arithmetical theories

摘要

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 Pi(0)(2). Similarly, we show that the predicate logic of HA*. i.e. Heyting's Arithmetic plus the Completeness Principle (for HA*) is complete Pi(0)(2). These results extend the known results due to Valery Plisko. To prove the results we adapt Plisko's method to use Tennenhaum's Theorem to prove 'categoricity of interpretations' under certain assumptions.