How Many Real Numbers Are There?

The question posed in the title of this paper is raised by a reexamination of Cantor's diagonal argument. Cantor used the argument in its most general form to prove that no mapping of the natural numbers into the reals could have all the reals as its range. It has subsequently been used in a more specific form to prove, for example, that the computable reals cannot be enumerated by a Turing machine. The distinction between these two forms of the argument can be expressed within a formal logic as a distinction between using the argument with a parameter F, denoting an arbitrary map from the natural numbers to the reals, and with a defined term F, representing a particular defined map. The setting for the reexamination is a natural deduction based set theory, NaDSet, presented within a Gentzen sequent calculus. The elementary and logical syntax of NaDSet, as well as its semantics, is described in the paper. The logic extends an earlier form by removing a restriction on abstraction, and by replacing first and second order quantifiers by a single quantifier. The logic remains second order, however; this is necessary to avoid an abuse of use and mention that would otherwise arise from the interpretation of atomic sentences. That there can be doubt about the number of reals is suggested by the failure of the general form of Cantor's diagonal argument in NaDSet. To provide a basis for discussion, a formalization of Godel-Bernays set theory is provided within NaDSet. The subsequent discussion reinforces Skolem's relativistic answer to the question posed. Although the general form of Cantor's argument fails in NaDSet, a rule of deduction which formalizes the argument for defined maps is derived. A simple application of the rule is provided. Feferman has argued that a type-free logic is required for the formalization of category theory since no existing logic or set theory permits self-reference of the kind required by the theory. A demonstration is provided elsewhere that category theory can be formalized within NaDSet. An elementary form of the demonstration is provided in the paper by proving a theorem suggested by $_{A}>$ for which $\oplus $ is a binary, commutative. and associative $_{A},$ is itself such a structure under cartesian product and isomorphism.