Standard propositional logic contains no quantifiers. It simply replaces sentences with propositional variables (“schematic letters”) that remain unbound. But there is nothing to prevent us from introducing quantifiers that bind these variables, ranging over propositions. These can be objectual or substitutional, according to taste. They will be read “for all p” and “for some p”. One might well think this enrichment was implicit all along, since the standard formulas are intended to express generality; that is why they contain variables not actual sentences. If we say “p and q entails p”, we mean to express the proposition that for any propositions p and q, if p and q, then p. Generality implies quantification. Adding the quantifiers will increase expressive power, but not beyond what was there all along. Thus, we can envisage two styles of propositional logic—quantified and unquantified. Each is legitimate and each can be studied in its own right. One might well regard the quantified form as more intuitive and natural; we can say things like “Every proposition has a negation” if we avail ourselves of this resource. In the case of predicate logic, as standardly rendered, we already have quantifiers built in: they bind the individual variables used to analyze the structure of whole sentences (along with predicate letters). But this is not essential to predicate logic as such: we could construct a notation that omits quantifiers and simply deals in formulas such as “Fx” and “not-Fx”. That is, we could do what we already do in propositional logic—write formulas that contain only unbound individual variables. This would be a quantifier-free predicate logic. The concepts of predicate logic and (first-order) quantificational logic are different concepts–just as propositional logic is different from quantified propositional logic. Adding quantifiers increases expressive power in both cases, though it is natural to suppose that this was implicit all along. Why not treat the two cases as essentially alike? As things are, we don’t, but this seems arbitrary—perhaps betraying dark suspicions about propositions as values of variables. In both cases we trade constants for variables, which allows for generality, and then introduce quantifier expressions to obtain the necessary expressiveness. But that is not the end of the line: we also have predicate expressions to deal with. They too have been introduced to allow for generality: instead of “red” and “square” we have “F”, intended to stand in for any natural language predicate. First-order predicate logic leaves these unbound, but there is nothing compulsory about this; there is nothing ill-formed about binding these variables with a quantifier. If we do, we get second-order predicate logic—where now the variables range over properties or some such. We have gone from an unquantified logic to a quantified logic—just as in the other two cases. And this was implicit all along in view of the generality conveyed by the usual formulas. So, now we have three sorts or levels of quantification: over propositions, over individuals, and over properties. Fine—we have such things to talk about and we want to make general statements about them. That is what the logical notation is designed to do. Is that the end of the line for quantification? No, because there remain constants not yet converted to variables that we also want to generalize about, viz. truth-functional connectives. We could introduce a variable over truth-functions, say T: then we could say things like “For any truth-function T, T is expressible in standard propositional logic”. We are quantifying over truth-functions, just as we quantified over propositions, individuals, and properties. This could be called “Quantified Truth-Function Theory” and added to the curriculum. We might think of it as involving third-order quantification. Now we have a fourth type of logic (or logical notation) to be added to the previous three. Each type is a counterpart to the quantifier-free logic that exists alongside it, and is a natural extension of it. Is that the end of the line for quantifiers? Not quite, because we still have one more type of constant left—the quantifiers themselves. Can’t these also be gathered under a suitable variable, thus allowing for generalized statement? Thus, we can say “For all quantifiers Q, Q admits of quantifier nesting”. This quantifier might range over the two standard quantifiers “all” and “some” or it could include the so-called non-standard quantifiers like “most”, “many”, “several”, “a few”, etc. The motivation is the same as before and so is the procedure: we want to talk generally so we replace constants with variables and introduce the necessary quantifier—in this case a quantifier over quantifiers. Thus, we obtain a quantified quantifier logic; we could think of it as concerned with the logic of second-level functions a la Frege, i.e., functions from first-level functions (corresponding to predicates) to truth-values. This we could describe as fourth-order logic—one step up from the logic of truth-functions. And with that we have covered all the constants that occur in the formulas of predicate logic; there is nothing left to quantify over. We now have five levels of quantified logic applicable to quantification over propositions, individuals, properties, truth-functions, and quantifiers themselves (construed as second-level functions). Each level has a non-quantificational counterpart—a logical system that lacks the quantifiers contained in its more expressive twin. This is the right way to understand the structure of the logical universe, not the familiar division into non-quantificational propositional logic and quantified first-order predicate logic. That is just a partial glimpse of full logical reality, an oversimplification of the space of logical systems.
 Of course, we must also add modal logic (and perhaps other types of logic), which invites new quantifiers and variables so that we can generalize about modal categories, as in “All modal operators M admit of nesting with other modal operators”. Quantifiers are not limited to the role they play in standard first-order logic; they crop up everywhere. Quantifier pluralism is the way to go.