Published online by Cambridge University Press: 12 March 2014
The logic of quantification is conveniently developed in terms of the so-called quantificational schemata. The atomic quantificational schemata consist each of a schematic predicate letter (‘F’, ‘G’, etc.) attached to one or more quantifiable variables (‘x’, ‘y’, etc.). Compound quantificational schemata are built up of these atomic ones by means of truth functions and quantifiers. The business of the logic of quantification then becomes that of spotting the valid schemata: the ones that are true under all interpretations.
The logic of quantification is well understood and well behaved. Proof procedures in this domain are known, thanks to Gödel, to be complete. If decision procedures are not known for the whole of this part of logic, still we do know, thanks to Church, that they cannot exist. And we know how to streamline our proof procedure for quick success in the average case where proof is possible. Because of all this, there is a premium on adapting special theories, of special subject matters, to this general mold. This means representing the truths of the special theory as a class of quantificational schemata with interpreted predicate letters and a chosen universe of discourse. Once a theory has been thus regimented, it is a standard theory (in approximately Tarski's sense of the term).