4 ms·
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 w
by gugagore 1y ago
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.
- SabrinaJewson 1y ago> 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 Ω).
- gugagore 1y agoYou 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.
- SabrinaJewson 1y agoYou 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.