Can we have a nearily unrestricted class comprehension over predicates that do not mention the class membership symbol

Suppose that $T$ is a consistent first order theory. Now let the language of $T$ be $L_T$.

Question: is it always consistent to add a new primitive constant $D$, and a new primitive binary relation $\in^*$ called 'class membership', and add a new symbol $\epsilon$ and axiomatize that for each formula $\phi$ the string $\epsilon \phi$ is a term of the language, and add the following schema to all axioms of $T$ bounded $\in^* D$

If $\phi$ is a formula in $L_T$ in which all and only $y,w_1,..,w_n$ occur free, and only occur free, and if $\phi^D$ is the bounded $\in^* D$ form of the formula $\phi$, then:

$\forall w1,..,wn \in^* D \ \forall y (y \in^* \epsilon (\forall y\phi^D )\leftrightarrow \phi^D)$,

is an axiom.

• What does it mean for a first-order theory to have axioms "presented in unbounded form"? What is a "primitive" constant (as opposed to just a constant)? What is a "primitive" binary "class" membership relation? You say $\epsilon\phi^D$ is a "term", but I think you want to add this as a function symbol. It seems you want to add objects representing the various definable classes, like a Henkin model. Is that right? I guess you'd want to replace the axioms $\phi$ of $T$ with the axioms $\phi^D$, right? – Joel David Hamkins May 25 '18 at 23:37
• @JoelDavidHamkins, primitive constant is just written to ensure that it is not a definable constant in $L_T$. 'class membership' is the name given to the symbol $\in^*$, I will rephrase it to make it clearer, what I wanted to say is to add a new primitive binary relation called "class membership" symbolized as $\in^*$, and yes I want to add objects representing the various definable classes through a function symbols on their defining formulas, also I want to add that schema of the bounded axioms of $T$. where the bound is $\in^*$ after each quantifier of axioms of T. – Zuhair Al-Johar May 26 '18 at 9:09
• @JoelDavidHamkins, unbounded presentation means that not all qunatifiers are bounded, like how ZFC is usually presented, while a bounded presentation means all of the quantifiers are relativized to be $\in^*$ a bounding class which is here $D$ – Zuhair Al-Johar May 26 '18 at 9:14
• According to that meaning, it seems to me that every first-order theory $T$ in language $L_T$ is presented in unbounded form, since by design $\in^*$ was chosen not in $L_T$, and so no assertions of $T$ have $\in^*$-bounded quantifiers. – Joel David Hamkins May 26 '18 at 10:27
• what I meant is that the theory must not have bounded quantifiers of the form $\forall x \in M$ or $\exists x \in M$, not necessarily just bounding by $\in^*$, but anyhow I think it is just a cosmetic requirement to make the bounding by $\in^*D$ looks simpler, we can really do that $\in^*$ bounding easily even on top of bounded axioms as far as the original bounding relation in axioms of $T$ is not $\in^*$. [because as you said $\in^*$ is new anyway].Thanks – Zuhair Al-Johar May 26 '18 at 14:40

If I understand you correctly, the answer is yes, providing that you don't just add those axioms directly to $T$, but instead add the assertion $\phi^D$ for each axiom of $T$.
Your theory is simply the syntactic analogue of taking a model $M$ in the language $L_T$, and adding a second-order part with an object representing each definable subset of $M$ (allowing parameters). Thus, the extension of $D$ is simply the original model $M$; the interpretation of $\epsilon\phi$ is the function mapping the parameters to the class defined by this formula, and so on. This natural interpretation of your theory shows that any model $M$ of $T$ can form the $D$-part of a model of your new theory. This argument also shows that the new theory is conservative over $T$ for assertions in the language of $L_T$ relativized to $D$.
• You said the extension of $D$ is simply the original model $M$, but for some theories can't we have models where $D \in D$? – Zuhair Al-Johar May 27 '18 at 18:07