Abstract

This chapter is devoted to the excruciating drudgery of a logical monk actually doing the work that a logical saint would find unnecessary, to establish the metatheorem which states that for all _n_, and for all substituends for Φ, one has _ ∇ n x Φ x ⊣ ⊢ ⋄ n x Φ x. Note that although for any particular n_ one can effectively find the requisite proofs in monadic first-order logic, the proof of the metatheorem itself, because of its general form, does not proceed within monadic first-order logic. An important philosophical corollary of this metatheorem is that no ordering of the Φ s—be it one intrinsic to them, or imposed upon them arbitrarily in the act of counting—can possibly figure into the truth-conditions of numerosity statements to the effect that ‘there are exactly this-many Φ s’.