A negationless interpretation of intuitionistic theories. II (Q1582305)

The author introduces negationless higher-order arithmetic, NAH, proves the translatability of HAH (intuitionistic higher-order arithmetic with product types, power types, and a type of natural numbers satisfying Heyting Arithmetic with full induction [cf. \textit{A. S. Troelstra} and \textit{D. van Dalen}, Constructivism in mathematics. An introduction. Vol. I, North-Holland, Amsterdam (1988; Zbl 0653.03040), pp. 168ff.] into NAH, and shows that NPC from Part I [Stud. Log. 64, No. 3, 323-344 (2000; Zbl 0964.03065)] is equivalent to a slight modification of the \(\Sigma\)-free fragment of Nelson's \(P_1\).