Is it possible to prove induction in $\lambda C$? In other words, is the following type inhabited?

$$\Pi P:\mathbf{nat} \to \ast. (P0 \land \Pi n : \mathbf{nat}. Pn \to P(\mathbf{succ}\ n)) \to \Pi n : \mathbf{nat}. Pn$$

  • $\begingroup$ I'm not sure what type theory you are working in, but the type should be inhabited in any reasonable type theory: the inhabitant takes as parameters (1) a proof of $P\,0$, (2) a function that transforms a proof of $P\,n$ into a proof of $P(\mathbf{succ}\,n)$, and (3) a natural number $n$; using recursion on $n$ it constructs a proof of $P\,n$ from that data. $\endgroup$ – Rob Arthan Apr 10 at 20:19
  • $\begingroup$ I'm using the $\lambda C$ system defined in Lambda Calculi with Types by Barendregt. I'm not sure how I can use recursion in this system. $\endgroup$ – Stefan Apr 10 at 23:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.