FOM: Conway's foundational ideas

[Stephen G Simpson]

Thomas Forster 22 May 1999 10:31:07

 > contributions the fainting violets could have made don't get made,
 > and we are all the poorer for it. ...

Does anyone else have evidence that the ``fainting violet'' phenomenon
has detracted from the scientific level of the FOM list?  I certainly
don't want to cause FOM to be impoverished in this way.

How can FOM solve this problem?  Perhaps we need to institute a
two-tier system.  The fainting violets would be called upon to label
themselves as fainting violets and refrain from any disturbing
remarks.  After that, the rest of us would make it a point to exempt
the fainting violets from the rough-and-tumble.  What do you think of
this two-tier idea?

:-)

In any case, some personal acquaintances of John H. Conway, including
Walter Felscher (posting of 6 May 1999 11:16:12) and Harvey Friedman
(offline discussion), have told me that Conway has a serious,
long-term interest in foundational issues, even if his approach is
brash and unorthodox.  Moreover, while Conway may want to position
himself as a 1960's-style revolutionary, he is also a prominent and
influential Establishment mathematician.  Furthermore, he has not
deliberately injected himself into the FOM discussion.  These may be
reasons for treating Conway with special deference.

Therefore, I hereby apologize for and retract all of my earlier
Conway-baiting remarks.  Let me turn instead to a sober, restrained
discussion of Conway's foundational ideas as expounded on pages 64-67
of ``On Numbers and Games''.  I reserve for possible future FOM
postings the difficult question of how the f.o.m. community can best
cope with the Conway phenomenon and similar phenomena.

Note: I am not aware of any foundational writings of Conway other than
the brief foundational remarks in ``On Numbers and Games''.  If Conway
and his followers have subsequently modified or amplified his
foundational ideas, I would be grateful for any leads or references.

Note: Some FOM subscribers, e.g. Gonzalez Cabillon 20 May 1999
02:39:52, may regard this as ``a storm in a teacup''.  I disagree,
because Conway is a highly respected and influential Establishment
mathematician.  He has a huge following.  Some people have even
described him as the leader of a cult within the mathematical
community!  For this reason, it seems to me that we
f.o.m. professionals need to take Conway's foundational ideas very
seriously indeed.  We would need to do this even if Conway's ideas
were poorly expressed and had no scientific merit, simply because of
who Conway is.

So, let me get on with it.

Here is what I regard as the main foundational passage from Conway's
book ``On Numbers and Games''.  I reproduce it in full, because I
don't want Pais and Gonzalez Cabillon to accuse me of leaving anything
out.  My detailed comments are below.

  The curiously complicated nature of these constructions tells us
  more about the nature of formalisations within ZF than about our
  system of numbers, and it is partly for this reason that we did not
  present any such formalised theory in this book.  But the main
  reason was that we regard it as almost self-evident that our theory
  is as consistent as ZF, and that formalisation in ZF destroys a lot
  of its symmetry.  Plainly the proper set theory in which to perform
  a formalisation would be one with two kinds of membership, and would
  in fact be very like the abstract theory of games that underlies the
  next part of this book.

  It seems to us, however, that mathematics has now reached the stage
  where formalisation within some particular axiomatic set theory is
  irrelevant, even for foundational studies.  It should be possible to
  specify conditions on a mathematical theory which would suffice for
  embeddability within ZF (supplemented by additional axioms of
  infinity if necessary) but which do not otherwise restrict the
  possible constructions in that theory.  Of course the conditions
  would apply to ZF itself, and to other possible theories that have
  been proposed as suitable foundations for mathematics (certain
  theories of categories, etc.), but would not restrict us to any
  particular theory.  This appendix is in fact a cry for a
  Mathematicians' Liberation Movement!

  Among the permissible kinds of construction we should have:
  (i) Objects may created from earlier objects in any reasonably
  constructive fashion.
  (ii) Equality among the created objects can be any desired
  equivalence relation.
  
  In particular, set theory would be such a theory, sets being
  constructed from earlier ones by processes corresponding to the
  usual axioms, and the equality relation being that of having the
  same members.  But we could also, for instance, freely create a new
  object (x,y) and call it the ordered pair of x and y.  We could also
  create an ordered pair [x,y] different from (x,y) but co-existing
  with it, and neither of these need have any relation to the set
  {{x},{x,y}}.  If instead we wanted to make (x,y) into an unordered
  pair, we could define equality by means of the equivalence relation
  (x,y) = (z,t) if and only if x=z,y=t *or* x=t,y=z.

  I hope it is clear that this proposal is not of any particular
  theory as an alternative to ZF (such as a theory of categories, or
  of numbers or games considered in this book).  What is proposed is
  instead that we give ourselves the freedom to create arbitrary
  mathematical theories of these kinds, but prove a metatheorem which
  ensures once and for all that any such theory could be formalized in
  terms of any of the foundational theories.

  The situation is analogous to the theory of vector spaces.  Once
  upon a time these were collections of n-tuples of numbers, and the
  interesting theorems were those that remained invariant under linear
  transformations of these numbers.  Now even the initial definitions
  are invariant, and vector spaces are defined by axioms rather than
  as particular objects.  However, it is proved that every vector
  space has a base, so that the new theory is much the same as the
  old.  But now no particular base is distinguished, and usially
  arguments which use particular bases are cumbrous and inelegant
  compared to arguments directly in terms of the axioms.

  We believe that mathematics itself can be founded in an invariant
  way, which would be equivalent to, but would not involve,
  formalisation within some theory like ZF.  No particular axiomatic
  theory like ZF would be needed, and indeed attempts to force
  arbitrary theories into a single formal strait-jacket will probably
  continue to produce unnecessarily cumbrous and inelegant
  contortions.

  For those who doubt the possibility of such a programme, it might be
  worthwhile to note that certainly principles (i) and (ii) of our
  Mathematicians' Lib movement can be expressed directly in terms of
  the predicate calculus without any mention of sets (for instance),
  and it can be shown that any theory satisfying the corresponding
  restrictions can be formalised in ZF together with sufficiently many
  axioms of infinity.

  Finally, we note that we have adopted the modern habit of
  identifying ZF (which properly has only sets) with the
  equiconsistent theory NBG (which has proper Classes as well) in this
  appendix and elsewhere.  The classification of objects as Big and
  small is not peculiar to this theory, but appears in many
  foundational theories, and also in our formalised versions of
  principles (i) and (ii).

