FOM: Let's get some perspective on things here ...

[Neil Tennant]

For those who, like Michael Thayer, see any sort of invidious contrast
between interest in large cardinals, independence results, etc., on
the one hand, and, on the other, interest in the nature of alien math,
the nature of conclusive proof, etc., I would like to say that I, for
one, respect and admire (and indeed envy) Harvey for the technical
depth and philosophical importance of the results he obtains, and the
questions he raises, about the sorts of problems that occupy him. He
ought to be receiving a greater measure of appreciation and
constructive feedback from this list. (Consider, for example, his
slam-dunk on the recursive independent axiomatization problem
discussed recently.)

My own view is that the foundational centrality of Harvey's work
should need no explanation to any professional academic on this list.
It might be a good exercise for detractors to print off Harvey's
eleven positive self-contained postings thus far, and read them right
through. Note that the underlying theme is always `what formally
tractable shape can we give such-and-such important philosophical
problem in foundations?'.

The problems cover a considerable range, also. Now, apart from reverse
mathematics, proof theory, recursion theory etc. in which Harvey seeks
results of interest, there is one particular area of endeavour on
which Thayer appears to cast aspersions: the work on independence
results.  I feel I must hasten to point out to Thayer the right
context in which to appreciate Harvey's recent finite independence
results; for they are different from Go"del's original ones. Here's how:

Go"del showed that a weak system (PA) could not decide a certain very
complicated sentence G that had no intuitive mathematical content of
its own. But G can be decided (as true, assuming the consistency of
PA) by extending the language of PA with a truth-predicate and using
induction on an appropriate formula involving the new predicate.  The
Go"del-Cohen result on the Continuum Hypothesis (CH independent of
ZFC) was different in that the independent sentence was of great
mathematical importance, and it was shown to be independent of quite a
strong system.  (Note, however, that CH involves quantification over
much higher-order entities than natural numbers.)  The Paris-
Harrington independent sentence is a more natural and intuitive
mathematical statement than G, combinatorial in nature, and not
involving those quantifications over higher-order entities that is
characteristic of CH; and it can be shown to be true within the much
weaker system ZF.

What distinguishes Harvey's independence result is the naturalness
of the independent sentence, its combinatorial character, and the power
of the system of which it is independent.

We can summarize as follows:

	   | Sentence...	  | Independent of... | Decided in...
___________________________________________________________________________
Go"del	    G ("I am unprovable")   	PA		Slight extension
	    Terribly complicated,  			of PA
	    very unnatural.
	    Combinatorial
___________________________________________________________________________
Go"del-		Continuum Hyp.		ZFC		ZF+V=L (positively)
Cohen		Natural,deep,				ZFC+MA (negatively)
		but higher-order
___________________________________________________________________________
Paris-		Natural,		PA		ZF
Harrington	combinatorial
___________________________________________________________________________
Friedman	Natural,	ZFC+large cardinals	ZFC+yet larger
		combinatorial				cardinal
___________________________________________________________________________

Harvey's result optimizes on both dimensions.

At the very least, we have now learned something about the necessary
use of large cardinals in set theory to settle the truth of simple
combinatorial statements.  What mathematician could now hope to get
away with saying "Oh, all this arcane set-theoretical stuff is totally
irrelevant to everyday mathematical concerns"?

Neil Tennant