Familiarity with classical quantification theory is presupposed here. Some proposed amendments are considered, as are several additions.

Alternatives to Classical Quantification Theory

First-order logic can be reformulated so as to avoid quantifiers and variables. This is only partially done in modal logic, which avoids explicit quantification over possible states of the world in favor of operators □ and ♢. However, in principle all quantification is avoidable, if one is willing to admit enough operators and does not worry about their having ordinary-language readings. In practice, however, few have preferred this predicate-functor approach (see Quine 1960, Benthem 1977). Thus, even such dissidents as the intuitionists adopt the classical quantificational language, though the properties they ascribe to the quantifiers are nonclassical. (Thus, while classically ∀ and ¬¬∀ and ∀¬¬ are equivalent, intuitionistically the first is stronger than the second and the second stronger than the third.)

Classical logic allows terms formed...