FOM: Re: categorical (pseudo) foundations

[Colin McLarty]

Vaughan Pratt hypothesized that from a categorical (or, little green
critter's) point of view:

>"By far the most
>interesting thing about set theory is functions."

Harvey Friedman replied:

>This is not a proper analogy. A better one is "By far the most interesting
>thing about set theory is the comprehension principles."

        Dedekind and Cantor both thought functions the interesting thing
about sets and formulated their theorems and open questions in terms of
functions. Comprehension principles gained prominence decades later. This
proves nothing decisive, but I'd be very happy if the worst charge made
against categorists were: we no have no better motivated picture of set
theory than Dedekind or Cantor did.


        I gave the abstract of Robert Rosebrugh and R. J. Wood's
characterization of the categories equivalent to Set, to which Vaughan replied: 

>>>If a category B with Yoneda embedding Y : B ---> CAT(B^op,set) has an
adjoint >>>string, U -| V -| W -| X -| Y, then B is equivalent to set.
>
>To what extent does this (extremely nice) universal property of Set
>(synonyms: "set", "sets") really characterize Set?  The difficulty is that
>"Set" appears in the antecedent.


        Yes, the bearing on fom is only that this characterizes one sweeping
family of universal properties of Set. It is not per se a foundational
characterization. 

        Note that in ZF set theory too, if you want to characterize not just
"models of ZF" but "models with the same ordinals as U" where U is a
parameter over models of ZF, then you need to use U in the definiens. This
result does not characterize "models of categorical set theory" but "models
equivalent to the given Set" (which implies having the same ordinals, same
degree of failure of V=L, et c).   


>Had the theorem read
>
>>>If a closed category B with Yoneda embedding Y : B ---> CAT(B^op,B) has
>>>an adjoint string, U -| V -| W -| X -| Y, then B is equivalent to Set.
>
>then this would be a *somewhat* better characterization.  (Note that the
>singleton category B=1 with the evident closed structure satisfies the
>condition.  Ruling out this case would be like including Consis(T) as an
>axiom of T.)

        The note is a good general point. All universal mapping properties
are exemplified in the singleton category. So set theory on this approach
will also need a non-triviality condition.

        The further questions Vaughan raises are interesting but I don't
know much about them. 

Colin