3 ms·

Type theories like the one of coq support inductive definitions. Inductive nat: Set := | O: nat | S: nat -> nat However, this feels a bit like hav

• enriquto 7y ago
  > An alternative would be to basically do the same as is usual in set theory. That is, have an axiom that states that an infinte set exists. (...) I was not aware of this construction, thanks! The only thing I knew is the construction of natural numbers from the empty set, by iteratively building singletons.
  • jfarmer 7y ago
    The axiom of infinity ("there exists an infinite set") is what gives you permission to carry out the construction you describe. The usual construction of the naturals via set theory has us define... 1. 0 as the empty set ∅ 2. succ(n) as n ∪ {n} So you get... 0 := ∅ 1 := {0} = {∅} 2 := {0, 1} = {∅, {∅}} 3 := {0,1,2} = {∅, {∅}, {∅, {∅}}} 4 := {0,1,2,3} = {∅, {∅}, {∅, {∅}}, {∅, {∅}, {∅, {∅}}}} ... etc. ... But how do we know the following? 1. The empty set ∅ is a set 2. If T is a set then {T} is also a set 3. If T is a set then T ∪ {T} is a set 4. There exists a set X such that ∅ is in X and T ∪ {T} is in X whenever T is in X These all follow from the axioms of ZFC and (4) is actually itself one of the axioms — the Axiom of Infinity. It says that an infinite set like X exists. But you can see that the essence of it is just: "There exists a set X which includes the natural numbers." Note that this set X might contain many things beyond the set-theoretic copy of the natural numbers — the axiom just guarantees that a set containing the natural numbers exists ("some infinite set"). You can then use some of the other axioms to remove the unwanted elements, creating the unique, smallest set that satisfies this property. In other words, the axioms of ZFC were designed to be Peano-friendly. It wasn't as if we arrived at ZFC and then said, "Oh, look at that, we can represent the natural numbers as sets. What a surprise!":D
• 0815test 7y ago
  Actually, that `Inductive nat` is precisely a natural number object in terms of categorial semantics - it's worth mentioning that NNO's in categorial semantics are unique up to isomorphism. That "Inductive" syntax in Coq is actually a key part of the system, it's involved in defining things as basic as equality and product- or sum-types. This is quite different from how things would be done in a "standard" set theory.
  • pwm 7y ago
    But is equality a basic thing to define? :)
• pron 7y ago
  > That is, have an axiom that states that an infinte set exists. Type theories do have that axiom. It takes the form of the axiom that postulates the existence of inductive types of the kind you've shown.
• cjfd 7y ago
  Seeing these comments let me remark that the problem that I have with inductive definitions is that one could have the expectation that the foundations of mathematics would be a rather small and simple set of rules from which the rest can be derived. When one introduces inductive definitions as is done in coq this principle is out of the window. The branches of an inductive must satisfy a 'positivity condition' that is quite complicated. Then there is the thing that one can also do mutually recursive inductive definions. Then there are more rules for what kind of match statements are allowed. And let us not even get started on CoInductive definitions. IIRC Freek Wiedijk described the foundations as they are in coq as 'beyond baroque' and that is quite to the point.
  • lmm 7y ago
    ZFC includes an infinite axiom schema, so it's not really elegant and simple in that way either.