# The ICICS/CS Reading Room

## UBC CS TR-89-07 Summary

- How Many Real Numbers Are There?, August 1989 Paul C. Gilmore
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.
\nThe 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.
\nThat 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.
\nAlthough 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.
\nFeferman 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.

If you have any questions or comments regarding this page please send mail to
help@cs.ubc.ca.