[Prev][Next][Index][Thread]

Re: Second order logic and recursion

>[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>
>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.

Given the relation between recursion and induction (see [3] for a
discussion of this in relation to the Calculus of Constructions), it would
appear to be enough to add induction.  This can be done in second- and
higher-order logic by defining a predicate in the way Dedekind did for the
natural numbers as the predicate which applies to those objects which
satisfy all predicates which apply to zero and are closed under successor.
This approach is carried out for the Calculus of Constructions in [4, p.
83].  With this approach, the induction "axiom" becomes a theorem, and the
logic can be used to prove that definition by recursion works (using, e.g.,
Kalmar's proof as presented in Landau's _Grundlagen der Analysis_).

References:
[3] F. Pfenning and C. Paulin-Mohring, Inductively Defined Types in the
Calculus of Constructions, SLNCS 442, pp. 209-228.
[4] J. P. Seldin, On the Proof Theory of Coquand's Calculus of
Constructions, Ann. Pure and Applied Logic 83 (1997) 23-101.

Jonathan P. Seldin                                      tel: 514-848-3254
Department of Mathematics                       seldin@alcor.concordia.ca
Concordia University                         seldin@poincare.concordia.ca
Montreal, Quebec, Canada		http://alcor.concordia.ca/~seldin
(Please to NOT reply to the e-mail address at Swansea.)