# What's the point of allowing only quantification of variables in first-order logic.

In first-order languages, ${\forall}$ is allowed to quantify only over variables, so that ${\forall}v(P)$, where $v$ is some variable and $P$ is a WFF is the only kind of a WFF concering universal quantifiers allowed in such languages.

Why is that? No texts I read on this subject (which due to the limitations I have due to the place I live have only been sites like Wikipedia, Proofwiki or Wolfram MathWorld) provided an explanation why quantifying over WFFs is not allowed. I don't see any advantages to this and it leads to annoying problems like ZFC being an infinite list of axioms, which don't avoid the concept of ${\forall}P(Q)$, $P$ and $Q$ being WFFs, just phrase it in another way.

So what's the justification of not quantifying over WFFs? What are the advantages of such approach?

• Because when you allow quantification over other elements of the language you're no longer in first-order logic, but rather second- or higher-order logic when you can quantify over predicate symbols, predicate-of-predicate symbols, etc. Note that what you propose is not quantifying over WFFs: it's not typical to allow the language to talk about its own WFFs and syntax in that way. In 2nd order logic, a new set of variables is introduced, $P^n_m$, interpreted as subsets and more generally relations of individuals that the variables $v_i$ range over. <cont> Commented Apr 17, 2016 at 18:22
• <cont> Just as you can substitute terms for free 1st order variables, in 2nd order logic you can substitute formulas for free 2nd order variables. The rules for doing so are rather complicated; they're spelled out in Church's 1930s book on mathematical logic. Commented Apr 17, 2016 at 18:24
• I know that it's not allowed in first-order logic. Why though? Why didn't people define first-order logic as allowing this? By my example it seems that it would have been pretty helpful. So why didn't they? Commented Apr 17, 2016 at 18:24
• The point is that FOL is defined to be the thing that you get when you only quantify over variables. If you want to quantify over other things, that's called HOL. So we can in fact quantify over other things, but when we want to avoid all the issues that entails, we can revert back to only quantifying over variables, and we have decided to call this First-Order Logic. Commented May 21, 2016 at 22:08

It's because when we do allow broader scopes of quantification, things get extremely ugly.

One extremely important fact about first-order logic is that it has a reasonable notion of proof: if I want to know whether $\varphi$ is true whenever each sentence in $\Gamma$ is true - that is, if $\Gamma\models\varphi$ - I just look for a proof of $\varphi$ from $\Gamma$. The crucial facts about proofs are:

• A proof is finite (in particular, can be represented by a single natural number).

• I can identify proofs (so the set of numbers corresponding to valid proofs is computable).

Passing to stronger logics tends to kill this property: in particular, second-order logic - which I think is the natural setting for what you're describing - provably has no good proof system! In fact, I can write down a second-order sentence which is valid (= true in every model) iff the Continuum Hypothesis is true! So, determining what constitutes a proof in second-order logic requires us to first make strong set-theoretic commitments - which is putting the cart before the horse a bit!

This is not to say that stronger logics are uninteresting (see Barwise and Feferman's book Model-Theoretic Logics), merely that they lack nice properties which make first-order logic manageable (the other main property being the Lowenheim-Skolem property, which is a bit more technical). In fact, we can characterize first-order logic as the strongest logic satisfying a couple nice properties (this is Lindstrom's Theorem). So there's a trade-off to be made, in choosing what logic to use.

• What are ${\Gamma}$ and ${\phi}$? Commented Apr 17, 2016 at 18:42
• @user1321213 $\Gamma$ is a theory (that is, a set of sentences) and $\varphi$ is a sentence. So, e.g., $\Gamma$ could be ZFC and $\varphi$ could be "Every field has an algebraic closure." Note that, while ZFC is an infinite theory, any specific proof from ZFC uses only finitely many axioms, which is part of what makes it palatable. Commented Apr 17, 2016 at 18:49
• @user1321213 I just realized I forgot to mention this: the study of non-first-order (but still classical) logics is called abstract model theory. It's not as much in vogue these days (at least, that's my understanding), but there's a lot of really interesting old papers on the subject. Commented Apr 18, 2016 at 8:47
• @Noah: although as one of my colleagues pointed out when I studied (plain) model theory as an undergrad, it should probably be called "theory theory". Considering models first is also rather putting the cart before the horse since proofs manipulate statements in the theory rather than entities in the model ;-) Commented Apr 18, 2016 at 9:44

