Vaughan Pratt <pratt@cs.stanford.edu> Wednesday, March 5, 2008 8:32 am wrote, with much else:

On a related note, a careful reading of Max Kelly's "Basic Concepts of Enriched Category Theory" reveals that it is thoroughly grounded in Set,as I pointed out in August 2006 in my initial Wikipedia article on Max. I gave some thought to how one might eliminate Set from the treatment,without much success, and concluded that Max's judgment there was spot on.

Without addressing this particular issue I want to say I appreciate the phrase in the article: "the explicitly foundational role of the category Set." I take it this is Vaughan's? Various people including Sol Feferman promote the view that if you use "sets" then you are admitting that you use ZF and not some categorical foundations. Vaughan's phrase goes aptly against that: If you use sets, then you use sets, but there is no reason it cannot be on categorical foundations. He does not say it *is* on categorical foundations, and that is fine in the context. He reminds people that it *could* be. best, Colin

Colin is exactly right on all points. I tend to look at sets from the perspective neither of a set theorist nor a category theorist but a combinatorialist. As long as people agree on the cardinalities of the homsets between sets, particularly the finite ones, I figure they must be talking about essentially the same objects. Infinite domains are problematic for everyone, infinite codomains much less so (we understand the homset N^2 much better than 2^N). The remark in my post about the self-evident being merely a convenient long-held hypothesis (which I put on my "sayings" website http://boole.stanford.edu/dotsigs.html less than a month ago) applies in spades to membership as characteristic of sets, the premise for ZF. Those who identify acceptance of the category Set with acceptance of ZF have not only not accepted but not even grasped that the wholesale replacement of the binary relation of membership by the (partial) binary operation of composition, with a set of axioms radically different from those of ZF, is a foundational move. ZF is so deeply ingrained in their thought processes that they have no idea how to think about mathematical structures without falling back on its axioms. Borrowing from Hilbert, they are unable to replace "set," "function," and "composite" by "table," "chair," and "beermug." If you find it hard to imagine how anyone could find it hard to imagine mathematics without ZF, just read Steve Simpson on 2/25/98 (almost exactly a decade ago) at http://cs.nyu.edu/pipermail/fom/1998-February/001228.html The bit "I totally repudiate every syllable of every word of every subclaim of every claim that McLarty has ever made about what he is pleased to call `categorical foundations'" made abundantly clear back then that Steve could not begin to concieve of replacing membership by composition as the basis for an alternative foundation of mathematics. While I can't speak for Steve today, this remains a stumbling block for those raised to believe that rigorous mathematics would not be possible in a world where propositions such as "for all x and y there exists z such that x is a subset of z and y is a member of z" did not hold. How could x U {y} fail to exist and the walls of mathematics not come tumbling down? Vaughan Colin McLarty wrote:

Vaughan Pratt <pratt@cs.stanford.edu> Wednesday, March 5, 2008 8:32 am

wrote, with much else:

...

On a related note, a careful reading of Max Kelly's "Basic Concepts of Enriched Category Theory" reveals that it is thoroughly grounded in Set,as I pointed out in August 2006 in my initial Wikipedia article on Max. I gave some thought to how one might eliminate Set from the treatment,without much success, and concluded that Max's judgment there was spot on.

Without addressing this particular issue I want to say I appreciate the phrase in the article: "the explicitly foundational role of the category Set." I take it this is Vaughan's?

Various people including Sol Feferman promote the view that if you use "sets" then you are admitting that you use ZF and not some categorical foundations. Vaughan's phrase goes aptly against that: If you use sets, then you use sets, but there is no reason it cannot be on categorical foundations. He does not say it *is* on categorical foundations, and that is fine in the context. He reminds people that it *could* be.

best, Colin

Vaughan has written, in part, that he would

happen to find Excluded Middle more convenient than its negation, but that's just me and perhaps others have had the opposite experience.

Me too, for the most part(*), but as regards

Then there are those who accept neither Excluded Middle nor its negation, which takes us into the Hall of Mirrors that I always find myself in when I go down this particular rabbit-hole.

I find that it's NOT the case that I "accept neither" -- rather, it's that I sometimes prefer neither to accept it, nor to reject it, but to remain uncommitted. Noncommittally yours, -- Fred (*) I'm reminded of the legendary airline passenger who, faced with the stewardess's classic offer of "coffee, tea, or me," countered with: "Any chance of some tonic water instead, please?" -- F.

Paul Levy wrote:

Maybe not the walls of mathematics, but what about theorems like "every polynomial functor on Set has a unique initial algebra whose structure map is an identity"? I think theorems like this are worth retaining (and antifoundation makes even more of them).

I'm not sure what "retaining" means here. Does the category Set, even as a cartesian category, have *any* properties that are open to debate? (Other than by intuitionists, who seem to thrive on quicksand.) For Set as a cartesian closed category I can see room for debate about the number of nonisomorphic sets that can appear along a chain of monics from X to 2^X when X is infinite (defined say as admitting endomonics that are not automorphisms), but relatively little in practical mathematics seems to hinge on the outcome. Correct me if I'm wrong, but my impression is that for any given language in which to express properties of Set, whether that of categories, cartesian categories, cartesian closed categories, or toposes, the properties of Set, understood classically and up to equivalence, are essentially fixed modulo largely irrelevant minutiae such as the above. Your example is a perfectly identifiable property of any category with polynomial functors (suitably defined) such as Set. If the polynomial functors are those generated from the identity functor by binary product and coproduct, e.g. X, X+X, X^2, X+X^2, etc. then it holds of Set because then the initial algebra is always the empty set (but you probably had the empty product 1 in mind as well). If Set didn't have that property it wouldn't be Set, just as Z wouldn't be Z if integer addition wasn't commutative. The property P = "for all objects x and y there exists a set z for which x is a subset of z and y is a member of z" holds of all models of ZF. It cannot be said to hold of the category Set however, not because we can't prove it, i.e. can't imagine how assuming it false could do any harm, but because we can't define it, i.e. can't imagine how it could be either true or false. What does it even mean when applied to Set as a category, or as a cartesian closed category, or even as a topos? More structure than that has to be added to Set to make P meaningful. The same goes for AFA. Chapters 1-6 of Aczel are developed starting within the ZF framework. Categories enter at Chapter 7, but Set is already fully encumbered at that point with all the machinery necessary to interpret all sentences of the language of ZF, where P is true. In that sense even FA (the Foundation Axiom) creates properties of Set that are not meaningful for Set as a mere topos. AFA as a weakening of FA means that generically there are fewer properties than with FA, not more. Fixing a particular model of AFA creates properties specific to the model, which may or may not contradict FA. (Every model of ZF is automatically a model of ZF-FA+AFA.) Vaughan

On 5 Mar 2008, at 09:11, Vaughan Pratt wrote: VP>> My feeling about ... Brouwerian modes of thoughts is that they are ... great stories about things that never actually happened ... I happen to find Excluded Middle more convenient than its negation, but that's just me and perhaps others have had the opposite experience. <<VP I suspect that this feeling is shared to a greater or lesser degree by most practicing mathematicians. I also suspect that it arises out of perceptions based on Brouwer's interpretation and subsequent assessment of his own, original, objection to Hilbert's particular expression of The Law of the Excluded Middle, rather than on a perception of what it was that Brouwer was actually objecting to and rejecting. In other words, such perceptions may be vulnerable to the "cover-up" syndrome remarked upon by Physicist Richard P. Feynman in his 1965 Nobel Lecture: “We have a habit in writing articles published in scientific journals to make the work as finished as possible, to cover up all the tracks, to not worry about the blind alleys or describe how you had the wrong idea first, and so on. So there isn’t any place to publish, in a dignified manner, what you actually did in order to get to do the work.” I believe that Brouwer's "finished" articulation of his objection to Hilbert's position vis-à-vis the foundations of logical reasoning may be an instance of such unconscious ‘cover up’; if so, it is one that has had an unintended, far-reaching and severely limiting consequences on a discipline. The basis for my belief lies in Hilbert's interpretation of the universal and existential quantifiers, which is detailed, for instance, in his 1927 paper "The Foundations of Mathematics". In this paper, Hilbert defines the quantifiers in terms of his epsilon-function as: (i) The formal sentence [(All x)F(x)] holds under a consistent interpretation I if, and only if, the interpreted relation F(s) holds whenever ~F(s) holds for any given s in I; hence ~F(s) does not hold for any s in I (since I is consistent}), and so F(s) holds for any given s in I. (ii) The formal sentence [(Exists x)F(x)] holds in I if, and only if, the interpreted relation F(s) holds for some s in I. He then deduces from it "Aristotle's dictum" and the "principle of the excluded middle": (iii) Aristotle's dictum: If the formal sentence [(All x)F(x)] holds in I, then the interpreted relation F(s) holds for any s in I, and: (iv) Principle of excluded middle: If the formal sentence [~(All x)F(x)] holds in I, then the formal sentence [(Exists a)(~A(a)] holds in I. (I assume that the above paper also reflects Hilbert's thesis prior to Brouwer's objection.) Now, in his 1908 paper "The Unreliability of the Logical Principles", Brouwer stressed that, for Hilbert's above interpretation to be considered sound when the domain of the quantifiers under an interpretation is infinite, the decidability of the quantification under the interpretation must be constructively verifiable in some intuitively and mathematically acceptable sense of the term "constructive". I doubt whether any practicing mathematician would take serious issue with this objection. I feel it is the perception that Brouwer's - and the Intuitionistic - objection relates specifically to the Law of the Excluded Middle - of which (iv) is merely one statement - that seems to give rise to the sense of disquietitude expressed by Vaughan Pratt in his above cited post. The reasons for such disquietitude are not far to seek. Currently it is implicitly accepted (as intuitively plausible) by practicing mathematicians that, in first-order Peano Arithmetic (PA) for instance: (1) The PA-formula [(Exists x)F(x)] is an abbreviation of [~(All x)~F(x)], and is defined as true in the standard interpretation M of PA if, and only if, it is not the case that, for any given natural number n, the interpreted relation ~F(n) holds in M; (2) The interpreted relation F(n) holds in M for some natural number n if, and only if, it is not the case that, for any given natural number n, ~F(n) holds in M. Now, since (1) and (2) together interpret (Exists x)F(x) in M as intended by Hilbert's epsilon-function, they similarly attract Brouwer's objection - which, thus, remains unresolved in current literature. Thus, for a practicing mathematician today, the Intuitionistic rejection of the Law of the Excluded Middle should be tantamount to rejecting the standard interpretation of first-order PA as a valid model for PA. This is not obvious if Brouwer's objection is perceived as primarily rejecting Hilbert's principle of the excluded middle (iv), since the latter may have other avatars, not all of which need attract Brouwer's objection. In other words, Brouwer's objection needs to be seen not as rejecting the Law of the Excluded Middle per se, but as specifically rejecting only Hilbert's interpretation of the existential quantifier in (ii). The point to note then is that, whereas (1) by itself preserves the formal properties of PA-negation under interpretation in M, the further inference in (2) from (1) does not; and it is this inference that is objected to by Brouwer. Moreover, Brouwer's objection becomes significant only if we accept that (2) appeals to Platonically non-constructive, rather than intuitively constructive, plausibility. Since most practicing mathematicians are comfortable with informal Platonic reasoning, but uncomfortable with formal reasoning that cannot be interpreted constructively, it is this aspect of (2) that appears to place them on the horns of the following dilemma: Even if we accept that the existential quantifier is interpreted non-constructively in current literature by accepting (2), how do we interpret such quantification constructively without sacrificing mathematical reasoning and mathematical structures that a practicing mathematician intuitively accepts as well-founded? This is the grey area that Intuitionistic - and finitist - reasoning have sought to address since Brouwer, primarily by focusing on what remains of classical mathematics (post Hilbert) after rejecting (2) above. The problem, of course, is that rejection of a widely - even if uncomfortably - held tenet is never a solution unless one replaces it with one that is less uncomfortable. This is the "It's better to live in a house with a leaking roof, than to bring the roof down over one's head" syndrome. So the question is: Can we provide a "comfortable", finitary, interpretation of PA that accepts (1), but rejects (2) if necessary? I believe that every practicing mathematician knows that the answer to this question must be a "yes', since mathematical languages seem to communicate effectively in practice in all areas of human endeavour. In other words, every practicing mathematician knows that the significant body of mathematical reasoning and structures is founded on a finitary foundation. The issue, therefore, is simply one of identifying the structure. Now Turing has shown in his seminal 1936 paper on computable numbers that every arithmetical function (or relation, when interpreted as a Boolean function) F defines a Turing-machine TM_F. This suggests the possibility of replacing (1) by: (3) The PA-formula [(Exists x)F(x)] is an abbreviation of [~(All x)~F(x)], and is defined as true in an interpretation B of PA if, and only if, it is not the case that the Turing-machine TM_F computes F(n) as always false (i.e., as false for any given natural number n in B). Now, I have shown in the Dec07 issue of the on-line journal, The Reasoner, that an interpretation along these lines is actually a finitary model for PA, since all theorems of PA interpret as true in B. http://www.thereasoner.org/ Moreover, the interpretation B satisfies Brouwer's criteria, since - by virtue of Turing's Halting argument - the mirror of (2) does not hold in B. In other words, in the finitary model B, from the PA-provability of [~(All x)F(x)], we may only conclude that TM_F does not compute F(n) as always true in B. We may not conclude further that TM_F must compute F(n) as false in B for some natural number n, since F(x) may be a Halting-type of function that is not Turing-computable. What this means is that we may not conclude from the PA-provability of [~(All x)F(x)] that F(n) does not hold in B for some natural number n. Of course the consequences of such a finitary model for PA are far-reaching, since it (expectedly?) follows that the accepted standard (non-constructive) interpretation of PA - which is based on accepting (2) above - is not a model of PA! I address the above points in detail in a series of commentaries in the Sep07, Oct07, Nov07, Dec07 and Jan08 issues of The Reasoner and in two papers that I am compiling for publication: * Why Brouwer was justified in his objection to Hilbert's unqualified interpretation of quantification http://alixcomsi.com/9_Why_Brouwer_was_justified_Rev_1000.pdf * Is PvNP formulated adequately? http://alixcomsi.com/Is_PvNP_formulated_adequately_Update.pdf Sincerely, Bhup

