Quantification theory, or the first-order predicate calculus, is ordinarily so formulated as to provide as theorems all and only those formulas which come out true under all interpretations in all non-empty domains. There are two strong reasons for thus leaving aside the empty domain.(i) Where D is any non-empty domain, any quantificational formula which comes out true under all interpretations in all domains larger than D will come out true also under all interpretations in D. (Cf. [4], p. 92.) Thus, though any small domain has a certain triviality, all but one of them, the empty domain, can be included without cost. To include the empty one, on the other hand, would mean surrendering some formulas which are valid everywhere else and thus generally useful.(ii) An easy supplementary test enables us anyway, when we please, to decide whether a formula holds for the empty domain. We have only to mark the universal quantifications as true and the existential ones as false, and apply truth-table considerations.Incidentally, the existence of that supplementary test shows that there is no difficulty in framing an inclusive quantification theory (i.e., inclusive of the empty domain) if we so desire. A proof in this theory can be made to consist simply of a proof in the exclusive (or usual) theory followed by a check by the method of (ii). We may, however, be curious to see a more direct or autonomous formulation: one which does not consist, like the above, of the exclusive theory plus a rule of expurgation. And, in fact, such formulations have of late been forthcoming: Mostowski [5], Hailperin [3], and, as part of a broader context, Church [2]. I shall not presuppose acquaintance with these papers, except in my final paragraph (and then only with [3]).
A decision procedure for a class of formulas of first order predicate calculus
