I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, Types and Programming Languages). Description of the simply-typed lambda-calculus and in particular PCF programming language are usually based on Nat's and Bool's. For the people using and teaching general-purpose industrial PL's it is great deal more natural to treat integers instead of naturals. Can you mention some good reasons why PL theorist prefer nat's? Besides that it is a little less complicated. Are there any fundamental reasons or is it just an honour the tradition?
UPD For all those comments about “fundamentality” of naturals: I'm a quite aware about all those cool things, but I'd rather prefer to see an example when it is really vital to have those properties in type theory of PL's theory. E.g. widely mentioned induction. When we have any sort of logic (which simply typed LC is), like basic first-order logic, we do really use induction — but induction on derivation tree (which we also have in lambda).
My question basically comes from people from industry, who wants to gain some fundamental theory of programming languages. They used to have integers in their programs and without concrete arguments and applications to the theory being studied (type theory in our case) why to study languages with only nat's, they feel quite disappointed.