# Can induction be proven in $\lambda C$?

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$$

• 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. – Rob Arthan Apr 10 at 20:19
• 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. – Stefan Apr 10 at 23:43