Pedagogical second-order λλ-calculus

The present work introduces the notion of pedagogical natural deduction systems, i.e. natural deduction systems for which hypotheses occurring in a proof must be motivated by an example. In formal terms, we replace the rule (Hyp): by the rule (P-Hyp): where σσ denotes a substitution which replaces all variables of ΓΓ with an example. This substitution is called the motivation   of ΓΓ. These systems are in essence negationless. In the present paper, we study second order propositional calculus, since it is a simple non-trivial natural deduction system in which negation can be defined. We present a Curry–Howard version of pedagogical second-order propositional calculus, i.e.  λλ-calculus bearing the pedagogical constraint. We establish that this system has the usual properties of typed calculi (subject reduction and strong normalization) and that it can type all second-order terms of λμλμ-calculus using a CPS translation. Furthermore, the main novelty is that all functions are useful: each polymorphic function has an instance which can be applied to a closed term.