This is a question that I've posed at MathStackExchange, however no answer to it was put forth [there][1], so I'll re-iterate it here with some modification. 

Suppose I have a first-order theory **T**; and let $\phi$ denote some specific formula in one free variable, written the language of **T**; and let $``\psi_1(y), \psi_2(y), \psi_3(y),..."$ be some particular decidable set of formulas in the language of **T** whose free variables are among symbols, $y,x_1,..,x_n$,

Now let **T** have the following extra-logical axioms only:

1. $\exists x: \phi(x)$

2.  $$n=0,1,2,...; i=1,2,3,... \\\forall x_1,..,\forall x_n: \phi(x_1), ...,\phi(x_n) \to \exists y: \psi_i (y) \\ \forall x_1,..,\forall x_n, \forall y: [\phi(x_1)\land...\land  \phi(x_n) \land \psi_i(y)] \to \phi(y)$$

The idea is that **T** only says that there exists an object that fulfills $\phi$, and stipulate a comprehension axiom saying that for any $\phi$ objects there are objects satisfying particular formulas $\psi_i$ parameterized by those $\phi$ objects, and that the resulting objects always satisfy $\phi$ also. The set of formulas $\psi_i$ is decidable, so **T** is effectively generated. 

>My question is that given the above conditions, is there a known extension of first order logic in which the following is provable? $$\sf [\exists H: (H \vdash \forall x: \phi(x)) \land Con(H)] \land Con( T) \\\to Con(T+ \forall x: \phi(x))$$.


My guess is to the negative, but I don't know of a counter-example.

Although the question is put in a general manner, but I'm most interested with the language of **T** being *first order logic with membership $``\in"$.* So the question would turn in this case for whether the above can be interpreted in some known piece of set theory that is thought to be consistent!

>Another related question is if there are no clear counter-examples, what would be the strength of adding such a principle to the ordinary first order logic rules?

I'm also interested about the same question when axiom schema 2 is changed to:

 2.  $$n=0,1,2,...; i=1,2,3,... \\\forall x_1,..,\forall x_n \, \exists y: \psi_i (y)$$

And **T** *proves* that: $$ \forall x_1,..,\forall x_n, \forall y:  \psi_i(y) \to \phi(y)$$

and in particular when we have finitly many $\psi_i$ formulas.


  [1]: https://math.stackexchange.com/questions/4033256/what-counter-example-to-the-following-rule