# First-order logic and second-order logic confusion

First-order logic uses only variables that range over individuals (elements of the domain of discourse); second-order logic has these variables as well as additional variables that range over sets of individuals. For example, the second-order sentence $\forall P\,\forall x (x \in P \lor x \notin P)$ says that for every set $P$ of individuals and every individual $x$, either $x$ is in $P$ or it is not (this is the principle of bivalence). ("Second-order logic", Wikipedia)

And

In the formal language of set theory, the axiom schema is: $\forall w_1,\ldots,w_n \, \forall A \, \exists B \, \forall x \, ( x \in B \Leftrightarrow [ x \in A \land \phi(x, w_1, \ldots, w_n, A) ] )$

Comparing and contrasting these two, I find that in the latter case, set $A$ can be considered as set of individuals that was quanitifed by universal quantifier. So, how is this different from second-order logic (in the first case, I would be referring to set $P$.)?

Usually we say that first-order quantification is to quantify over elements of the universe, while second-order allows quantification over subsets. However we can only think of second-order quantification as quantifiers over predicates and relations instead.

Why would we want to do that? Well, it removes the ambiguity about "sets" when it comes to set theory in which elements of the universe are subsets of the universe.

What does that mean? It means that second-order quantifications in ZFC are quantifiers over classes and not over sets. This is what makes ZFC a suitable foundation for mathematics, as it turns high-order logic into first-order logic, and first-order logic is good.

• So you mean that even in first-order logic, we can allow first-order logic to quantify over sets of individuals - set $A$ in the quoted axiom of specification (when the thing quantified is not a non-set class)? Jun 3, 2012 at 7:13
• Just to be sure I'm understanding this, would the following then amount to such a 2nd order statement: $\exists g, \forall f . g(f) => \forall x,y . f(x)=f(y)$ ? Jan 5 at 19:45