Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Sorry to do this, but for some reason an “XML Parsing Error” is not allowing me to enter the earlier discussion. So I’m continuing here.
I was trying to find the link to Toby’s document, but without success. But I’m sure he can help. Alternatively, if I get a head of steam, I may try writing down ETCS formally somewhere in the Lab.
Wait, I thought we were talking about Bourbaki set theory because you (Harry) liked it for some reason.
That’s what I thought too! And still waiting to hear which of Bourbaki’s ideas about foundations Harry finds attractive.
I think the XML parsing error is because you wrote “Caf&ecute;” instead of “Café”. Maybe the forum should detect and clean nonexistent entities.
I like how meaning arises from the formal rules, and how so much structure is built up from such a small amount of initial structure.
Harry wrote:
I’ll be happy to abandon it if I can find a sufficiently formal exposition of a better one.
Are you saying that you choose your foundational system based on how detailed of a formalization you can find? That’s a different ethic from mine. (-:
If building up structure from a small number of formal rules is what you like, you may want to look into dependent type theory. That’s a very formalized, and very structural, foundational system, and it’s moreover been implemented in many computer proof assistants like Coq and Agda.
Are you saying that you choose your foundational system based on how detailed of a formalization you can find? That's a different ethic from mine. (-:
I don't like taking things on faith.
If building up structure from a small number of formal rules is what you like, you may want to look into dependent type theory. That's a very formalized, and very structural, foundational system, and it's moreover been implemented in many computer proof assistants like Coq and Agda.
Does DTT require one to assume that there's some crazy kind of giant universe of types? I like the small number of rules, but I also like the minimalist initial structure of Bourbaki, where you have a universe consisting of variables with no actual structure on them. The only rule of inference in Bourbaki is modus ponens. Is the same true of DTT?
DTT is a purely syntactic calculus; it requires no assumptions of any sort. The basic notions are (dependent) abstraction and application, which are essentially the same as modus ponens under propositions as types.
Very cool. Could you suggest a book/series of papers that will bring me in on the ground level (like Bourbaki does) and develop the whole thing from scratch?
Okay, Harry, I’ve written an article fully formal ETCS. You will note there’s no informal anything like informal classes, collections, or whatnot. I hope this clears up the matter that was initiated over at MO.
It’s possible that a mistake crept in, but hopefully the presentation is followable. Discussion and (carefully considered) suggestions for improvement are of course welcome!
Neat, thanks!
I added some hyperlinks to fully formal ETCS, also linked to it from a new “Definition”-section at ETCS and linked to it from a new “Examples”-section at algebraic theory
Thanks very much!
Lawvere & Rosebrugh’s Sets for Mathematics is at roughly the same level as Halmos’s Naive Set Theory. (But I may be wrong, since I’m going only by memory of Halmos without checking again. Actually, I’m not checking L&R again either, but I’m quite confident about my memories of L&R.) Neither of these books covers elementary first-order logic in a formal way, and this remains a gap in the formality of the foundations that they present.
I am tempted to say that if one knows logic, then it is obvious how to make either L&R or Halmos into a fully formal theory with no gaps, so anybody who doubts them just needs to study logic. As first-order theories, they are given in complete detail (although both of them do so in a dawdling way, with a complete list of axioms only at the end). But you still have know how to deal with a first-order theory. (Also, L&R use a simply typed theory, while Halmos’s theory is untyped, so you have to know a little bit more logic for L&R than for Halmos. You could present ETCS as an untyped theory, but L&R doesn’t do it that way.)
In contrast, any foundation which is not a first-order theory (such as dependent type theory) is going to look both more formal and more complicated than these books. And then there’s Bourbaki; their foundation is a first-order theory, but since they insist on putting in all of the detail, they also have to put in all of the detail of first-order logic, which L&R and Halmos do not do. (But Bourbaki doesn’t cover first-order logic in general, only the first-order language of their particular theory. And they handle bound variables in an unusual way, although I’m pretty sure that it’s fully equivalent to first-order logic as normally understood.)
@ Harry #6 re
Does DTT require one to assume that there’s some crazy kind of giant universe of types?
To forestall confusion: Some versions of dependent type theory talk about universes, much as some versions of set theory talk about universes. Besides being optional, they are part of theory, not an assumption used by the theory (which, as Mike said, is purely syntactic).
@ Urs #11
But ETCS is not an algebraic theory. As Todd explains in the remarks at the end, even the theory of a topos with natural numbers object is only an essentially algebraic theory. With well-pointedness and the axiom of choice, ETCS is not even that. (As far as I know, it doesn’t fall under any interesting subclass of first-order theories, although of course this depends on what ‘interesting’ means.)
(But Bourbaki doesn't cover first-order logic in general, only the first-order language of their particular theory. And they handle bound variables in an unusual way, although I'm pretty sure that it's fully equivalent to first-order logic as normally understood.)
I could have sworn that the epsilon calculus makes it a bit stronger, but otherwise, yes, I think that sounds right (although I wouldn't be the person to ask). Thanks for the information!
I am tempted to say that if one knows logic, then it is obvious how to make either L&R or Halmos into a fully formal theory with no gaps, so anybody who doubts them just needs to study logic.
I was going to say something along these lines, about how this is why hardly anyone presents such theories in a completely formal manner any more. Anyone who cares, usually knows enough logic to be able to do it themselves.
Quite right, but I hope it’s clear why I went through the exercise anyway. Apparently there were some misconceptions which needed clearing up. What you call a “teachable moment”.
Of course, ZFC actually has an infinite number of axioms, but I know what you mean; not sure how to phrase that better.
Why did you choose the single-sorted definition of a category?
perhaps to avoid using (even low level) ’dependent type’-type language or constructions? (ugh, can’t think how to avoid some sort of linguistic clash there. the other involved the word ’sort’)
It was obviously completely unnecessary to use the single-sorted definition; the only reason I did so is my impression that “most (non-logician) people”, when they read accounts of things like signatures and first-order theories, are shown just the single-sorted notions, so I went along with that. Again, a completely unnecessary restriction, and there’s probably another teachable moment in there.
I don't understand this Zen of "teachable moments". Could you clarify?
“Teachable moment” is partly a winking allusion to the beers-with-the-president event a few months ago involving Henry Gates, but that’s completely irrelevant here, so you can ignore it.
I constructed fully formal ETCS in response to something you said (and which I might not be able to access fully if it’s on the old Bourbaki set theory discussion, since my typo got me locked me out) – that ETCS somehow involves an informal idea of collection, in contrast with say Bourbaki set theory. You did say something like this at MO, and I wasn’t sure what you meant, and later you mentioned Sets for Mathematics and how they had that informal notion in there, and that you looked in vain for where they avoid that, and you seemed to come to the conclusion that, in contrast to Bourbaki’s treatment, it was somehow needed.
My response at MO was that ETCS is, like ZFC and Bourbaki’s set theory, a formal first-order theory which, as such, makes no reference to informal collections. The fact that almost no one sets it out in such a formal way is beside the point. But since you continued to reiterate your point, I thought it would be a good idea to set down the formal axioms once and for all, to remove any doubts. So, I turned what seemed to be a misunderstanding into something a little bit constructive, hence, “a teachable moment”. Hope it makes sense now.
1 to 23 of 23