# Why isn't it "enough" to prove induction with one extra "INat" argument?

It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is,

Nat =
∀ P : *
∀ S : P -> P
∀ Z : P
P

Zero =
λ P : *
λ S : P -> P
λ Z : P
Z

Succ =
λ n : Nat
λ P : *
λ S : P -> P
λ Z : P
S (n P S Z)

NatInd :
∀ P : Nat -> *
∀ S : ∀ (n : Nat) -> P n -> P (Succ n)
∀ Z : P Zero
∀ n : Nat
P n


There is no term of type NatInd on CoC, for either this or any other representation of Nat. But I've noticed that the following slightly different type can be constructed:

INat =
λ n : Nat
∀ P : Nat -> *
∀ S : ∀ (n : Nat) -> P n -> P (S n)
∀ Z : P Zero
P n

NatInd2 :
∀ P : Nat -> *
∀ S : ∀ (n : Nat) -> P n -> P (Succ n)
∀ Z : P Zero
∀ n : Nat
∀ i : INat n
P n


Here, we first define a new type, INat : Nat -> *. That type is isomorphic to Nats and can be easily constructed for any natural number. Then, NatInd2 is a term that, given a proposition indexed on Nats, a base case Z, a step case S, for any nat n and its corresponding INat n, proves P(n) holds for every n. Or, in simpler words, NatInd2 is essentially induction, except that you must provide an additional argument i of type INat n, which you can always construct anyway. You could as well use dependent pairs to conveniently store Nat, INat pairs together.

It seems like this accomplishes the same one would expect from induction, i.e., you prove all cases from a base and a step case. Of course, there is an extra argument, but that argument is trivial to construct. For a "human reader", any proof using the method above would be equally convincing that some property holds for all n. So, my question is: is there any reason for the above method to be insufficient in general? Why is it so important to have the former unaltered definition of NatInd?

