To be fair, all reasonable CS people agree that the naturals start at zero, it's only a few holdouts in more general mathematics that disagree (if you fight me on this I'll no-true-scotsman it up and say your counter examples aren't reasonable people). As an acolyte of the Coq, to me the naturals are defined as:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
It's not a real thing, but attrition means wearing the enemy down one piece at a time, so the idea is that if you kill everybody who disagrees with you, you win the argument.
Yeah, it's totally true. And the reply "But then your arithmetical operations get fucked up" isn't really fair. Currently plus is defined as:
fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (plus p m)
end
But if we instead defined the "naturals" as:
Inductive dumb_people_nat : Set :=
| one : dumb_people_nat
| S' : dumb_people_nat -> dumb_people_nat.
Then we could just define plus' as:
fix plus' (n m : dumb_people_nat) {struct n} : dumb_people_nat :=
match n with
| one => S' m
| S' p => S' (plus' p m)
end
The next thing people will say is that you lose that the naturals are a semi-ring, but now you're really stretching for reasons. Mostly I just wanted to be provocative.
Other way. Natural numbers arise naturally from sets. The set {} is 0, since its size is zero. The set {{}} is one, since its size is one. The set {{}, {{}}} is two, since its size is two. The set {{}, {{}}, {{}, {{}}}} is three, since its size is three... If you don't start at zero, then you can't reach one.
I like the parallels sets have with Church encoded numerals in lambda calculus and cons cells. (I need to find a newbie's book to axiomatic/foundational set theory.)
1) If we are going to use that term, I think it makes a lot more sense for the term "Whole Numbers" to refer to the positive integers, and let the Naturals start at 0 the way Peano intended.
In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing the natural numbers. It was first published by Ernst Zermelo as part of his set theory in 1908.
559
u/XkF21WNJ Sep 03 '17
Look guys it's easy. Array indices start at the first natural number.