What are the known conditions for a restriction on naive comprehension that enables a generalization of a property all so constructed sets meet?

Question

Let $\mathcal Q$ be some qualification on formulas in the first order language of set theory (FOL($\in$)), that is met by at least one formula; Let $T$ be the first order set theory whose extra-logical axioms are the following sole axiom schema:

$\mathcal Q$-Comprehension schema: if $\phi(y)$ is a formula that meets qualification $\mathcal Q$, in which $x$ doesn't occur, and in which the symbol $y$ occurs free, and only free; then all closures of: $$\exists x \forall y (y \in x \leftrightarrow \phi(y))$$, are axioms.

Now suppose that $T$ is consistent, and that $\psi(x)$ is some formula in one free variable $x$, and $x$ only occur free in it, and suppose that theory $T$ proves that per the same conditions written above for $\mathcal Q$-Comprehension, all closures of following: $$\forall x [\forall y (y \in x \leftrightarrow \phi(y)) \to \psi(x)]$$, are theorems.

Would it always follow that: $T + \forall x (\psi(x))$ is consistent?

The other question is:

If not, then: are there known conditions that if qualifcation $\mathcal Q$ meets then $T + \forall x (\psi(x))$ would be consistent?

Answer 1

The answer to the first question is no. Suppose no formula meets qualification Q. Let 𝜓(𝑥) be x≠x.

The answer when there is at least one formula 𝜙 that meets qualification Q and the language does not have = as a primitive symbol, is still no. Suppose that the only formulas which meet qualification Q are (y∈y or not(y∈y)), and ∃u(tr(u)∧∀s(s∈y-->s∈u)∧∃s(s∈u∧empty(s))) where tr(u) is ∀w∀v(w∈u∧v∈w-->v∈u) and empty(w) is ∀x(not(x∈w)(that is y is contained in a transitive set which has an empty set as an element). By Q-Comprehension, there is an empty set. A universal set(guaranteed to exist by Q-Comprehension) is a transitive set which has an empty set as an element. Let 𝜓(𝑥) be ∃t(t∈x). Then for this Q, T is consistent(it holds in the 2 element set {a,b} with the binary relation E, where E is defined by xEy iff y=b), ∀𝑥[∀𝑦(𝑦∈𝑥↔𝜙(𝑦))→𝜓(𝑥)] is provable from T for all 𝜙 meeting qualification Q, and 𝑇+∀𝑥(𝜓(𝑥)) is not consistent.