Now for my detailed analysis of Conway's remarks.

 > we regard it as almost self-evident that our theory is as
 > consistent as ZF

This is correct if we interpret ``as consistent as ZF'' in terms of
consistency strength.  Actually, much more is true: The theory of the
No(kappa)'s (i.e. surreal numbers that are hereditarily of size less
than or equal to kappa), for all infinite cardinal numbers kappa, is
straightforwardly formalizable in ZFC.  (Actually it is formalizable
in ZC, Zermelo set theory with the axiom of choice.)  If in addition
we consider the proper class No of *all* surreal numbers, then
Conway's theory is straightforwardly formalizable in the closely
related VNBG, perhaps with global choice.  In short, the theory of
surreal numbers presents no special difficulties with respect to
formalization in the usual ZC/ZFC/VNBG-style foundational setup.

 > and that formalisation in ZF destroys a lot of its symmetry.

Why does Conway complain about ``destroying symmetry''?  It seems to
me that this kind of attack on formalization is unjustified.  Whatever
symmetry exists before formalization still exists afterward, and it
may then be brought out in a more precise way.  

For example, the corollaries derived in my posting of 21 May 1999
19:59:44 concerning surreal numbers bring out some symmetries
(automorphisms) in the surreal numbers that Conway's non-ZFC approach
apparently overlooked.  My posting was of course based on the obvious
ZFC formalization of the surreal numbers (see above) and consequent
applicability of general model-theoretic results which are also
formalized within ZFC.  Thus, in this instance, formalization with ZFC
*contributed* to the elucidation of certain symmetries.  It did not
detract from or destroy any symmetries.

Moreover, the Conway complaint about ``destroying symmetry'' seems to
have lost sight of the f.o.m. purpose of set-theoretic foundations.
The purpose of formalizing the surreal numbers in ZFC is foundational,
not mathematical.  Part of the purpose is to show that the surreals
are consistent with the bulk of mathematics, which is already known to
be formalizable in ZFC.  I think this is worth knowing.  What do
Conway and his followers think?

 > Plainly the proper set theory in which to perform a formalisation
 > would be one with two kinds of membership, ...

OK.  Contrary to what I may have said before, Conway *is* proposing an
alternative set-theoretic f.o.m., one with two membership predicates.
The first question that comes to my mind is, what would be the effect
of this alternative f.o.m. on the symmetry of mathematical topics that
do *not* make any particular use of Conway's left/right membership
distinction?  Would we be required to choose one of the two?  Would we
choose the left one or the right one? 

