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?
+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:
I think this is what you're after?