# Languages with quantification over *formulas*?

The 4th page of this paper mentions:

A first-order language that contains “substitutional quantifiers” (with formulas as substituends) in addition to ordinary quantifiers turns out to be precisely the sort of “infinitary” language that we need

So, it seems to be describing a sort of extension of first-order logic where you can quantify over formulas (in addition to the normal quantification over elements of the “universe of discourse”), but little detail is provided.

What exactly is this language (or class of languages)? Does anyone know of a book or something that talks about this in more detail?

• Second-order or higher-order logic. Commented May 17 at 8:44
• It seems a way to "embed" axiom schema into object language; see example: $S$ is true iff $\forall p ( \text {if } S='p', \text { then } p)$. Commented May 17 at 8:47
• Well, second-order logic allows quantification over subsets, but it’s not clear to me that this is the same as quantification over formulas. For example in ZFC, not every FOL formula defines a subset (it may define a proper class)
– NikS
Commented May 17 at 8:51
• Maybe useful this post. Commented May 17 at 9:25
• The thing you're looking for is called second-order propositional logic. The name is a bit misleading, in that you can have a version of this logic that includes first-order quantifiers too (and is therefore a proper predicate logic), but that's how we distinguish it from the kind of second-order logic that model theorists like to study, which quantifies over sets. Commented May 17 at 9:47