Conway's ideas seem to present us with a nearly intolerable dilemma.
On the one hand, we need to take Conway's foundational ideas very
seriously, because Conway is a respected and influential Establishment
mathematician.  On the other hand, if we were to take this particular
idea seriously, then every major branch of mathematics or minor topic
within mathematics would be called upon to set up its own tailor-made
foundation in terms of its own variant of set theory.  There would be
a special set-theoretic foundation for infinite group theory, another
for finite group theory, another for real analysis, another for
complex analysis, etc etc.

Clearly this idea of pluralistic set-theoretic foundations would tend
to divide mathematics into mutual incompatible foundational camps.
Wouldn't it be much more sensible to agree on a common foundation for
*all* of mathematics, or as much of it as possible?  I think it would.
Obviously a common foundation would tend to promote the unity of
mathematics.  Can Conway and his followers agree that this is a
desirable goal?  Furthermore, if the common foundation were chosen
intelligently, then it might even contribute to a better understanding
of the place of mathematics within human knowledge as a whole.  I view
this kind of understanding as part of the mission of f.o.m.

Perhaps Conway or some of his followers would care to explain why they
think that some mathematical theories (e.g. Conway's theory of surreal
numbers) require a specialized set-theoretical foundation, while
apparently others (e.g. group theory? real analysis?) can get along
with the general ZFC-style foundation.  Do they think there is a
serious f.o.m. distinction to be drawn here?  If so, what is the
distinction?

So far as I know, there is no serious distinction here.  It seems to
me that surreal numbers are just like any other mathematical topic,
with respect to formalizability in ZFC.  Do Conway and his followers
dispute this?

 > mathematics has now reached the stage where formalisation within
 > some particular axiomatic set theory is irrelevant

My impression from this passage is that Conway seems to be attacking
the entire idea of formalization within foundational axiomatic
theories as such.  Is this impression correct?

In any case, I would note that formalization of particular
mathematical topics within particular foundational theories is *not*
irrelevant.  Indeed, formalization often contributes to (i) improved
mathematical understanding of the particular mathematical topic in
question and its connections to other mathematical topics, e.g. my
remarks on connections between surreal numbers and model theory, as
above and in my posting of 21 May 1999 19:59:44, (ii) improved
foundational understanding, e.g. the program of reverse mathematics,
as in my new book ``Subsystems of Second Order Arithmetic''
<http://www.math.psu.edu/simpson/sosoa/>.

 > mathematics has now reached the stage where formalisation within
 > some particular axiomatic set theory is irrelevant, even for
 > foundational studies.

The conventional wisdom among f.o.m. professionals is that
formalization within particular foundational axiomatic theories is of
the essence in foundational studies, and will remain so for the
forseeable future.  This insight has been of key importance for modern
f.o.m. research.  But apparently Conway wishes to oppose this
conventional f.o.m. wisdom.  If so, then I think he needs to explain
himself more fully.

Have Conway or his followers published some sort of amplification of
Conway's anti-formalization views?  I am curious to know how Conway
and his followers think f.o.m. can get along without formalization.

 > It should be possible to specify conditions on a mathematical
 > theory which would suffice for embeddability within ZF
 > (supplemented by additional axioms of infinity if necessary)

I am not sure what sort of embeddability or what sort of sufficient
conditions Conway has in mind here.  Can anyone clarify this?  My
specific question for Conway and his followers would be: Do you
recognize the usefulness of the conventional f.o.m. notion of
``definitional extension of a theory'', as explained in mathematical
logic textbooks?  Do you think that this notion may have any relevance
to what you have in mind?  It seems to me that, properly understood
and applied, this well known f.o.m. notion may completely dispose of
the concerns that are troubling you.

 > other possible theories that have been proposed as suitable
 > foundations for mathematics (certain theories of categories, etc.),

Here it seems that Conway is alluding to the Lawvere/MacLane idea of
``categorical foundations'', which has been called into question both
in the printed category-theoretic literature and here on the FOM list.
How much is Conway committed to this discredited idea, and what is its
relevance here?  The commitment seems to be more than just casual,
because both Conway and the topos theorist Johnstone attack
set-theoretic foundations and refer to each other.

 > This appendix is in fact a cry for a Mathematicians' Liberation
 > Movement!

Again, we need to take this very seriously, because Conway is a
respected and influential Establishment mathematician.  The first
question we need to ask is: What tyrannical force does Conway want
mathematicians to liberate themselves from?  Is it formalization?  Why
does Conway apparently think that formalization is a kind of tyranny?