• You have the type Nat which only has recursion, but not induction (i.e. the type of the result can't depend on the input). Then you build Nat2 (named INat) which allows you to have some kind of weak induction: if you give a Nat2 as input, then the type of the output can depend on a Nat. Aug 9 '18 at 13:19
• @xavierm02 yes, I think that's more or less what I did. My question is pretty much "why that is not enough", perhaps in a philosophical sense? Because as I understand, an inductive proof using NatInd2 would be equally "truthful" as an inductive proof using NatInt. Aug 9 '18 at 13:25
• My intuition is that: (1) You will need to define Nat3, Nat4 etc. to do some things. (2) There may be (very weird convoluted?) things for which no Natn would work. (3) You may be interested in the trick to get induction from recursion plus induction for the equality type. Aug 9 '18 at 13:30
• The trick was something like this: (1) Change the domain to $\Sigma_{n:\mathbb N}P n$ to make it non-dependent. (2) Use the recursion principle to build a term $t$ of type $\forall P : \mathbb N \to Type, \forall z : P Z, \forall s : (\forall n : \mathbb N, P n \to P (S n)), \forall n, \Sigma_{n:\mathbb N}P n$ (3) Define the induction principle as the first projection of the previous term. This term has type $\forall P : \mathbb N \to Type, \forall z : P Z, \forall s : (\forall n : \mathbb N, P n \to P (S n)), \forall n, P (\pi_1 (t n))$ where $\pi_1$ is the first projection. Aug 9 '18 at 17:24
• I think that this describes a way to achieve what you're trying to do: Impredicative Encodings of Inductive Types in HoTT. Aug 9 '18 at 17:29

Let us spell out the informal meaning of INat, IntNat and IndNat2. Suppose we have a predicate P on natural numbers. Say that P is inductive if we can inhabit P Zero and ∀ k . P k -> P (Succ k). Then we have:

• NatInd P states "if P is inductive then, for all j : Nat, we have P j"
• INat n P states "if P is inductive then P n"
• NatInd2 P states: "if P is inductive and for every n we have an i which allows us to inhabit inductive predicates at n, then we can inhabit P n".

As you can see, NatInd2 just sweeps the problem under the rug, because it essentially asks that we give it a way of implementing induction. It is true that we can inhabit INat Zero, INat (Succ Zero), INat (Succ (Succ Zero)), ... but that does not imply that we can inhabit ∀ k . INat k! If you think otherwise, provide a term that does so.

In essence, you just hid the problem a little deeper by introducing a level of indirection. You could have already asked this: I can inhabit an infinite sequence of types NatInd P S Z Zero, NatInd P S Z (Succ Zero), NatInt P S Z (Succ (Succ Zero)), ... – why is this not sufficient to have induction? The answer: because you are suposed to inhabit ∀ n : Nat, NatInd P S Z n, which is not the same thing! The former is truth at the meta-level and the latter is an internal induction principle inside the calculus.

The question revolves around the difference between having an infinite sequence of terms inhabiting

t0 : Q 0
t1 : Q 1
t2 : Q 2
t3 : Q 3
...


versus having a single term

t : ∀ n : Nat, Q n


Given t, we can of course produce t0, t1, t2, etc. But there is generally no way to produce a t if we know that we have the infinite sequence of terms t0, t1, t2, ..., even in the case when there is an algorithm generating the sequence, for such an algorithm may not be expressible in the language (CiC in our case). Is that clear?

In fact, we can show that, given any (sufficiently expressive) strongly normalizing calculus (and a total language in general), there will be an instance of Q : Nat -> * such that we can inhabit each of Q 0, Q 1, Q 2, ... separately, but not ∀ n : Nat, Q n. This just says that no strongly normalizing calculus can express all total computable functions.

Supplemental: The OP is aksing why one needs, ought, or should internalize universal quantifiers. From a programmer's point of view the answer is simply that this is what is needed. Let us consider the practical difference between having an infinite sequence of terms

t0 : P 0
t1 : P 1
t2 : P 2
...


versus a single term

u : ∀ n : Nat, P n


Suppose you want to write a program which reads from the standard input a natural number k and outputs a witness of the statement P k. If we have u then we can do it easily (I am inventing syntax as I go here):

print "Please enter a natural number" ;
let k = input() in
print (u k)


How could we write such a program if instead of u we had a sequence of terms t0, t1, t2, as above? One could attempt something like

print "Please enter a natural number" ;
let k = input() in
if k = 0 then print t0
else if k = 1 then print t1
else if k = 2 then print t2
...


but this will not do because programs cannot be infinite. One could also try to do it as follows, assuming there is an algorithm A which produces the sequence t0, t1, t2 (but this algorithm is not expressible in our programming language):

1. The programmer asks the user to tell him a natural number.
2. The user provides a natural number k.
3. The programer runs A to get the expression tk of type P k.
4. The programer writes down the program print (u tk) and runs it.

We can see quite plainly that the programmer is now doing the job of the program, i.e., everything has moved to the meta-level, which is not what we want. We want the machines to do the job for us. You could also use a programming language which can express the algorithm A, but then you've switched to a different programming language and your algorithm A will correspond to the original program u.

The program u is needed because we must be able to compose and combine it with other pieces of code where it is not known in advance how u will be used.

We can also take the logical point of view. What is the difference between having at our disposal an infinite sequence of proofs

t0 : P 0
t1 : P 1
t2 : P 2
...


versus a single proof

u : ∀ n : Nat, P n


When we inspect u and verify that it is valid, we have provided evidence that P holds for all numbers. In contrast, the sequence of proofs t0, t1, t2, ... is not a finite amount of information, and so it cannot be verified and validated in finite time. Such infinite amount of information does not provide evidence that P holds for all numbers, at least not according to the standard that evidence in mathematics means proof. A proof by definition is finite and verifiable.

You may try to save the day by saying something like "but if we verify the algorithm that produces the sequence t0, t1, t2, ... then we will know that P holds for all n". This is true, but again, you're switching to the meta-level in which the verification that the algorithm works corresponds to having the proof u.

• I'm very sorry but I don't think that covers my doubt. I understand "that does not imply that we can inhabit ∀ k . INat k" but don't understand why you should, nor why "you are suposed to inhabit ∀ n : Nat, NatInd P S Z n". I understand that there is not an algorithm on the language capable of producing t0, t1, t2 given a n : Nat, but I don't understand why, in practice, you need that. What I see is that, anytime you'd use NatInd, you need a n : Nat to get a result. Anytime you'd use NatInt2, you need a n : Nat and i : INat n. So, what (...) Aug 14 '18 at 13:21
• (...) I'm having trouble is figuring out "when", or "in what practical situation" NatInt2 wouldn't be enough, because, in the context of "programming", anytime you can provide a n to NatInt, the programmer could just provide a pair n, i to NatInt2 and get the same result. Similarly, if we take CoC as a formalization of mathematics, a proof of ∀ n : Nat . ∀ i : INat n . P n would clearly imply that P truly holds for all n - which is what we want, right? So, in the context of proving mathematical theorems, I, too, I don't understand when NatInt2 wouldn't suffice. Aug 14 '18 at 13:25
• (I meant NatInd not NatInt. And sorry for making those additional comments, but I think I should be honest when I don't understand a point, despite being given a great explanation.) Aug 14 '18 at 13:26
• Btw, ∀ n : Nat . ∀ i : INat n . P n implies ∀ n : Nat . P n because we can construct a INat n for all n, even though we can't do that inside the language (i.e., there is no proof of ∀ n : Nat -> INat n). So, perhaps the issue is that it is somehow it is considered essential to have that last bit internalized, but what I don't get is, "why"? Again, for programming, the editor could just fill the INat n. For mathematics, anyone reading ∀ n : Nat . ∀ i : INat n . P n would be equally convinced that P n holds for all n. Right? Aug 14 '18 at 13:33
• It is false that ∀ n : Nat . ∀ i : INat n . P n implies ∀ n : Nat . P n. For that to be the case, you need to provide a term of type (∀ n : Nat . ∀ i : INat n . P n) → ∀ n : Nat . P n, which you cannot do. What you are observing is that every instance can be inahbited, which is useless from a programming point of view. I supplemented my answer with an explanation of why this is so. Aug 14 '18 at 20:27