# Axiom schema of replacement/specification(separation) as second-order

A question to check whether my confusion is correctly removed: how would axiom schema of replacement and specification be written in second-order?

By the way, I know that second-order logic is not reducible to first-order logic, and those matters are irrelevant to this question. Just provide me how these axiom schema would be written as second-order and I would really, really appreciate.

-

The replacement axiom as second-order would be something like this:

\begin{align} \forall F\forall p_1\ldots\forall p_n\forall A(&\forall x(x\in A\rightarrow\exists y(F(x,y,p_1,\ldots,p_n)\land\forall z(F(x,z,p_1,\ldots,p_n)\rightarrow z=y))\rightarrow\\ &\exists B\forall u(u\in B\leftrightarrow\exists v(v\in A\land F(v,u))) \end{align}

We say that for every $F$ which defines a function (up to parameters $p_i$'s) on a set $A$, there is a set $B$ which is the image of $A$ under the function $F$ (with the parameters $p_i$).

The difference between the first-order schema and second-order axiom is that $F$ quantifies over all classes, even those not defined by a formula. The result is that we have a single axiom, instead of "a lot of them".

Note however, that second-order relies on the notion of a set to be well-defined so doing second-order set theory is a bit... awkward because usually define sets as objects in a universe of set theory, and this causes a bit of circularity.

This is somewhat similar to the difference between first-order and second-order induction in Peano Axioms, you can read some about this in here: Axiom schema and the definition of natural numbers

-
Thanks, Asaf. Now my confusion is all cleared :) –  user32751 Jun 3 '12 at 10:21