no membership-respecting morphisms
Mike Barr quoted a "thought of Chairman Pratt" that was attributed to him,
Monotone functions respect order, group homomorphisms respect the group operation, linear transformations respect linear combinations, and gangsters respect membership in the Cosa Nostra, but what morphism has ever respected membership in a set? It is sheer hubris for a relation that can't get no respect to claim to support all of mathematics. (Old argument of category theorist Mike Barr, new polemics.)
and commented on it,
That is not a bad rendition (save for the reference to Cosa Nostra) of what I actually said which was that we create these elaborate structures of well-founded trees subject to the rule that two chidren of the same leaf cannot be isomorphic. But then, unlike all other structures that we build, we make no hypothesis that functions preserve the structure. Indeed, I think a structure-preserving map must be the inclusion of a subset. And there are no non-identity endomorphisms.
Of course, I entirely agree with the sentiment that epsilon-structures are completely inappropriate as a basis of most ordinary mathematics. However, mathematics and mathematicians are contrAry beasts, who treat any statement of the form "there is no such thing as ..." as a challenge, whether it be about membership-preserving functions or the square root of -1. Indeed, it's quite interesting to look at "carriers equipped with membership relations" in the same way as "carries equipped with group multiplications". This is what I did in my paper "Intuitionistic Sets and Ordinals", JSL 61 (1996). For a more categorical treatment, we may regard the relation as a coalgebra structure for the full covariant powerset functor. This is what Gerhard Osius did in his "Categorical Set Theory" in JPAA 4 (1974) and what I did for other functors in my unpublished paper "Towards a Uniform Treatment of Induction - the General Recusion Theorem" in 1995-6. (This was presented at "Category Theory 1995" in Cambridge and part of it appeared in Section 6.3 of my book.) As Mike Barr says, and Gerhard Osius proved in his paper, for "extensional" structures ("well-founded trees subject to the rule that two > chidren of the same leaf cannot be isomorphic"), the structure-preserving map must be a subset inclusion. However, without extensionality, it is a COALGEBRA HOMOMORPHISM. Well founded coalgebras behave like fragments of the initial algebra (the von Neumann hierarchy, in the case of the powerset functor), so their rigidity (lack of endomorphisms) is related to the uniqueness of homorphisms out of the initial algebra. The sense in which coalgebra homomorphisms are like partial algebra homomorphisms is explored in the early sections of my unpublished paper. Osius's recursion scheme has attracted some attention in recent years amongst functional programmers as a way of describing recursive programs. See "Recursive Coalgebras from Comonads" by Venanzio Capretta, Tarmo Uustalu and Varmo Vene, in "Information and Computation" 2006. In fact, the description also works for imperative programs - see Section 2.5 of my book. I have a longer survey of this subject that I intend to publish on "categories" later this month. MY WEB PAGES AT www.cs.man.ac.uk/~pt While I'm here, I'd like to draw your attention to some new things that I have put on my web pages recently. * The slides that I have used at recent conferences and seminars. * The unpublished paper and scanned transparencies of 1995-6 talks on well founded coalgebras. * A new web page for my book, "Practical Foundations of Mathematics", including where to buy it, errata, who has used or cited it, etc. If you have used it in a lecture or seminar series, please send me a URL and your experiences. * The full text of Jean-Yves Girard's "Proofs and Types". * A new version of my TeX package for "commutative diagrams", together with an explanation of the "PostScript" mode, why the "pure DVI" mode is strongly deprecated (NB those long-standing users who have spoiled their otherwise excellent books, papers and online journals by using it), and how to overcome its uglier features if you really insist on using it. * A collection of other TeX macros. * Scanned manuscripts of my 1983 Cambridge Part III Essay (= MSc thesis) (see "domain theory") and undergraduate algebra lecture notes. Paul Taylor
Paul Taylor wrote:
Mike Barr quoted a "thought of Chairman Pratt" that was attributed to him,
Monotone functions respect order, group homomorphisms respect the group operation, linear transformations respect linear combinations, and gangsters respect membership in the Cosa Nostra, but what morphism has ever respected membership in a set? It is sheer hubris for a relation that can't get no respect to claim to support all of mathematics. (Old argument of category theorist Mike Barr, new polemics.)
and commented on it,
That is not a bad rendition (save for the reference to Cosa Nostra) of what I actually said which was that we create these elaborate structures of well-founded trees subject to the rule that two chidren of the same leaf cannot be isomorphic. But then, unlike all other structures that we build, we make no hypothesis that functions preserve the structure. Indeed, I think a structure-preserving map must be the inclusion of a subset. And there are no non-identity endomorphisms.
Of course, I entirely agree with the sentiment that epsilon-structures are completely inappropriate as a basis of most ordinary mathematics.
However, mathematics and mathematicians are contrAry beasts, who treat any statement of the form "there is no such thing as ..." as a challenge, whether it be about membership-preserving functions or the square root of -1.
Indeed, it's quite interesting to look at "carriers equipped with membership relations" in the same way as "carries equipped with group multiplications". This is what I did in my paper "Intuitionistic Sets and Ordinals", JSL 61 (1996).
For a more categorical treatment, we may regard the relation as a coalgebra structure for the full covariant powerset functor. This is what Gerhard Osius did in his "Categorical Set Theory" in JPAA 4 (1974) and what I did for other functors in my unpublished paper "Towards a Uniform Treatment of Induction - the General Recusion Theorem" in 1995-6. (This was presented at "Category Theory 1995" in Cambridge and part of it appeared in Section 6.3 of my book.)
As Mike Barr says, and Gerhard Osius proved in his paper, for "extensional" structures ("well-founded trees subject to the rule that two > chidren of the same leaf cannot be isomorphic"), the structure-preserving map must be a subset inclusion.
However, without extensionality, it is a COALGEBRA HOMOMORPHISM.
Well founded coalgebras behave like fragments of the initial algebra (the von Neumann hierarchy, in the case of the powerset functor), so their rigidity (lack of endomorphisms) is related to the uniqueness of homorphisms out of the initial algebra. The sense in which coalgebra homomorphisms are like partial algebra homomorphisms is explored in the early sections of my unpublished paper.
Osius's recursion scheme has attracted some attention in recent years amongst functional programmers as a way of describing recursive programs. See "Recursive Coalgebras from Comonads" by Venanzio Capretta, Tarmo Uustalu and Varmo Vene, in "Information and Computation" 2006. In fact, the description also works for imperative programs - see Section 2.5 of my book.
I have a longer survey of this subject that I intend to publish on "categories" later this month.
MY WEB PAGES AT www.cs.man.ac.uk/~pt
While I'm here, I'd like to draw your attention to some new things that I have put on my web pages recently.
* The slides that I have used at recent conferences and seminars.
* The unpublished paper and scanned transparencies of 1995-6 talks on well founded coalgebras.
* A new web page for my book, "Practical Foundations of Mathematics", including where to buy it, errata, who has used or cited it, etc. If you have used it in a lecture or seminar series, please send me a URL and your experiences.
* The full text of Jean-Yves Girard's "Proofs and Types".
* A new version of my TeX package for "commutative diagrams", together with an explanation of the "PostScript" mode, why the "pure DVI" mode is strongly deprecated (NB those long-standing users who have spoiled their otherwise excellent books, papers and online journals by using it), and how to overcome its uglier features if you really insist on using it.
* A collection of other TeX macros.
* Scanned manuscripts of my 1983 Cambridge Part III Essay (= MSc thesis) (see "domain theory") and undergraduate algebra lecture notes.
Paul Taylor
Dear Paul, as far as i remember model theorists have an extremely elegant way of comparing structures: no morphisms there but "games" of finite isomorphism extensions (see Fraisse' and Ehrenfeucht for the game aspect or B.Poizat's book) All the first order syntax is subsumed by those games. I quite like categories and for sure I do not know everything, but I have not seen so far a convincing categorical counterpart for these games. (And model theory is good stuff!) Best, Vincent.
My request for precursors to Mike Barr's deprecation of set membership seems to have set loose a thread that has veered off from set theory into model theory. The following extract from the introduction to Gerald Sacks' "Saturated Model Theory" (335 pages, W.A. Benjamin, 1972) serendipitously ties up this loose thread while at the same time promising that category theory offers deeper insight into categoricity, a central notion of model theory, than the alternatives. "It is true that model theory bears a disheartening resemblance to set theory, a fascinating branch of mathematics with little to say about fundamental logical questions, and in particular to the arithmetic of cardinals and ordinals. But the resemblance is more of manners than of ideas, because the central notions of model theory are absolute, and absoluteness, unlike cardinality, is a logical concept. That is why model theory does not founder on that rock of undecidability, the generalized continuum hypothesis, and why the Los conjecture is decidable: A theory T is k-categorical if all models of T of cardinality k are isomorphic. Los conjectured and Morley proved (Theorem 37.4) that if a countable theory is k-categorical for some uncountable k, then it is k-categorical for every uncountable k. The property 'T is k-categorical for every uncountable k' is of course an absolute property of T. The notion of rank of 1-types was invented by Morley to prove Los's conjecture. There are proofs of it that make no mention of rank, but they leave one ill-prepared to prove Shelah's uniqueness theorem (Section 36). I have made rank a central idea of the book, because it is the central idea of current model theory. ... Morley's notion of rank was inspired by the Bendixson differentiation of a closed subset of a compact Hausdorff space; however, the Morley derivative differs from the Cantor-Bendixson derivative in that the former commutes with the inverse limit operation. The Morley derivative is expounded in section 29 as a transformation which acts on functors of a class common in model theory. One advantage of a category theoretic treatment of Morley rank is that it applies equally well to other notions [Shelah] of rank of 1-types. Section 25 reviews the apparatus of category theory needed in section 29." The difference between this recommendation of category theory for model theory and (for example) the literature on accessible categories is that Sacks was not a card-carrying category theorist but a recursion theorist. While category theory has no bias towards Goedel's notion of absoluteness (that I'm aware of), it seems reasonable to infer from Sacks' acceptance of CT that neither is CT biased away from absoluteness but rather is a neutral general-purpose tool. Vaughan Pratt V. Schmitt wrote:
Dear Paul, as far as i remember model theorists have an extremely elegant way of comparing structures: no morphisms there but "games" of finite isomorphism extensions (see Fraisse' and Ehrenfeucht for the game aspect or B.Poizat's book) All the first order syntax is subsumed by those games. I quite like categories and for sure I do not know everything, but I have not seen so far a convincing categorical counterpart for these games. (And model theory is good stuff!)
Best, Vincent.
participants (3)
-
Paul Taylor -
V. Schmitt -
Vaughan Pratt