AN EMBEDDING OF 2ND-ORDER CLASSICAL-LOGIC INTO FA(2)

One embeds 2(nd) order classical logic, expressed as a natural deducti on with the rule of reductio ad absurdum (RAA), into the same calculus without RAA, in other words into 2(nd) order functional arithmetic FA (2) (see [1], ch. 9): Using the fact that reductio ad absurdum --A pro ves A can be intuitionistically proved from its restriction to the cas e where A is atomic (see [5], ch. 3 1), one merely relativize the form ulae to the ''classical'' predicates i.e. to the predicates P satisfyi ng --P --> P. Like the -(o)-traduction of [1], ch. 10, this embedding allows to translate a classical proof of function totality into an int uitionistic one. The normalization of the proof translations proves to be an analysis of the lambda mu-calculus reduction (see [2], [3], and [4]), so that the strong normalization property of the 2(nd) order la mbda mu-calculus follows at once from that of system F. Moreover in th e lambda mu-calculus with eta mu-expansion (see below), the translatio n keeps normal from of proofs and even set up a 1-1 correspondence bet ween the closed normal lambda mu-terms of type A and the normal (intui tionistic) proofs of the relativization A of A for sufficiently simpl e types A, in particular-for the integer type N. Therefore, the normal proofs of N in FA(2) are exactly the classical integer representatio ns of the lambda mu-calculus.