ABSTRACT
This chapter explains how an invalid argument form may be proved to be invalid. In respect of distinctively quantificational forms, however, the most important class for which there is a decision procedure available are monadic forms. A suitable method is this: immediately to the left of each quantifier draw a vertical line and at right-angles draw a line exactly covering the formula governed by the quantifier. In dequantification for a formula F which is governed by a quantifier another formula is found which is free of that quantifier and yet is equivalent to F with respect to the universe in question. Decision procedures are known for various other important classes of quantificational forms. For the many quantificational forms which are governed by a quantifier, and contain that governing quantifier only, dequantification is the only one of the three operations which is needed.
