Second order logic and recursion

• To: types@cis.upenn.edu
• Subject: Second order logic and recursion
• From: Laszlo Nemeth <laszlo@dcs.gla.ac.uk>
• Date: Tue, 29 Jun 1999 12:44:51 +0100 (BST)

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.

• Prev: Posts at Heriot-Watt
• Next: Re: Second order logic and recursion
• Index(es):
  • Main
  • Thread