Take second order logic, weaken the comprehension axiom schemata 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?

5more comments