Elwood Wilkins reminds us that...
In his 1974 paper Osius showed that there are enough transitive objects in the initial topos to define a naive set theory. ...
Gerhard Osius's work was significant in 1974 as one of the ways in which it was shown that toposes do the same thing as set theory. In fact Osius's is, so far as I am aware, the only work that discusses *set* theory - Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing as some form of *type* theory. Of course, it is the latter that mathematicians actually use when they claim to be using set theory as foundations, but set theory - epsilontics as Lawvere calls it - is of some interest in the study of very high powered induction. Peter Johnstone included a precis of Osius's paper in his book "Topos Theory" (Academic Press, 1977). Apart from that, I was unable to track down anything that built significantly on it. Indeed, Osius himself didn't seem very interested when I wrote to him about it (he now does statistics). The successor to this paper would therefore seem to be my "Intuitionistic Sets and Ordinals", J. Symbolic Logic, 61 (1996) 705--744 This develops, in a symbolic way, the notions of "transitive set" and "ordinal" in the sense of a carrier equipped with an extensional well founded relation. Several qualitatively different notions of ordinal arise intuitionistically. I also pick up on Osius's set theory and pose some questions that suggest ways of adapting it to Grothendieck toposes in general. What remains of considerable interest (once we have agreed that set theory is wrong, wrong, wrong) is Osius's categorical notion of recursion. The equation f(x) = r( { f(y) | y in [=element_of] x } ) he writes as the (3=1, not 2=2) commutative square P(f) { y | y in x } P(X) ---------> P(A) ^ ^ | | | | | | | | | | r | | | | | | - | f v x X -------------> A which we may of course generalise to a "homomorphism" from any P-coalgebra to any P-algebra, where indeed P may be any functor instead of the covariant powerset functor. The coalgebra admits recursion by definition if there is exactly one such "homomorphism" to any algebra whatever. The exercises in Chapter VI of my book "Practical Foundations of Mathematics" (Cambridge University Press, 1999) explore applications of the commutative square to recursive functional programs. http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s6e.html Osius's 3+1 square is about RECURSION - defining functions or programs - but I have also considered INDUCTION - proving theorems - categorically. Again this is a property ("well foundedness") of coalgebras. See Section 6.3 http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s63.html of the book, or my unfinished paper "Towards a Unified Treatment of Induction" (also known as "On the General Recursion Theorem") which you can get from my Hypatia page http://hypatia.dcs.qmw.ac.uk/author/TaylorP The final section of the book (s96.html) sketches the way in which this categorical notion of ordinal can be used to define transfinite iterates of a functor (for example, internally in a topos). I hope to use this to develop categorical notions of the Axiom of Replacement. Paul Taylor