Take [second order logic](https://plato.stanford.edu/entries/logic-higher-order/), weaken the [comprehension axiom schemata](https://plato.stanford.edu/entries/logic-higher-order/#AxioSecoOrdeLogi) to using only FIRST order formulas; that is, $\phi(x\_1,..,x\_n)$ in the referred article is restricted to be a first order formula. Keep all the other aspects of second order logic.



> 
> Now would the resulting system be a kind of a conservative extension of first order logic? That is, a logic that allows quantification over relation and function symbols, yet not having axioms extra to those of first order logic, and so enjoys the merits of first order logic.
> 
> 
> 



> 
> Can we always add a first order theory, but write its schemas as SINGLE axioms in that logic? So for example separation schema in Zermelo would be written as a single axiom by quantifying over predicates, as: $$\forall P \forall A \exists X \forall y (y \in X \leftrightarrow y \in A \land P(y))$$
> 
> 
> 


I had asked a similar question on MathStackExchange, and I received no answer?



IF we weaken comprehension of second order logic to first order formulas, would the resulting system be a conservative extension of FOL?
Preliminary remark: after some clarification in the comments, I am posting my comment as an answer.


Let $\varphi$ be a first-order formula which is proved in your Hilbert style system $S$. Let $M$ be a first-order structure (adapted to the appropriate first-order language). From the completeness of first-order logic, it is enough to show that $M$ satisfies $\varphi$. Add to $M$ all first-order definable relations and functions, obtaining $M^∗$. All axioms and rules of your weakened second-order system $S$ are valid in $M^∗$ (Henkin semantics), so $M^∗$ satisfies $\varphi$ by soundness. Since $M$ is a reduct of $M^\*$ and is adapted to the language of $\varphi$, $M$ satisfies $\varphi$.


