# What untyped term inhabits induction on natural numbers in CoC?

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions.

If we assumed indNat as an axiom, is there an untyped term that would have the semantics of the induction function? What if we had Scott-encoded natural numbers and fix?

Can induction be inhabited in CoC + fix (such that the function would have the proper semantics, not an infinite loop)?

• What type would you give to fix? – cody Jul 9 at 15:30
• fix : (t : *) -> (t -> t) -> t – Labbekak Jul 10 at 12:12
• The indNat would have the same erasure as the recnat right? – user833970 Sep 9 at 17:53
• I think so yes (if you mean iteration on nats with recnat) – Labbekak Sep 9 at 20:11

If you have $$fix$$ you can definitely implement induction principles, using structural recursion on the natural number. This is how they do it in CiC and Coq, with an extra restriction that the recursive calls must be on a structurally smaller value. Without this condition, you can write induction, but you also can write nonterminating terms with the same type as an induction principle.
• I'm not convinced about that second comment about fix: in Coq they add a fixpoint for dependent types, not the one Labbekak seems to have in mind. I'm not sure the non-dependent one is sufficient. – cody Jul 10 at 15:32
• However, non-dependent fix + dependent match for naturals seems to be sufficient, so now I'm not sure... – cody Jul 10 at 15:45