Natural Numbers, Integers, and Rationals
摘要
We first construct the natural numbers, in a way that, according to Brouwer, is based on the fundamental intuition of the passage of time. This intuition justifies definition by recursion and the Principle of Complete Induction. We also illustrate the difference between effective and non-effective proofs; for example, the Least Number Principle is not constructively valid. Equality on the natural numbers is shown to be decidable; and that property extends to the integers and rational numbers, which we construct as equivalence classes. We discuss the orderings, in particular of the rational numbers.