FOM: Books, foundations, intuitionism, NF

[Harvey Friedman]

Reply to Pratt 7:15PM 2/27/98. I wrote:

>>The problem is that at the moment
>>there is no comprehensive categorical foundations, or any comprehensive non
>>set theoretic foundations.

Pratt replied:

>This claim, frequently made on FOM, reflects not so much on the coherence
>of categorical foundations as on the technical narrowness of those making
>the claim.  The claim is more than adequately refuted by the substantial
>body of literature on categorical foundations.  Besides the many papers
>on the subject, books on categorical foundations appear these days at
>the rate of one every eighteen months or so.

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.

>This is serious work, which you do a serious injustice in
>dismissing so casually.

This is not serious work as f.o.m., and I do justice by distinguishing it
merits as organizational schemes, ultimately founded in set theory, from
its demerits as coherent comprehensive autonomous f.o.m.

Let me remind you of my two favorite revealing quotes on the fom in this
regard:

>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 7:15PM 1/16/98:

>... 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.  'Logical' because what a
>topos is requires a definition in order to work with it and prove theorems
>about it, and this definition ultimately returns to the notions of
>collection (class, set, or whatever word you prefer) and function
>(or operation). 'Psychological' because you can't understand what a topos
>is unless you have some understanding of those notions. Just writing down
>the "axioms" for a topos does not provide that understanding.

You could directly address these two quotes.

>BOOKS ON CATEGORICAL FOUNDATIONS

>Johnstone, "Topos Theory", Academic Press, 1977.
>Goldblatt, "Topoi: the categorical analysis of logic", North-Holland,
>1979.
>Makkai and Reyes, "First Order Categorical Logic", Springer-Verlag, 1977.
>Barr and Wells, "Toposes, Triples, and Theories," Springer-Verlag, 1985.
>Lambek and Scott, "Introduction to Higher-Order Categorical Logic,"
>Cambridge, 1986.
>Bell, "Toposes and Local Set Theories," Oxford, 1988.
>Makkai and Pare, "The Foundations of Categorical Model Theory", AMS
>CM104, 1989.
>Freyd and Scedrov, "Categories, Allegories", North-Holland, 1990.
>Moerdijk and Reyes, "Models for Smooth Infinitesimal Analysis",
>Springer-Verlag, 1991.
>McLarty, "Elementary Categories, Elementary Toposes," Oxford, 1992.
>Mac Lane and Moerdijk, "Sheaves in Geometry and Logic", Springer-Verlag,
>1992.
>Borceux, "Handbook of Categorical Algebra" (three volumes), Cambridge,
>1994.
>Lawvere and Schanuel, "Conceptual Mathematics", 1997.
>Joyal and I. Moerdijk, Algebraic Set Theory, LMS Lecture
>	Note Series 220, Cambridge University Press, 1995.

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?

>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?

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.

At a more fundamental level, there is the intuitive concept of changing
number, or moving point. These are handled by adding an additional
variable. E.g., a changing number is a function. I have long asked for an
autonomous comprehensive coherent foundations where you DONT add additional
variables for such purposes. I never got the chance to work on this
properly. This I regard as hopeful, interesting, promising, and exciting.

>Computer scientists for whom flow, process, transformation, and function
>are fundamental notions have been very receptive to other foundations
>than set theory.

Most computer scientists take elementary math for granted, and know there
is a firm f.o.m. They just use elementary math, and distinguish f.o.c (c =
computer science) from f.o.m.

>In fact there are hardly any programming languages
>that start from sets and implement their remaining abstractions on top
>of them.

F.o.p. is not f.o.m. (p = programming).

>The preferred fundamental abstractions in computer science have
>traditionally been arrays, strings, and linked lists, and more recently
>records or structs, which occupy positions in the mathematical universe
>somewhere midway between sets and categories.

F.o.d. is not f.o.m. (d = data structures).

>Friedman and Simpson's insistence notwithstanding, the intellectural
>debt owed by arrays, strings, linked lists, and records to sets is no
>stronger than that to categories.

The intellectual debt is extremely indirect - that computer scientists take
elementary math for granted, and accept that there is a foundation behind
it, which they usually don't care about or need to know about.

>Most computer scientists view their
>fundamental data structures as self-evident notions that are adequately
>primitive in their own right, and see no advantage to reducing them to
>sets, however one might go about it.

It is a defensible view, since one can make up some kind of appropriate
foundation for such focused notions; i.e., a theory of inductively
(ordinary, not transfinite) defined structures with induction and recursion
as the basic principles. However, the difficulties even surrounding this
are not to be underestimated. I doubt if it has been done adequately by the
standards of the usual set theoretic foundations.

>From Pratt 6:47AM 2/27/98

>If you treat intuitionism as pure formalism and pretend it is meaningless
>then you are at risk of committing the same fallacy as David Hilbert and
>Roger Penrose (to pick just two prominent offenders), namely that not
>having double negation and excluded middle as laws ties one's hands.
>Goedel realized early on the fallacy of this reasoning when he showed
>one way of embedding classical arithmetic in intuitionistic.

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."

Reply to Tennant, 2:38PM 2/27/98

>The whole interest in Dummett's meaning-
>theoretic justification of intuitionism is that it gets away from the
>earlier solipsistic motivation that Brouwer had. Dummett's argument for
>intuitionism is based, rather, on the *publicity* of communication, and
>the so-called Manifestation Requirement. The MR is that grasp of meaning
>should be able to be made manifest in the appropriate exercise of
>recognitional
>capacities relating to the use of sentences.

You seem to suggest that there is a coherent view of intuitionism -
different than Godel, Heyting, and Brouwer. I would like to see you explain
*carefully* what this is without sending us to papers and books. If it is
good, it can explained on the fom, at least enough so that one can get a
feel for it.

Reply to Randall Holmes, 1:30PM 3/1/98

>However, there is an underlying conception of sets which leads to
>NF.  I believe I described it in an earlier posting to the fom list.
>It is described in my paper "The set-theoretical program of Quine
>succeeded, but nobody noticed", in Modern Logic, vol. 4, no. 1.

Virtually noone thinks that there is such a thing that leads to NF. (Do you
mean NFU?) If you have such a thing, surely you can explain it *carefully*
on the fom, at least enough so that one can get a feel for it.