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

Question

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?

Answer 1

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.