A proof procedure for quantification theory

The purpose of this paper is to present and justify a simple proof procedure for quantification theory. The procedure will take the form of a method for proving a quantificational schema to be inconsistent, i.e., satisfiable in no non-empty universe. But it serves equally for proving validity, since we can show a schema valid by showing its negation inconsistent. Method A, as I shall call it, will appear first, followed by a more practical adaptation which I shall call B. The soundness and completeness of A will be established, and the equivalence of A and B. Method A, as will appear, is not new. The reader need be conversant with little more than the fairly conventional use (as in 8) of such terms as ‘quantificational schema’, ‘interpretation’, ‘valid’, ‘consistent’, ‘prenex’, and my notation (as in 7) of quasi-quotation.