Is the validity of induction in Coq axiomatic?

Question

When one defines an inductive type in Coq, for example, natural numbers,

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Coq automatically creates an induction principle for that type:

nat_ind : forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, P n.

The induction principle is itself a theorem. The derivation, meaning, and usage of such induction principle is clear to me.

Does this induction principle becomes an axiom in Coq, or it is a logical consequence of more fundamental principles? Can one prove the induction principle in Coq?

Answer 1

The answer is "no, Coq does not introduce an axiom", but this is not the whole story, because type theory does not operate by postulating axioms. Instead, Coq has some primitive building blocks from which the natural numbers, and other inductive types, can be built.

Let's see how it is done for induction on natural number. If you Print nat_ind. you get:

nat_ind =
fun (P : nat -> Prop) (f : P 0) (h : forall n : nat, P n -> P (S n)) =>
fix F (n : nat) : P n :=
  match n as k return (P k) with
  | 0 => f
  | S k => h k (F k)
  end
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

The fix construct is used for recursive definitions. Here is the same definition written without fix:

Fixpoint my_nat_ind (P : nat -> Prop) (b : P 0)
  (h : forall k, P k -> P (S k))
  (n : nat) : P n :=
  match n with
  | 0 => b
  | S k => h k (my_nat_ind P b h k)
  end.

We see that b is the base case, and h is the induction step. Notice that we make a recursive call to my_nat_ind in the induction step.

If we are allowed to make arbitrary recursive definitions, then we can prove False very easily:

Definition nonsense : False := nonsense.

Of course, Coq disallows this. When you make a recursive definition, it verifies that all recursive calls will actually terminate. In the case of my_nat_ind it can tell that the fourth argument n has one fewer constructors S applied in the recursive call, so it allows it. This is known as "guardedness condition".

In summary, Coq does not postulate any new axioms when you define nat. Instead, it defines induction using guarded recursion.

---

Let me also explain why you want to be careful with the word "axiom" when you speak to type theorists. In type theory, an axiom is the same thing as a constant c of a type A. For example, one might postulate excluded middle as an axiom by introducing a new constant $$\textstyle \mathtt{lem} : \Pi_{p : \mathtt{Prop}}.\, p \lor \neg p $$ This approach does not work well, because it messes up the nice computational properties of type theory. When $\mathtt{lem}$ appears in the middle of some term, the engine won't know how to compute with it.

Answer 2

You could say that induction is a logical consequence of the fact that the inhabitants of an inductive type are fully defined by the list of the constructors. It would be better to say that the induction principle is a way to specify that you want the inhabitants of the inductive type being defined to be fully specified by its constructors.

Coq is not there to add an axiom behind your back, it is just there to help you write the induction principle that you really need to complete your definition.

This is not specific to Coq, this comes with any type theory featuring inductive types. The induction principle cannot be proved within the theory, because it is part of the definition of the inductive type: you are free to define a type with a list of constructors, and not add the induction principle: that's ok, just it is not an inductive type !

Finally you need to be a bit careful by the meaning of "the inhabitants of an inductive type are fully defined by the list of its constructors". That means that they are freely generated by the list of constructors within the context of the theory, where the context may play a significant role in the story. See for instance Andrej Bauer's note about it.