Previous: Quasi-identity logic

Next: Downward Löwenheim-Skolem Theorem

Up: Supplementary Text Topics

Calculus of Classes II: Expressive power in the Calculus of Classes

Now we return to the Calculus of Classes studied in Chapter I of LMCS to look at what a first-order formula can say about the classes .

Quantifier-free formulas

Given an equation we can find an equivalent equation (using symmetric difference) . Then using complete expansion we can assume p is a disjunction of constituents . Thus we see that

every equation (or set of equations) is simply an assertion about certain constituents being empty.

(One can apply the same to any quantifier-free positive formula.) Thus an equation follows from others iff each constituent forced by the conclusion to be empty is a union of the constituents which the premisses force to be empty.

To handle the syllogisms within the logic of classes one needs negation. Adding this to our expressive power one can show

every quantifier-free formula is equivalent to a disjunction of conjunctions of assertions about the constituents being empty or nonempty.

We can still make remarkable reductions after adding quantifiers. This will be the topic of the next section.

EXERCISES


Elimination of Quantifiers

The elimination problem originated in the work of Boole as the elimination of middle terms from (equational) hypotheses in the Calculus of Classes. This was extended by Schröder to both equational and negated equational hypotheses.

It is first in the 1919 paper of Skolem that we find the modern formulation of the elimination problem, in the case of the Calculus of Classes with numerical predicates, as the elimination of quantifiers; namely for a formula , where is quantifier-free, we want to find a quantifier-free formula which is equivalent (with respect to the Calculus of Classes). Once one shows this is possible, then one can also eliminate the universal quantifier by using , and then eliminating the existential quantifier from . Thus being able to eliminate quantifiers from formulas of the form leads to the conclusion that any first-order formula in the Calculus of Classes is equivalent to a quantifier-free -- simply put in prenex form, and then eliminate one quantifier at a time, from the inside out.

Following the work of Skolem, certain syntactic transformations are standard in quantifier elimination. Let us look at them, and then give the details of Skolem's work on the Calculus of Classes.

The standard syntatic transformations

Given a first-order formula:

The above transformations can be useful even without trying to eliminate quantifiers. Let us use them to analyze the expressive power of sentences in the first-order monadic logic gif without equality. Suppose the unary predicate symbols appearing in are . Then is seen to be equivalent to a Boolean combination of sentences of the form , where is one of the ``constituents'' . Now simply says that the ``constituent'' is not empty.

Thus a first-order sentence in the monadic logic without equality simply expresses some Boolean combination of the assertions `` is empty''. One can easily determine if such a Boolean combination is true in all structures ; and thus we have proved the following.

This theorem (in its more general form, with equality) is due to Löwenheim, 1915, with credit given to Skolem, 1919, for a nice proof. Actually Löwenheim states, with a sketch of a proof, that if a sentence in this language is not valid, then it has a finite countermodel. Furthermore his proof gives an algorithm to determine which is the case; and in the latter case shows how one can quickly find a finite countermodel. Skolem gives a quantifier elimination procedure for the calculus of classes with numerical predicates, presented below, and from this he has a decision procedure for the first-order statements of this theory. Then he shows that one can easily translate back and forth between this calculus and first-order monadic logic with equality. Consequently he can describe the expressive power of first-order sentences in monadic logic with equality; and he uses this to prove Löwenheim's assertion about the existence of finite countermodels.

Now let us turn to Skolem's 1919 paper [1]. In this he adds numerical predicates to the language of the Calculus of Classes, for , with the understanding that, in any given domain, is to express the fact that X has at least n elements in it.

PROOF. First we do some simple transformations. All subformulas of a given which involve can be put in the form , and hence in the form . Thus can be eliminated from our formula. It suffices to show how to eliminate the quantifier in a formula of the form

To do this put the term in disjunctive form

and then by repeated use of

for s and t disjoint, we see that it suffices to show how to eliminate the quantifier from formulas of the form

where each denotes one of the -constituents.

Now collect the atomic formulas involving each particular constituent together to obtain

Then an easy argument shows that this is equivalent in the Calculus of Classes to

Consequently we are left with the problem of showing how to eliminate a quantifier from a formula of the form

for a single constituent . As implies in the Calculus of Classes, we can reduce such a formula to one involving at at most 4 conjuncts:

It can also be the case that some of these atomic's are omitted. This can now be transformed into a Boolean combination of statements of the form

in case there are some y's; and otherwise one has a Boolean combination of statements of the form

i.e., assertions about the size of the universe 1.

Thus we have established the elimination of quantifiers, and the claims about the expressive power of formulas and sentences.

EXERCISES


Second-order monadic logic refers to extending first-order monadic logic by allowing quantification over the (unary) relation symbols.



References

1
Th. Skolem, Untersuchung über die Axiome des Klassenkalküls und über Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen. Videnskabsakademiet i Kristiania, Skrifter I, No. 3, 1919, pp. 37. Also in ``Selected Works in Logic by Th. Skolem'', ed. by Jens Erik Fenstak, Scand. Univ. Books, Universitetsforlaget, Oslo, 1970.


Previous: Quasi-identity logic

Next: Downward Löwenheim-Skolem Theorem

Up: Supplementary Text Topics


© Stanley Burris