Hacker News Reader

I was talking to someone about inductive data types, and showed them the zero/succ definition of `Nat`, e.g. in Lean or Rocq.

It was interesting because they were asking "is this all you need? What about the Peano axioms? Is there anything more primitive than the inductive data type?"

I bring it up because it's good not to take for granted that the Peano axioms are inherent, instead of just one design among many.

View on HN

> Is there anything more primitive than the inductive data type?

I believe that the natural numbers are more primitive than inductive data types, since all inductive data types may be constructed from the natural numbers alongside a small number of primitive type formers (e.g. Π, Σ, = and Ω).

You don't need all the natural numbers for that, though. I think you need 0 and 1 only?

I think there are two primitive sets for dependent type theory. The one with omega, and then the one with inductive types. None of them need axioms like the Peano axioms.

You need some source of infinite-ness, otherwise the entire theory can be modelled by finite sets. It can be provided by the natural numbers or W types or inductive types, but the naturals are arguably the most fundamental of the three.

Reply on news.ycombinator.com