FOM: Topos book

[Harvey Friedman]

Response to Mclalrty, 4:28PM 1/24/98.

>    	You must have missed a lot of my posts, but here is an idea:
>Read my book. It has been around for 6 years saying just what I said
>here, firmly fixed on paper. Below I append a summary of the relevant
>passages with page numbers.

This is an irresponsible way to make your points on the fom. People are
busy, your book may not be easily accessible, and nobody thinks that the
best way for you to defend this stuff is necessarily in a six year old
book, since you now have the benefit of direct criticism from so many
genuine f.o.m. professionals. E.g., your book is taken out of the library
here, so I have never seen it.

>    	I just got my author's copies from the third printing and I'd
>be happy to send you one Harvey. (I can't do this for everyone.) Give me
>your surface address if you like. It might make the discussion more
>constructive.

Congratulations on three printings! Surface address: Harvey M. Friedman,
Department of Mathematics, Ohio State University, 231 W. 18th Ave.,
Columbus, O. 43210. Thank you.

I wrote:

>>Also, we don't have a concession from you that there is no
>>coherent conception of the mathematical universe that underlies categorical
>>foundations in your sense. You should make it more clear that you are very
>>proud of the fact that there is no such coherent conception of the
>>mathematical universe on which you base your approach so that the rest of
>>us can stop thinking that you are even trying to do foundations of
>>mathematics.

McLarty writes:
>
>    	You have my repeated statements that categorical foundations
>spring from many disparate examples--you quote one a few lines further
>on in your post (I do not requote it here). You are right that I am
>proud of this, though it was hardly my doing. I'll give you this,
>call it a concession if you like:
>    	I find many things relevant to foundations that you find
>irrelevant.

"Springing from many disparate examples" does not entail "no coherent
conception of the mathematical universe that unlerlies categorical
foundations." You still have not conceded that there is no coherent
conception of the mathematical universe that underlies categorical
foundations. We're still waiting for you to confirm or deny this. If you
want to confirm it, tell us about the coherent conception. If you want to
deny this, then tell us why you are proud of it, and what  concept of
"foundations" you have in mind. And then I will have more questions, later.

>    	Grothendieck uses perfectly usual set theoretic foundations
>himself. (I assume you consider inaccessible ordinals usual.) Is that
>supposed to prove his categorical ideas are not widely used to
>organize math?

Grothendieck as well as almost everyone else right now "uses perfectly
usual set theoretic foundations." Why don't you emulate him, instead of
trying to use his name in order to promote categorical/topos "foundations?"

I have already "conceded" that categorical ideas are widely used to present
some core mathematics.

>    	You have specific objections to category theory, and specific
>complaints about the motives of categorists, wildly disproportionate
>to your knowledge of either the theory or the theorists. You have a
>right to ignore whatever you want, but then what is the point of
>arguing about it?

Were you a five year colleague of Lawvere and Schanuel? I know them. And I
have talked to MacLane a fair amount over the years. I also am fully
familiar with Boolean valued models of set theory, and, more generally, of
Heyting valued models of set theory. I've used them in formal publications.
Perhaps you can elucidate for us the exact connection between these and
topoi.

>Summary of the statements on real analysis
>in toposes, from my book ELEMENTARY CATEGORIES,
>ELEMENTARY TOPOSES (Oxford, 1992).
>
>pages 128-132 describe differences between the logic valid in any
>topos, and the classical logic which is valid in certain ones.

Classical logic is the major way to do foundations of mathematics. Other
logics are normally used to formalize interesting restrictions on proofs
for many diverse foundational purposes and investigations. For instance, in
many contexts, if a proof is based on intuitionistic logic then we can
immediately deduce certain kinds of algorithmic information. Also in many
contexts, there are good reasons for looking at intuitionsitic logic since
it seems to correspond to a robust, informal conception - and this can be
backed up by important theorems.

The "logic" one is operating under is appropriately placed outside the
formalization - not enmeshed with mathematical objects. So from the point
of view of genuine f.o.m., what you wrote is philosophically incoherent.
You are confusing some sort of formal algebraic treatment of logic with
logic itself. This is a typical conceptual error of categorical
foundationalists. E.g., Lawvere told me that the existential quantifier is
not only best understood as some sort of map or functor (or other more
complex categorical object) - but can only be properly understood that way.

>pages 177-78 discuss arithmetized real analysis in any topos with a
>natural number object. The usual definitions are used, but in the weaker
>topos logic they do not give all the classical results. For a start,
>the Cauchy and Dedekind reals do not agree.

You seem to have gone out of your way not to make this point clear in your
response to my 9:06 PM 1/17/98. Your response was 10:59AM 1/18/98.

>pages 211-218 describe the topos of sets (that is, categorical set
>theory). Here, because the logic is classical, arithmetized analysis
>gives all the results in classical analysis that do not use the
>axiom of choice. If you add the axiom of choice to the topos axioms,
>you get all of classical analysis.

Here, presumably, you have topoi, natural number object, well pointedness,
and choice. This is what I call a slavish translation of set theory into a
bad notation.

>page 235 briefly mentions recursive real analysis, using the
>standard definitions for arithmetization but in a topos of recursive
>sets.

This I want to look at it with some care. What about the more
"foundational" (and philosophically interesting) Bishop's constructive
analysis? This is not the same as recursive real analysis. There is a big
difference. In any case, the proper formalization of Bishop's constructive
analysis is in a conventional f.o.m. style system. I wrote a long paper for
the Annals of Math. about this topic some time ago.

>There are references for more information, and I specify that little
>is published on categorical set theory per se because it "is not
>very different from other set theories, being just a little bit
>closer to naive practice" (page 255).

I'm not sure that it is "just a little bit closer to naive practice", but I
am sure that it is "very far away from genuine f.o.m." As you say, even
"Grothendieck uses perfectly usual set theoretic foundations
himself." Maybe you should, too.