Re: no membership-respecting morphisms

Re: no membership-respecting morphisms

[V. Schmitt]

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.

Re: no membership-respecting morphisms

[Vaughan Pratt]

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.

no membership-respecting morphisms

[Paul Taylor]

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