Vaughen wrote: My question to Steve and the list as a whole would be, if you had been assigned the task of writing an explanation section following the formal definition section, where would you have put the emphasis: on how the definition facilitates a first-order characterization of the notion of "subobject", or on the geometric morphism perspective? My answer: Topos theory, like other theories, is about the interaction of objects (toposes) and morphisms (geometric morphisms). I see it as inherently an aspect of category theory. We use category theory to define it and I believe the most effective expositions on topos theory are those that are based on category theory. Agreed, a strength of the definition of topos is that it allows a multi-faceted approach (three blind men ...) but my personal view is that this must confuse any newcomer. A topos is a type of category which [insert definition here]. Some of the basic results of topos theory are [insert categorical lemmas here]. Once these categorical foundations are in place one is able to (a) investigate/research toposes and (b) learn more about other (say logical) aspects of toposes. I don't want to detract from the importance of (b), but (a) can be carried out without (b). Christopher -----Original Message----- From: cat-dist@mta.ca [mailto:cat-dist@mta.ca] On Behalf Of Vaughan Pratt Sent: 11 March 2008 07:33 To: Categories list Subject: categories: Re: Heyting algebras and Wikipedia Steve Vickers wrote:

The gorilla in the cage is the topos in the classical world.

According to http://en.wikipedia.org/wiki/Gorilla, gorillas in captivity tend to obesity and earlier maturation of females, and have been taught sign language. It doesn't mention any other differences, and the rest of the article is about gorillas in the wild. Does this make a "topos in the classical world" a gros topos and the wild ones petit? The analogy is rather on the colorful side for me. The first half of http://en.wikipedia.org/wiki/Topos is about Grothendieck topoi [sic], the rest about elementary toposes (was topoi but I changed it out of deference to PTJ's strong feelings in the matter). The Explanation section (my contribution, intended as a response to the "respectful awe" tone of the comments on the article's talk page reacting to the bald definition, i.e. the commenters seemed largely mystified but accepted this as par for the course for anything this far beyond rocket science) is presented from the point of view of elementary toposes as a solution to the problem of characterizing the notion of subobject in elementary terms. My question to Steve and the list as a whole would be, if you had been assigned the task of writing an explanation section following the formal definition section, where would you have put the emphasis: on how the definition facilitates a first-order characterization of the notion of "subobject", or on the geometric morphism perspective? Vaughan