A Negationless Interpretation of Intuitionistic Axiomatic Theories: Higher-Order Arithmetic
Victor N. Krivtsov

Abstract:
A Negationless Interpretation of Intuitionistic Axiomatic Theories:
Higher-order Arithmetic
Victor N. Krivtsov

This work is a sequel to our [14] (ed: report ML-1998-06). It is shown how 
Theorem 6 of [14], dealing with the translatability of {\bf HA} (Heyting's
arithmetic) into negationless arithmetic {\bf NA}, can be extended to the 
case of intuitionistic arithmetic in higher types.