Does there exist a characterization of Goedel's constructible universe $L$ in purely categorytheoretic terms, or is constructibility an 'artifact' of material set theory? If, in fact, constructibility is an 'artifact' of material set theory, is there a categorytheoretic 'analogue' for $L$?

2$\begingroup$ As far as I know, this is an open problem. $\endgroup$ – Mike Shulman Feb 22 '17 at 3:39

$\begingroup$ @MikeShulman: Has there been any progress made on this 'open problem'? Has there been any interest by categorytheorists in developing such a characterization? $\endgroup$ – Thomas Benjamin Feb 22 '17 at 6:38

$\begingroup$ If, in fact, my question is an open problem, Peter Koepke's work on ordinal turing machines (and the equivalent formulation of $\ast$recursion on $Ord$ provided by Koepke and Koerwien in their paper, "The Theory of Sets of Ordinals") might provide a basis by which this open problem might be solved. $\endgroup$ – Thomas Benjamin Feb 23 '17 at 6:00

$\begingroup$ I don't know of any significant progress. I expect people would be interested in such a characterization. $\endgroup$ – Mike Shulman Feb 23 '17 at 11:59

1$\begingroup$ Yes, of course. There are lots of ways of representing material sets in structural set theory, see for instance ncatlab.org/nlab/show/pure+set or arxiv.org/abs/1004.3802 and references cited therein. $\endgroup$ – Mike Shulman Feb 24 '17 at 18:12
Consider the following statement from Lawvere's paper, "Cohesive Toposes and Cantor's 'lauter Einsen' (Philosophia Mathematicae (3) Vol. 2 (1994), pp. 515):
It might seem that G$\ddot o$del's $L$ would rest, if anything does, on von Neumann's a priori $\epsilon$chains, but that was refuted twenty years ago by William Mitchell who showed how to construct it from a suitable given category, structured only by composition of maps; however, to my knowledge this has not been pursued since.
Though it might not be 'kosher' to answer a question with a question, why does Mitchell's construction not provide the necessary categorytheoretic characterization of $L$ I seek (Mitchell's construction is contained in his papers, "Boolean Topoi and the Theory of Sets" (Journal of Pure and Applied Algebra 2(1972), 261274) and "Categories of Boolean Topoi" (Journal of Pure and Applied Algebra 3 (1973) 193201))?

$\begingroup$ As far as I know, what's involved here is just that membershipbased set theory can be interpreted in appropriate categories of sets, either by using the structure $(\text{TC}(\{x\}),\in)$ from your earlier comment or by using the trees obtained by unraveling this structure. Once this is done, you can just translate traditional set theory (including the definition of $L$) into categorytheoretic language. $\endgroup$ – Andreas Blass Aug 2 '17 at 16:46

$\begingroup$ Technical addendum: The set theory that gets interpreted into the theory of wellpointed topoi with naturalnumbers object is a version of Zermelo set theory (so without replacement) with separation only for formulas with all quantifiers bounded (but the bounds can include power sets, so it's not too weak). The development of $L$ in that theory requires a bit of caution. $\endgroup$ – Andreas Blass Aug 2 '17 at 16:49

$\begingroup$ As a standard comment: one can strengthen the definition of (wellpointed) elementary topos a little to get analogues of the replacement axiom, and Replacement after doing the above construction. Mike Shulman's paper on the stack semantics does this using the concept of autology, though there are other approaches, eg McLarty's. $\endgroup$ – David Roberts Aug 2 '17 at 21:07

1$\begingroup$ The caution that I had in mind comes from the fact that the usual construction of $L$ uses transfinite recursion on the ordinals and thus involves replacement. Without replacement, one needs to work with general wellordered sets rather than von Neumann ordinals, and one needs to formulate the definition of $L$ in a way that doesn't use replacement to justify transfinite recursion. $\endgroup$ – Andreas Blass Aug 4 '17 at 16:24

1$\begingroup$ On your other question, about the weakest set theory needed for a particular theorem, I don't know enough about extremely weak set theories to give you useful information about that. Presumably, you don't need any form of power set, so it would be quite different from what topos theory gives you. $\endgroup$ – Andreas Blass Aug 4 '17 at 16:25