From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: Report on Philosophies of Physicists
Organization: Computer Science Department,  Stanford University.
Date: Sun, 13 Sep 1992 17:47:21 GMT

In article <TORKEL.92Sep13095337@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <1992Sep13.050206.18067@CSD-NewsHost.Stanford.EDU> pratt@Sunburn.
>Stanford.EDU (Vaughan R. Pratt) writes:
>
>   >Let # denote the Goedel coding of "ZFC is inconsistent."  What I
>   >interpret you to be asking is, what reality R could possibly be
>   >described by ZFC+# under the assumption that ZFC is consistent in R?
>   >Right?
>
>  No, nothing like that. I am just wondering what anybody would mean by
>saying that ZFC+# can be used as a foundation for mathematics. A foundation
>for what? In what sense a foundation?

Well, I thought I'd answered just that, but maybe I was jumping the
gun.  The meaning of ZFC+# as a foundation for mathematics is no
different from say ZFC+V=L (all sets constructible), or any other
addition to ZFC.  It just means the same mathematics you've always
done, plus anything new you can get from this additional postulate.

You might object that # has no mathematical content.  That remains to
be seen.  The test for this is not the form of # but whether
interesting new mathematics results.  If # "goes nowhere" as they say
in foundations (I'll call this "fruitful"), ZFC+# will have proved to
be essentially ZFC, just the old foundations encumbered with some
pointless baggage (note that # is a lot of baggage, encoding not only
ZFC itself but all of proof mechanics).  But if it opens up a hot new
field with exciting results not obtainable in ZFC then your position
that # has no mathematical content becomes hard to defend.  (I owe this
insight to Sol Feferman, who expressed a mild feeling that # would go
nowhere, but that if it did yield interesting mathematics it would
reopen the question of the appropriateness of ZFC.  I would add to that
prospect the likelihood that people would then start looking for a nice
(at least shorter) rephrasing of # abstracting its real "engine".)

To make this yet more concrete, Harvey Friedman (and there may be
others I don't know about) has for a long time been investigating the
mathematical content of not-#, to see whether it is equivalent to a
nice statement (which would make # similarly nice since the class of
nice statements, whatever that is, is presumably closed under
negation).  He says that thus far he hasn't found anything really
convincing for ZFC, though he has nice stuff off to the side, at ZC+V=L
(Zermelo with Choice and Constructibility but without Fraenkel's
Replacement).

This seemingly quixotic quest is put in perspective by the celebrated
Paris-Harrington result, that the infinite Ramsey theorem is
independent of Peano Arithmetic.  This was proved by showing that it
was equivalent to (a slight strengthening of) not-# for PA, the
consistency of Peano Arithmetic.  The corresponding situation for ZFC
is that, while various nice propositions are known to be independent of
(i.e. undecided in) ZFC, none of these proofs to date have been via the
route that succeeded for Paris-Harrington in PA.  If a nice restatement
of not-# exists then one immediately obtains that this nice statement
is independent of ZFC, *via the independence of inconsistency* a la
Paris-Harrington.

It is probably wishful thinking to hope that one of not-# or # might
turn out to imply one of CH or not-CH (continuum hypothesis).

(Note in passing: relative to ZFC, we have now seen three independent
types of propositions, undecided, fruitful, and nice.  Well, almost
independent, if we restrict "fruitful" to undecided propositions.  The
nice class is closed under negation but the fruitful class is surely
not, I would even expect this to be easy to prove for a suitably
general class of notions of "fruitful".)

-- 
======================================================| God found the positive
Vaughan Pratt   pratt@cs.Stanford.EDU   415-494-2545  | integers, zero was
======================================================| there when He arrived.
Newsgroups: sci.physics