In the US Declaration of Independence, Thomas Jefferson called for
liberation from another kind of tyranny.  This call was accompanied by
a detailed list of the English king's particular offenses against the
rights of man.  Unfortunately, Conway does not seem to want to go to
the trouble of drawing up a similarly detailed expose of the alleged
bad consequences of formalization.  Such a list would be very useful
for those of us who take Conway seriously and want to understand his
foundational ideas.

 > Among the permissible kinds of construction we should have:
 > 
 > (i) Objects may created from earlier objects in any reasonably
 > constructive fashion.

If we are to take Conway's foundational ideas seriously, then we need
to ask: What theory of ``construction'' or ``constructiveness'' is
Conway referring to here?  

Or is Conway's point simply that he doesn't want anybody to look over
his shoulder?  The latter would of course be an understandable human
emotion, but I don't think it would constitute a significant
f.o.m. advance.

 > (ii) Equality among the created objects can be any desired
 > equivalence relation.

In the familiar f.o.m. theory of definitional extensions, introduction
of new sorts of objects with an accompanying new relation of equality
is permissible, in fact an integral part of the method.  Is Conway
aware of this?  If so, then why does Conway apparently think that the
familiar method of definitional extensions is inadequate for what he
wants to do?

On the other hand, Conway's specific proposal *may* be highly unusual,
because the familiar predicate calculus axioms for the equality
predicate (=) consist of not only the axioms for an equivalence
relation but also axioms of congruence for other predicates.  In other
words, one often assumes congruence axioms such as ``if x = y then Px
if and only if Py''.  Is Conway now proposing to drop the congruence
axioms?  If so, then this would be a new twist indeed.

For example, in connection with Conway's discussion of ordered pairs,
does Conway want to drop the axiom ``if (x,y) is an element of z and
(x,y) = (u,v) then (u,v) is an element of z''?  If so, has Conway done
the necessary spade work to make sure that the absence of this
assumption will not cause unexpected difficulties?
  
  What is proposed is instead that we give ourselves the freedom to
  create arbitrary mathematical theories of these kinds, but prove a
  metatheorem which ensures once and for all that any such theory
  could be formalized in terms of any of the foundational theories.

What kind of metatheorem Conway is asking for here?  What sort of
hypotheses would it have?  Have Conway and his followers ever taken
the trouble to spell this out with adequate precision?

  We believe that mathematics itself can be founded in an invariant
  way, which would be equivalent to, but would not involve,
  formalisation within some theory like ZF.  No particular axiomatic
  theory like ZF would be needed

Again, have Conway and his followers ever taken the time to spell this
program out, so that we benighted f.o.m. pedants might have a chance
of understanding what in the world Conway is talking about?

  attempts to force arbitrary theories into a single formal
  strait-jacket will probably continue to produce unnecessarily
  cumbrous and inelegant contortions.

In the absence of additional explanation, I am having a hard time
distinguishing Conway's remark here from f.o.m.-bashing of the type
that is familiar from the writings of quasi-empiricists such as Reuben
Hersh.  Still, I think Conway must have some more substantial thought
in mind, because Conway's understanding of at least some foundational
issues (e.g. transfinite induction) appears to be better than that of
the quasi-empiricists.

I wish Conway or his followers would explain themselves.  What
alternative to formalization do they envision?

  certainly principles (i) and (ii) of our Mathematicians' Lib
  movement can be expressed directly in terms of the predicate
  calculus without any mention of sets (for instance),

Is Conway referring to the well known theory of definitional
extensions in the predicate calculus?  Some variant of it?

  and it can be shown that any theory satisfying the corresponding
  restrictions can be formalised in ZF together with sufficiently many
  axioms of infinity.

Could Conway or his followers please provide a precise statement of
the metatheorem which Conway appears to be claiming?  A precise
statement may help to clear up a lot of issues, both for Conway and
his followers, and for f.o.m. professionals.

  The classification of objects as Big and small is not peculiar to
  this theory, but appears in many foundational theories, ...

What foundational theories?  So far as I know, the only theories where
the big/small distinction plays a significant role are set theory
(sets versus proper classes) and category theory (small categories
versus large categories).  And set theory is a foundational theory,
but category theory is not.

I think this passage is further evidence that Conway may have bought
into the discredited idea of ``categorical foundations''.

Referring to Conway, Walter Felscher said

 > From personal acquaintance, I can assure you that he is not
 > prejudiced against foundational issues; it just happens that he is
 > not interested in pursuing them with the logician's machinery.

Has Conway ever explained his non-logical ideas more fully in a
published or public forum?  I would welcome this, because it would
allow f.o.m. professionals and others to subject Conway's non-logical
foundational ideas to rational examination.

I repeat that, even before we know what Conway's non-logical
foundational ideas are, we need to take them very seriously, because
Conway is a highly respected Establishment mathematician.

-- Steve