[Prev][Next][Index][Thread]
Second order logic and recursion
The correspondence between second-order logic and the Girard-Reynolds
polymorphic lambda-calculus is fairly well known, see for example [1].
For the natural deduction presentation of second order logic (also for
sequent calculus) proofs of cut elimination (by Girard, Martin-Lof)
can be found in [2].
By the isomorphism, in a given context C a term M has type t, iff (the
range of C) |C| |- t has a proof in the {\/, ->) fragment of the
second order intuitionistic propositional logic [Theorem in 1, pg198].
Question: How does recursion appear in the logic? And if we introduce
(first order) recursion, do we still have cut elimination (proofs in
normal form)?
Any insights, pointers are welcome.
Thanks,
Laszlo Nemeth
References:
[1] M.H.B.Sorensen and P.Urzyczyn: Lectures on the Curry-Howard Isomorphism
[2] J.E.Fenstad(Ed): Proceedings of the Second Scandianavian Logic Symposium
Amsterdam 1971.