 We will now describe a theory PFO of plural first-order quantification based on the language \(L_{\textrm{PFO}}\). Let’s begin with an axiomatization of ordinary first-order logic with identity. For our current purposes, it is convenient to axiomatize this logic as a natural deduction system, taking all tautologies as axioms and the familiar natural deduction rules governing the singular quantifiers and the identity sign as rules of inference. We then extend in the obvious way the natural deduction rules for the singular quantifiers to the plural ones. Next we need some axioms which for suitable formulas \(\phi(x)\) allow us to talk about the \(\phi\)s. In ordinary English the use of plural locutions generally signals a concern with two or more objects. But the existence of two or more objects may not be semantically required; for instance, “The students who register for this class will learn a lot” seems capable of being true even if only one student registers. It is therefore both reasonable and convenient to demand only that there be at least one object satisfying \(\phi(x)\). (Most people who write on the subject make this concession.) This gives rise to the plural comprehension axioms, which are the instances of the schema