Why it's impossible to declare an induction principle for Church numerals

Question

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way:

SimpleNat = (R : Set) → R → (R → R) → R

zero : SimpleNat
zero = λ R z _ → z

suc : SimpleNat → SimpleNat
suc sn = λ R z s → s (sn R z s)

SimpleNatRec : (R : Set) → R → (R → R) → SimpleNat → R
SimpleNatRec R z s sn = sn R z s

However, it seems that we can't define Church numerals with the following type of Induction principle:

NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n)

Why is it so? How can I prove this? It seems that the problem is with defining a type for Nat which becomes recursive. Is it possible to amend lambda calculus to allow this?

Answer 1

The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background.

Given a type constructor $T : \mathsf{Type} \to \mathsf{Type}$, we might be interested in the "minimal" type $A$ satisfying $A \cong T(A)$. In terms of category theory $T$ is a functor and $A$ is the initial $T$-algebra. For example, if $T(X) = 1 + X$ then $A$ corresponds to the natural numbers. If $T(X) = 1 + X \times X$ then $A$ is the type of finite binary trees.

An idea with long history is that the initial $T$-algebra is the type $$A \mathrel{{:}{=}} \prod_{X : \mathsf{Type}} (T(X) \to X) \to X.$$ (You are using Agda notation for dependent products, but I am using a more traditional mathematical notation.) Why should this be? Well, $A$ essentially encodes the recursion principle for the initial $T$-algebra: given any $T$-algebra $Y$ with a structure morphism $f : T(Y) \to Y$, we get an algebra homomorphism $\phi : A \to Y$ by $$\phi(a) = a \, Y \, f.$$ So we see that $A$ is weakly initial for sure. For it to be initial we would have to know that $\phi$ is unique as well. This is not true without further assumptions, but the details are technical and nasty and require reading some background material. For instance, if we can show a satisfactory parametricty theorem then we win, but there are also other methods (such as massaging the definition of $A$ and assuming the $K$-axiom and function extensionality).

Let us apply the above to $T(X) = 1 + X$: $$\mathsf{Nat} = \prod_{X : \mathsf{Type}} ((1 + X) \to X) \to X = \prod_{X : \mathsf{Type}} (X \times (X \to X)) \to X = \\ \prod_{X : \mathsf{Type}} X \to (X \to X) \to X. $$ We got Church numerals! And we also understand now that we will get a recursion principle for free, because the Church numerals are the recursion principle for numbers, but we will not get induction without parametricity or a similar device.

The tehcnical answer to your question is this: there exist models of type theory in which the type SimpleNat contains exotic elements that do not correspond to numerals, and moreover, these elements break the induction principle. The type SimpleNat in these models is too big and is only a weak initial algebra.