FOM: Books, foundations, intuitionism, NF

[Vaughan Pratt]

From: Harvey Friedman <friedman at math.ohio-state.edu>
>This claim, frequently made on fom, reflects on the coherence of set
>theoretic foundations and on the misunderstanding of that coherence and of
>the concept of "foundations" by those rejecting the claim. The claim is
>more than adequately established by the substantial body of literature on
>set theoretic foundations, and its comparison with books on categorical
>foundations.

Almost every 19th physicist would have surely felt just this way about
classical mechanics.  That CM is coherent and "adequately established"
by a "substantial body of literature" makes it an attractive subject for
20th and even 21st century high school and beginning undergraduate physics
students.  But its coherence and thorough documentation notwithstanding,
classical mechanics is viewed today as a highly incomplete account
of mechanics.

You are in good company when you reject novel foundations that conflict
with your own understanding of your own subject.  Einstein rejected
the new quantum mechanics of Heisenberg and Schroedinger because its
intrinsically probabilistic component conflicted with his pre-1926 view
of the universe as governed by entirely deterministic laws.  Yet Einstein
saw the incompleteness of the older pictures and had a strong sense that
improvement was possible, a sentiment you have expressed yourself about
your own subject, in which you are much more expert than I.

From: Silver
>What I'm looking for is a development of category theory, or
>perhaps topos theory, that is based on some underlying *conception*.
From: Feferman
>... the notion of topos is a relatively sophisticated mathematical
>notion which assumes understanding of the notion of category and that in
>turn assumes understanding of notions of collection and function. ...
>Thus there is both a logical and psychological
>priority for the latter notions to the former...

From: Friedman
>You could directly address these two quotes [Silver and Friedman].

You may be forgetting that I already did, in FOM mail dated respectively
Thu, 22 Jan 1998 16:12:05 -0800 and Thu, 20 Nov 1997 10:16:03 -0800.

>I have recently looked at Lambek and Scott, at McLarty, at MacLane and
>Moerdijk, and at Lawvere and Schanuel. None of these books puts forward
>category theory as a comprehensive, coherent, and autonomous f.o.m. What
>about the rest?

Since you're making a claim about what the authors put forward,
clearly those authors are the appropriate people to comment on this.
Since one of them is here we can ask him directly.  Colin, did you put
forward category theory as a foundation for mathematics?

My impression was that he did.  If so, the fact that you have misjudged
what one of them has put forward, combined with the fact that they all
tell aspects of the same coherent story, together raise the possibility
that you have misjudged not merely what individual authors are putting
forward but what the entire enterprise is putting forward, with regard
to all three of coherence, comprehensiveness, and autonomy.

>From Pratt 9:34PM 2/28/98
>Going in the other direction, how can one reasonably view as a set the
>process of *gradually* stretching the real line until all its points are
>twice as far apart?

Friedman:
>Perhaps you mean something more subtle. The function F:[1,2] x R into R
>given by F(x,y) = xy. Adding an extra variable for such purposes is
>standard in, say, homotopy theory; e.g., see section 4-2 Homotopic
>mappings, Topology, Hocking and Young, Addison-Wesley, 1961.

Point conceded, my argument was a bit of a strawman.

>I'm not sure what you are saying, but Godel obviously regarded classical
>logic as the underlying logic of mathematical reasoning. ...
>In his review of
>Heyting, The intuitionist's way of founding mathematics, 1931, Godel states
>his view of the philosophical attitude of the intuitionist, "for whom
>amthematics is a natural function of the intellect, a product of the human
>spirit, and who therefore grants no objective existence, independent of
>thought, to mathematical enetities. This conception - that mathematical
>objects exist only insofar as they can actually be comprehended by human
>thought - leads to the rejection of pure existence proofs, as well as the
>principle of the excluded middle in all cases in which a decision among the
>alternatives cannot actually be made." This is from Godel, Collected Works,
>ed. Feferman et al, vol. 1, page 247. Godel vehemently rejected this point
>of view in a great many of his writings. He regarded intuitionism as a way
>of "tieing one's hands."

What Goedel is rejecting here in 1931 would be less confusingly called
formalism today.  Although formalism is still alive and well, what
passes for intuitionistic logic today reconciles syntax and semantics
every bit as well as does classical logic.  My impression (and I will
gladly defer to the experts on Goedel, who are far better qualified
than I to pronounce on what he believed) is that Goedel understood as
well as any the difference between formalism and what at least some of
us now standardly mean by intuitionistic logic, perhaps not in 1931 but
certainly in his lifetime.

My personal understanding of intuitionistic logic as it arises in the
practice of law, science, etc. is an entirely semantic one, to the full
extent that any precise concept can be semantic.  Intuitionistic truth
resides in a distributive lattice, with implication A->B being that
proposition which is just sufficient to entail B whenever A holds.

That intuitionistic implication is more properly understood semantically
than syntactically is witnessed by its having no canonical syntactic
definition (A->B can be defined as the greatest C such that (A and C) <=
B, or the function Aimplies(x) can be defined as left adjoint to Aand(x)),
but a unique denotation in the semantic domain.  The same is true of
intuitionistic conjunction and disjunction, but that should occasion less
concern since taken by themselves they are indistinguishable from their
classical counterparts, unlike intuitionistic implication which fails
Peirce's law all by itself despite its uniquely determined denotation.

Vaughan Pratt