[dbpatterson]

Have you actually done any proofs in one of these systems? (or used one?)

Natural numbers are used because of the induction principle you get: it's very useful, and generally straightforward to use in lots of contexts (e.g., just the other day I had students proving the correctness of multiplication implemented as iterated addition; the multiplication is over integers, but the inner loop is after you've ensured what you are iterating is non-negative, since you decrement each iteration, and _proving_ it is much more straightforward if you interpret the loop counter as a natural number).

And your point about syntax is also baffling: Coq will display natural numbers as decimal literals, not "S(S(S...".