# How to extract the sets "produced" by a axiomatic set theory, into some newly introduced collection?

Say I know well how to reason in a set theory, which for the sake of this question I'll call $\bf{ST}$, say one of those, it can by $\bf ZFC$. It's principally written down via first order logic and it doesn't involve a class of all sets of the theory, like e.g. NBG-set theory does. There is one "biggest" domain of discourse w.r.t. which I'd interpret the quantifiers $\forall$ and $\exists$, but it's not like that's a thing $\mathfrak D$ within the set theory, i.e. one I could use in formulas I reason about.

I don't want to modify the written down axioms, but I want to step back to allow myself more modes of reasoning, adjoin rules etc., because what I want to achieve is define a mathematical object which contains all sets said theory "produces". Produced means all sets the theory says exist, or construct if it's a constructive theory. I.e. I want to capture the logical domain of discourse from before as some sort of class $\mathfrak{U}$. How would I go about doing this?

Attempt: What I'd like do to, but I don't know to which extend this is proper, is the following:

I say my logic allows me to introduce a type/seperate domain $\mathrm{Pred}$ (that feels like a second order act to me, but I don't want to actually use predicates in formulas or derivation, I only need this for one rule), and then I add the rule (don't know for sure if that's the way you write it down)

1) $\large\frac{}{\mathfrak{U}\ :\ \mathrm{Class}}$

2) $\large\frac{\phi\ :\ \mathrm{Pred}\hspace{1cm}{\bf ST}\ \vdash\ \phi(x)}{x\ \in\ \mathfrak{U}}$

Does this work, do I get an object which is equivalent to all the sets my set theory grants existence?

Are there ways to do this without ranging over predicates. I remember one must watch out with the quantifiers and possibly empty variables.

And is that right to write that down with $\vdash$ and frac bars like I did?

I can also introduce a type of sets, but still I don't quite know how to draw the connection.

Again, the motivation is to have $\mathfrak{U}$, whatever sort of object it is, so that I can use, in formulas or my logic of which the set theory is part of "on the side", e.g. "$x\in\mathfrak{U}$" or "$x:\mathfrak{U}$". That $\mathfrak{U}$ doesn't need to be a class too, it was just my first idea. I can use categories too. I know there are theories like ETCS which produce "sets" themselves, but as I said I want to pull the sets out of an established theory to use them in "a zone" which the set theory alone wouldn't have access to. Say I already have a theory of categories, how to "import" the sets granted to exist by my set theory into a class, say given by the $\mathfrak{U}\equiv\mathrm{Ob}_U$ for a category $U$ to be defined?

• Well, one thing you can do is convert a theory of pure sets into one of sets, classes, and possibly semisets, which is equiconsistent to the original set theory and has essentially the same sets. Another is to work in a stronger theory that has something like a Grothendieck universe. Your exposition leans a bit heavily on some notation I find opaque, though, so I'm not sure if these are like what you want. Apr 1 '14 at 19:55
• @MaliceVidrine: Introducing a Grothendieck universe seems, for one, like a move which can't be done so simply, and secondly I think a Grothendieck universe is a set right? If I'm not fixed on the size of the universe produced by the set theory in question, then I don't know how to make a set-universe definition which works in any case. I don't quite want to introduce a whole new set theory, maybe just add a few rules/axioms which one can handle well. Why is the notation opaque? As I said, the $\mathrm{Pred}$ thing was just the way I think about it, the first idea and I don't know better. Apr 1 '14 at 20:04
• The notation's opaque because I can't tell from it what you're trying to say :p Could just be me, maybe it makes perfect sense and is just in a style I'm unaccustomed to. It sounds like you want to be able to have a model of your set theory, but you don't want to strengthen the existing theory or alter the existing axioms. And I'm not sure how you can avoid both. Apr 1 '14 at 20:22
• @MaliceVidrine: Well "model", I don't want to do semantics, I just want to have an expression $\mathfrak{U}$, which I can use in contexts of definitions "let $x\in\mathfrak{U}$ and such that $P(x)$", where the logic I reason with doesn't only contain $x$'s of this set theory but other stuff too. And $\mathfrak U$ should be exactly defined w.r.t. a bunch of other statements which make the axioms of $\bf{ST}$. Since the domain of discourse isn't an object within $\bf{ZFC}$, I can't concisely say what the whole bunch of sets of the theory are. Apr 1 '14 at 21:04
• Right, but you're placing essentially the same demand on the new theory as that it contain a model of the set theory--at minimum a class model. Apr 1 '14 at 21:25

+1 for an interesting question.

Here's an idea to get you started. Let $\frak{U}$ denote the class of all models of $\mathbf{ST}$. Write $x \in \frak{U}$ to mean that $x$ is a family of elements that assigns to every model of $M$ of $\mathbf{ST}$ some element $x_M \in M$. Write $f : \mathfrak{U} \rightarrow Y$ to mean that $f$ is a family of functions that assigns to every model $M$ a function $f_M : M \rightarrow Y,$ perhaps subject to some niceness constraints.

etc.

In the end, we see that:

• there are ways of talking about $\mathfrak{U}$ as if it were a model, despite that it is really a class of models
• since $\mathfrak{U}$ basically is $\mathbf{ST},$ hence there are ways of talking about $\mathbf{ST}$ as if it were a model

I think this is what you're after?

• Thanks for the response. I wonder why not really just say ${\large\frac{{\bf ST}\vdash \phi(a)}{a\in\mathfrak U}}$? Apr 6 '14 at 19:03
• @NiftyKitty95, sorry I do not understand your notation. It seems to read: "Given that $\mathbf{ST}$ proves $\varphi(a)$, we may deduce that $a$ is an element of $\frak{U}$" Apr 6 '14 at 19:17
• That's what I mean, yes. For some predicate $\phi$ my logic recognises. Apr 6 '14 at 19:48