# Second order logic and quantification over formulas

According to Wikipedia second order logic allows quantification over sets of individuals and thus goes beyond first-order logic, e.g. in expressive power.

On the other hand some sort of quantification over formulas is allowed even in first-order theories. Formulas correspond to definable sets, and quantification over formulas (= definable sets) is typically realized by some axiom schema.

In the context of set theory quantification over sets of sets seems to be no problem, because sets of sets are themselves sets and thus belong to the domain of discourse. (Is this correctly stated?) Quantification over arbitrary collections (classes) of sets instead goes beyond first-order set theory. (Does this mean, that the Wikipedia definition is too narrow or even flawed?) But again the result of quantification over definable classes seems to resemble first-order logic.

In another Wikipedia entry one reads, "that quantification over all first order formulas cannot be formalized in the language of [first-order] set theory". A specific example of this fact is, that the notion of "definable sets" (involving an existential quantifier over formulas) is not first-order definable.

Why can some quantifications over formulas be formalized/realized in the language of a first-order theory (e.g. by axiom schemata), and others can not?

• In first-order logic, there is the corresponding notion of "theorem schema", where we have a separate theorem for each definable formula (of whatever type is relevant), and we can prove that our first-order theory can prove each individual theorem. (which, I suppose, would be a "proof schema")
– user14972
Oct 25, 2013 at 9:08

Regarding the second Wikipedia entry, which is about ordinal definable sets, the assertion "quantification over all first order formulas...cannot be formalized in the language of set theory" is wrong in that context. Indeed, in the very same paragraph, existential quantification over the set of formulas is used to define $\text{OD}$, the class of ordinal definable sets.
The reason that the definable sets can fail to form a (definable) class, and that the naive attempt to define $\text{OD}$ does not work, is because the satisfaction relation is not definable, as user39080 points out. We can quantify over formulas $\varphi$ all we want, but after that we can't necessarily say what we want to say about the formula $\varphi$. In special cases such as the definition of $\text{OD}$ we might find a way to say what we want to say about our formulas, but in general the undefinability of satisfaction may cause problems.
If we are dealing with ill-founded models then this quantification may range over nonstandard formulas, as user39080 also points out. However, if we are talking about $V$ (which is of course well-founded) then I think it is fair to say that "$\exists \varphi \in \text{Form}$" expresses quantification over formulas in the same way as "$\exists n \in \mathbb{N}$" expresses quantification over natural numbers, leaving aside the issue of natural numbers versus meta-natural-numbers.