[FOM] real numbers

[Andreas Blass]

	Some time ago (May 3), Richard Heck asked what modality is
involved when one says that the real numbers *can* be Dedekind cuts and
*can* be equivalence classes of Cauchy sequences, when one is unwilling to
say that they *are* either of these things.  As an occasional user of this
modality, I'd like to try to explain what I mean by it.  The explanation
is related to some previous postings, particularly ones by Harvey Friedman
and Matt Insall, but I think it's sufficiently different to deserve an
explicit statement.  I believe that it describes what many mathematicians
believe --- or would believe if they ever thought about such foundational
matters.
	Mathematicians generally reason in a theory T which (up to
possible minor variations between individual mathematicians) can be
described as follows.  It is a many-sorted first-order theory.  The sorts
include numbers (natural, real, complex), sets, ordered pairs and other
tuples, functions, manifolds, projective spaces, Hilbert spaces, and
whatnot.  There are axioms asserting the basic properties of these and the
relations between them.  For example, there are axioms saying that the
real numbers form a complete ordered field, that any formula determines
the set of those reals that satisfy it (and similarly with other sorts in
place of the reals), that two tuples are equal iff they have the same
length and equal components in all positions, etc.
	There are no axioms that attempt to reduce one sort to another.
In particular, nothing says that real numbers are sets of any kind.
(Different mathematicians may disagree as to whether, say, the real
numbers are a subset of the complex ones or whether they are a separate
sort with a canonical embedding into the complex numbers. Such issues will
not affect the general idea that I'm trying to explain.)  So
mathematicians usually do not say that the reals are Dedekind cuts (or any
other kind of sets), unless they're teaching a course in foundations and
therefore feel compelled (by outside forces?) to say such things.
	This theory T, large and unwieldy though it is, can be interpreted
in far simpler-looking theories.  ZFC, with its single sort and single
primitive predicate, is the main example of such a simpler theory.  (I've
left large categories out of T in order to make this literally true, but
Feferman has shown how to interpret most of category theory, including
large categories, in a conservative extension of ZFC.)  For most
mathematicians, type theory will also serve to provide an interpretation
of T, and there may be other, equally good possibilities.
	There are, of course, several choices to be made in constructing
an interpretation of T in ZFC.  The one immediately relevant to the topic
at hand is the choice between Dedekind cuts and equivalence classes of
Cauchy sequences to represent reals.  But there are also choices in
representing ordered pairs by sets, representing functions by sets of
ordered pairs. (Do you use pairs (input, output) or (output, input)?  Most
of us use the former, but there are serious authors who preferred the
latter.)  So there are many interpretations of T --- interpretations into
different theories, and even different interpretations into the same
theory.
	After this long introduction, I can finally explain "can".  When I
say that something, like "the real numbers are Dedekind cuts", can be
true, I mean that it becomes true under such an interpretation.
(Usually, I mean also that I know and even somehow approve of such an
interpretation, but I don't think that's essential.)  So the familiar
interpretations show that the real numbers can indeed be Dedekind cuts and
that they can be equivalence classes of Cauchy sequences.
	This view is, from a technical point of view, not too far from
Kripke-style semantics of modal operators.  In that semantics, there are
possible worlds and an accessibility relation between them; something
*can* be true in one world iff it *is* true in a world accessible from
that one.  In place of worlds, I have theories; in place of accessibility,
I have interpretations.  Something *can* be true in one theory (like T, in
which I claim mathematicians really work) iff it *is* true, after
interpretation in another theory (like ZFC).
	A difference betwen this situation and Kripke semantics is that
there may be, as I indicated above, several interpretations from one
theory to another.  So instead of dealing with Kripke structures of the
familiar sort, over a set (of worlds) with a binary relation (of
accessibility, often a partial order), we have a Kripke structure over a
category (of theories) whose morphisms are the interpretations.  But such
generalized Kripke structures have been thoroughly studied; they
constitute the presehaf semantics for intuitionistic logic.  So I claim
that I am not introducing anything weird here.  (My comment earlier about
knowng and approving of interpretations suggests that one might want to
restrict to some subcategory of "reasonable" theories and interpretations,
so as to really avoid introducing anything weird.)

Andreas Blass