Category Theory and Hereditarily-Finite Sets

Category Theory and Hereditarily-Finite Sets

[Galchin Vasili]

Hello Cat Theory Community,

     Hereditarily-finite sets are becoming increasingly more popular in
computer science research.

1) What kind of interesting categories exist where an 
     "object" is a hereditarily-finite set plus some 
     structure on the set and a "morphism" would be a
     structure-preserving function. (I can think
     of the obvious subcategory of SET and also the 
     category where an object is a hereditarily-finite
     set together with a "SET" endomorphism on that 
     set, but neither of these categories would have 
     interesting or useful properties, in my opinion)
     

2) What kind of papers can I read on this subject?

Regards,

Bill Halchin

Re: Category Theory and Hereditarily-Finite Sets

[Wilkins E B]

Paul Taylor wrote:

> > Hereditarily-finite sets are becoming increasingly more popular
> > in computer science research.
>
> Why?  Because some ill-advised first year maths lecturer told you that
> the element relation was the foundation of mathematics, maybe?

Maybe because someone read papers by Friedman (1977) which gave the set
theory B which is [Beeson] "the theory of hereditary extensional sets of
finite rank" and which is strong enough to model Bishop-style constructive
mathematics. This seems to be a good reason.

Elwood

--
 Dr Elwood Wilkins          tel:  (+44) (0)1206 872771
 Senior Research Officer    fax: (+44) (0)1206 872788
 Department of Computer Science
 University of Essex, Colchester, Essex, UK

Re: Category Theory and Hereditarily-Finite Sets

[Paul Taylor]

> Hereditarily-finite sets are becoming increasingly more popular
> in computer science research.


Why?  Because some ill-advised first year maths lecturer told you that
the element relation was the foundation of mathematics, maybe?

> "object" is a hereditarily-finite set plus some structure on the set
> and a "morphism" would be a structure-preserving function.

If you're really interested in heredity, so the "structure" is the
element relation, this is a well-founded coalgebra for the covariant
powerset functor.

Coalgebras for the powerset functor were first studied by Gerhard Osius
in JPAA in 1974, although he considered recursion rather than induction.

Well founded coalgebras for general functors (but with some emphasis
on the powerset) are defined in Section 6.3 of my book "Practical 
Foundations of Mathematics" (Cambridge University Press, 1999).

The exercises for that chapter show how various ideas with recursive
programs may be expressed in these terms.  In particular, unary
recursion (with at most one recursive call at each level) is reduced
to tail recursion (equivalent to while programs) together with an
accumulator monoid.

Paul