Because when you allow quantification over other elements of the language you're no longer in first-order logic, but rather second- or higher-order logic, where you can quantify over predicate and relational variables, predicate-of-predicate variables, etc.

Note that what you propose is not best thought of as quantifying over WFFs: it's not typical to allow the language to talk about its own WFFs and syntax in that way. In 2nd order logic, a new set of variables is introduced, $P^n_m$ (= the $m$-th variable for an $n$-ary relation), interpreted as subsets and more generally relations of individuals that the variables $v_i$ range over.

Just as you can substitute terms for free 1st order variables, in 2nd order logic you can substitute formulas for free 2nd order variables. The rules for doing so are somewhat complicated; they're spelled out in Introduction to Mathematical Logic by Alonzo Church (first published in 1944, revised in 1956).

There are very good reasons to isolate first order logic as a thing in itself, worthy of attention and study. One is that it's sufficient to formalize traditional logic, a la Aristotle, and even the logic of relations as developed in the 19th century by Schroder and others. Another reason is that first order logic has many "nice" properties (completeness, compactness) which none of the higher-order logics enjoy.

2nd and higher order logics are indeed helpful and very expressive -- they can capture distinctions in natural language which first order logic can't. But higher order logics are very different beasts: they lack the nice mathematical properties possessed by first order logic. For example, there is no complete deductive system. They're really a form of set theory — "set theory in sheep's clothing", as Quine put it. In fact, the "theory of types", Russell & Whitehead's system that provided a foundation for mathematics in a higher order logic, predates Zermelo's set theory by a decade or so. Russell maintained that this established that mathematics is logic, a philosophy of math subsequently known as logicism; but current consensus is that Russell & Whitehead accomplished a reduction of mathematics to set theory, and not to what's commonly accepted as "logic".

• Church's book was published in 1944 and revised in 1956. press.princeton.edu/titles/291.html "This volume . . . is a reprint of the revised 1956 version of this notable title first published in 1944 in the Annals of Mathematics Studies".
– chx
Commented Apr 18, 2016 at 2:55
• @chx Thanks, I don't have my copy here. It reads like a 30s book :) and perhaps he began it then. Commented Apr 18, 2016 at 8:45
• @chx Originally it was "Vol. 1" of a planned 2-volume work. The second volume was to cover "the functional calculus" of higher order, but sadly it never appeared. Church's formulation of type theory is quite elegant, presented in a paper by him and explored in papers by his students Henkin and Andrews. An interesting twist: it also has propositional variables, and allows quantification over them. Commented Apr 18, 2016 at 8:57

There's nothing inherently wrong with quantifying over propositions, as in your $\forall P$ quantifiers.

However, a logic is, by definition, "first-order" if quantification is restricted to variables ranging over the universe of discourse, only. Quantifying over subsets of said universe, over predicates, over propositions, etc. makes the logic "higher-order" instead.

In first order logic, we get some metatheoretic results which fail in higher order logics. For instance, we get soundness and completeness: the provable formulae are exactly those which hold in all possible models. In higher order logics, usually only soundness holds: provable formulae are true in all models, but there are some formulae which do hold in all models yet can not be proved by the logic.

Also note that, if you have a formula $\phi(P)$ which depends on $P$ in an extensional way, i.e. $$(P_1 \iff P_2) \implies (\phi(P_1) \iff \phi(P_2))$$ then the quantification $\forall P.\ \phi(P)$ can be expressed in FOL as $$\phi({\sf true}) \land \phi({\sf false})$$ The above "encoding" of the universal quantifier relies of the classical tautology $$(P \iff {\sf true}) \lor (P \iff {\sf false})$$ Hence, at least for this case, we get an equivalent first-order formalization.

You can actually have formulas like $\forall P. \textbf{Apply}(P,x)$ (where $\textbf{Apply}$ is your predicate symbol that you want to denote the application of the predicate $P$ to $x$) in a first order logic with two type of variables. The problem is there can be nothing in the rules implying that the variable $P$ must range on fbf's, strings, sets or numbers: it will depend on your model.