Hi Paul,
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?
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).
If we leave out "the structure map is the identity", I have no problem. The 2nd part seems to be rather cosmetical anyway, but in a bad sense of hiding the structure. Yes, I know you save some ink...
I'd also like to suggest that "foundations" is being used in two very different senses. In FoM, it's about quantifying the philosophical risks involved in particular formal systems and proofs, i.e. issues such as relative consistency, omega-consistency, etc. For this purpose the primacy of membership vs composition is quite immaterial. One could, I suppose, make a formal theory based on composition equal in strength (in whatever sense) to ZF.
Exactly, the discussion is similar to the question whether the carta of human rights should be written in English or French. I don't care whether foundations are expressed in the language of predicate logic, category theory or type theory as long as they make sense (to me). Having said this I prefer the latter two, which work very well together, but this again has to do with beauty as opposed to cosmetics.
Category theory on the other hand is about fundamental algebraic structures. I don't think it makes sense to ask "is category theory omega-consistent?" as one can for ZF (not that anyone knows the answer).
Precisely! Cheers, Thorsten
Paul
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
-- Paul Blain Levy email: pbl@cs.bham.ac.uk School of Computer Science, University of Birmingham Birmingham B15 2TT, U.K. tel: +44 121-414-4792 http://www.cs.bham.ac.uk/~pbl
This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.