FOM: Grothendieck and Friedman

[Harvey Friedman]

I wish to thank McLarty for drawing similarities between aspects of
Grothendieck's work and mine. But I still think that the analogies are
somewhat strained.

The aspect of my work that I would emphasize the most in this context is this:

1. Mathematicians are very fond of using relatively abstract machinery to
solve relatively concrete problems. E.g., use of complex analysis to prove
number theory.

2. Generally, the mathematicians know how to eliminate the machinery -
perhaps at the cost of losing the clarity of the proofs. However,
mathematicians  don't have any demonstrably necessary uses of relatively
abstract machinery. They don't know how to formulate such a result.

3. I have a series of demonstrably necessary uses of extremely abstract
machinery for discrete/finite mathematics. The results are clearly and
robustly formulated using modern mathematical logic.

McLarty 5:53PM 4/2/99 wrote:

>        The combinatorial theorems are formally derivable in (ZFC plus the
>consistency assertion). But you claim the consistency assertion is
>unmotivated and unmathematical unless it is derived from existence of the
>cardinals.

The consistency of large cardinals can sometimes be used as an alternative
axiom to the existence of large cardinals themselves. And the
appropriateness of the consistency of large cardinals as an axiom is an
interesting issue. However, I have not addressed this issue in anything I
have written or posted on the FOM. Furthermore, this issue is entirely
irrelevant to the discussion we are having.

Instead, the issue that I have addressed is the distinction between
mathematically well motivated assertions (e.g., every continuous function
on the closed unit interval attains a maximum value), and
metamathematically well motivated assertions (e.g., consistency of large
cardinals). I strive to show that there are assertions of the first kind
lying in discrete/finite mathematics that require use of large cardinals to
prove. Under the analysis of "require" in terms of translatability, this is
normally done by showing that the assertions of the first kind lying in
discrete/finite mathematics are equivalent to the consistency of large
cardinals.

What you wrote above doesn't make any sense since the consistency of large
cardinals obviously follow from existence of (slightly bigger) large
cardinals.
>
>        Similarly Grothendieck knew that formal proofs were available
>without using universes. But those formal proofs seemed to him unmotivated,
>vast seas of technicality, lacking the clear mathematical motivation of his
>method--and indeed those proofs were found precisely by eliminating the
>universes from Grothendieck's methods.

My case is not similar, even in this respect. In my case, the proofs of the
discrete/finite results from large cardinals are virtually identical to the
proofs from the consistency of large cardinals. (This has to be modified
slightly: in some cases I need 1-consistency, and also some additional
arguments which are interesting and useful).
>
>The similarity is: just as you feel the consistency
>assumptions only make sense when you derive them from existence of the
>cardinals; so Grothendieck feels individual calculations of cohomology only
>make sense in the general context of derived functor cohomology.

But I gather that these individual calculations of cohomology consitute
real removals of his universes in a sense that is widely recognized by
mathematicians. The consistency statements are not in any comparable way a
removal of large cardinals. They are mentioned explicitly in the
consistency statements. And as I have indicated, the proofs using the
consistency statements are more or less the same as the proofs using the
large cardinals themselves.

>        My phrase "forget rigor" should tip you off that this approach is
>not formalizable. Ditto when I say it is "unconcerned with FOM". It simply
>ignores real foundational problems. It is commonly used and it "works" for
>the "working number theorist". But we should not confuse it with FOM.
>
[McLarty was referring to another approach of, e.g., Gunter Tamme, and not
Grothendieck].

It still might be interesting to try to formalize this approach in a way
that preserves its attraction for the "working number theorist." One might
find some interesting new formalisms that skirt inconsistency in some new
way. It would be surprising if, say, NF or NFU could be used in a
particularly neat way to formalize this "informal algebraic geometry"!