# IF we weaken comprehension of second order logic to first order formulas, would the resulting system be a conservative extension of FOL?

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))$$

• Could you state the list of axioms of your second-order logic? For example, does it contain the axiom of choice $\forall x\exists y R(x,y)\to \exists f \forall x R(x,f(x))$? Commented Aug 22, 2020 at 18:09
• Let $\varphi$ be a first-order formula which is proved in your system. Let $M$ be a first-order structure (adapted to the appropriate first-order language). It is enough to show that $M$ satisfies $\varphi$. Add to $M$ all first-order definable relations, obtaining $M^*$. All axioms and rules of your weakened second-order system are valid in $M^*$, so $M^*$ satisfies $\varphi$. Hence $M$ satisfies $\varphi$. Commented Aug 23, 2020 at 14:17
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$$.