A negationless interpretation of intuitionistic theories. II (Q1582305)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A negationless interpretation of intuitionistic theories. II |
scientific article |
Statements
A negationless interpretation of intuitionistic theories. II (English)
0 references
6 February 2001
0 references
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\).
0 references
intuitionistic higher-order arithmetic
0 references
negationless higher-order arithmetic
0 references