Curry's paradox in contractionless constructive logic (Q1914375)

The paper shows the consistency of a naive abstraction principle in a logic which is \textit{D. Nelson's} logic of constructible falsity [J. Symb. Logic 14, 16-26 (1949; Zbl 0033.24304)] minus the contraction principle \(((\alpha\to(\alpha\to\beta))\to (\alpha\to \beta))\). The result is established proof-theoretically, via a suitable normal form theorem. Comparisons are made with results for the similar logics of \textit{F. B. Fitch} [Symbolic logic. An introduction (1952; Zbl 0049.00504)], \textit{D. Prawitz} [Natural deduction (1965; Zbl 0173.00205)] and the BCK logic of \textit{H. Ono} and \textit{Y. Komori} [J. Symb. Logic 50, 169-201 (1985; Zbl 0583.03018)]. Although the paper calls this system `naive set theory', there is no extensionality axiom; nor does it discuss the consistency of adding one. -- Adding one to the naive abstraction schema in the slightly stronger Łukasiewicz' infinite-valued logic is provably inconsistent [see \textit{R. White}, J. Philos. Logic 8, 509-534 (1979; Zbl 0418.03037)].