3 ms·
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
by gugagore 1y ago
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.
- 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.