                                              Notes prepared by
                                                 Stanley Burris
                                                   July 3, 2001

1 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 φ(X⃗) can say about the classes X⃗.

1.1 Quantifier-free formulas

Given an equation ε(X⃗) we can find an equivalent equation (using symmetric difference) p(X⃗) ≈ 0. Then using complete expansion we can assume p is a disjunction of constituents Ca⃗(X⃗). 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 Problem 1

(a) Show that one can find [at most] 2^{2^{n}} (unquantified) equations ε(X_{1}, …, X_{n}) in the calculus of classes such that for any two of these equations one can find an assignment such that the two equations have different truth values. [Hint: Show that every equation is equivalent to one in the form p(X_{1}, …, X_{n}) ≈ 0.]

(b) Show that the number of inequivalent &, ∨ combinations of such equations in the variables X_{1}, …, X_{n} is the same as the number of antichains^{1} in a Boolean algebra^{2} of size 2^{2^{n}}. [Hint: First show that every such combination is equivalent to a disjunction of conjunctions of equations of the form p ≈ 0. Then show that & can be eliminated. Thus every such combination is equivalent to one of the form p_{1} ≈ 0 ∨ ⋯ ∨ p_{k} ≈ 0. Next argue that one only needs to consider cases where the p_{i} are pairwise incomparable.]

1An antichain is a set of pairwise incomparable (under ≤) elements.

1.2 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 ∃xφ(x, y⃗), where φ is quantifier-free, we want to find a quantifier-free formula ψ(y⃗) 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 ∀xφ(x, y⃗) ∼ ¬∃x¬φ(x, y⃗), and then eliminating the existential quantifier from ∃x¬φ(x, y⃗). Thus being able to eliminate quantifiers from formulas of the form ∃xφ(x, y⃗) leads to the conclusion that any first-order formula φ(y⃗) in the Calculus of Classes is equivalent to a quantifier-free ψ(y⃗)

— 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 syntactic transformations Given a first-order formula:

• first put it in prenex form, say

Q_{1}x_{1} ⋯ Q_{n}x_{n}φ.

• If Q_{n} is ∀, change it to ¬∃¬. Then we will have an equivalent (perhaps the same) formula

Q_{1}x_{1} ⋯ Q_{n−1}x_{n−1} ± ∃x_{n}φ′.

2No closed expression is known for this number.

Now we focus our attention on ∃x_{n}φ′, with the intention of eliminating the existential quantifier. When this has been accomplished, we return to the above formula, replacing ∃x_{n}φ′ with the quantifier-free equivalent, and start to work on Q_{n−1}, etc.

• Our next step is to put φ′ into disjunctive form:

φ′ ∼ ⋁ ⋀ ±atomic.

• Then one can move the existential quantifier inside the disjunction:

∃x_{n}φ′ ∼ ∃x_{n} ⋁ ⋀ ±atomic ∼ ⋁ ∃x_{n} ⋀ ±atomic.

Thus we can now concentrate on eliminating ∃x_{n} from each of the disjuncts ∃x_{n} ⋀ ±atomic.

• Now, fixing our attention on one of the disjuncts, x_{n} may not appear in some of the atomic formulas, so we can pull those atomic formulas outside the scope of the quantifier:

∃x_{n} ⋀ ±atomic ∼ [∃x_{n} ⋀ ±atomic(x_{1}, ⋯, x_{n})] ∧ ⋀ ±atomic(x_{1}, ⋯, x_{n−1}).

• Thus, to carry out the elimination of quantifiers, it suffices to eliminate quantifiers in the cases of the form

∃x_{n} ⋀ ±atomic(x_{1}, ⋯, x_{n}),

where x_{n} actually appears in each of the atomic formulas.

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^{3} without equality. Suppose the unary predicate symbols appearing in φ are P_{1}, ⋯, P_{k}. Then φ is seen to be equivalent to a Boolean combination of sentences of the form ∃x_{i}C_{j}(x_{i}), where C_{j}(x_{i}) is one of the “constituents” ±P_{1}(x_{i}) ∧ ⋯ ∧ ±P_{k}(x_{i}). Now ∃x_{i}C_{j}(x_{i}) simply says that the “constituent” C_{j} is not empty.

Thus a first-order sentence in the monadic logic without equality simply expresses some Boolean combination of the assertions “C_{j} is empty”. One can easily determine if such a Boolean combination is true in all structures (D, P_{1}, ⋯, P_{k}); and thus we have proved the following.

3Recall that this means all relation symbols are unary

THEOREM 1 One can decide if a sentence in the first-order monadic logic without equality is valid.

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 A_{n}( ) to the language ∪, ∩,′ , 0, 1 of the Calculus of Classes, for n ≥ 0, with the understanding that, in any given domain, A_{n}(X) is to express the fact that X has at least n elements in it.

DEFINITION 2 For y⃗ = (y_{1}, ⋯, y_{k}), a y⃗-constituent is a term of the form

±y_{1} ∩ ⋯ ∩ ±y_{k}.

DEFINITION 3 A Boolean combination of formulas φ_{1}, ⋯, φ_{k} is a formula built up from the φ_{i} using and, or, and not.

THEOREM 4 [Skolem] The first-order theory of the Calculus of Classes with numerical predicates admits elimination of quantifiers. Indeed,

(a) every formula φ(y⃗) is equivalent, in the Calculus of Classes, to a formula which is a Boolean combination of numerical assertions about the y⃗- constituents, and

(b) every sentence is equivalent to a Boolean combination of assertions about the size of the domain.

Proof. First we do some simple transformations. All subformulas of a given φ which involve ≈ can be put in the form p ≈ 0, and hence in the form ¬A_{1}(p). Thus ≈ can be eliminated from our formula. It suffices to show how to eliminate the quantifier in a formula of the form

∃x ⋀ ±A_{i}(p_{i}(x, y⃗)).

To do this put the term p_{i} in disjunctive form

⋃ ±x ∩ ±y_{1} ⋯ ∩ ±y_{k},

and then by repeated use of

A_{k}(s ∪ t) ∼ ⋁_{j=0}^{k} A_{i}(s) ∧ A_{k−i}(t),

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

∃x ⋀ ±A_{i}[±x ∩ C_{j}(y⃗)],

where each C_{j}(y⃗) denotes one of the y⃗-constituents.

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

∃x ⋀_{j} (⋀_{i} ±A_{i}[±x ∩ C_{j}(y⃗)]) .

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

⋀_{j} ∃x (⋀_{i} ±A_{i}[±x ∩ C_{j}(y⃗)]) .

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

∃x (⋀_{i} ±A_{i}[±x ∩ C(y⃗)]) ,

for a single constituent C(y⃗). As A_{i+1}(x) implies A_{i}(x) in the Calculus of Classes, we can reduce such a formula to one involving at at most 4 conjuncts:

∃x (A_{i_{1}}[x ∩ C(y⃗)] ∧ ¬A_{i_{2}}[x ∩ C(y⃗)] ∧ A_{i_{3}}[x′ ∩ C(y⃗)] ∧ ¬A_{i_{4}}[x′ ∩ C(y⃗)]) .

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

A_{i}[C(y⃗)],

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

A_{i}(1),

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.

COROLLARY 5 [Skolem] The first-order theory of the Calculus of Classes is decidable.

Exercises

Problem 2 Prove that a sentence in the Calculus of Classes which is not valid on all domains is not valid on some finite domain.

Problem 3 Show that a sentence in the Calculus of Classes holds for only finitely many sizes of the domain, all of which are finite; or it holds for all but finitely many sizes of the domain, all of which are finite.

Problem 4 Prove that one can eliminate quantifiers in first-order monadic logic without equality.

Problem 5 [Löwenheim] Prove that a sentence in the first-order monadic logic with equality which is not valid on all domains is not valid on some finite domain.

Problem 6 Let F in( ) be unary predicate which is to mean “is finite”. Show that by adding F in to the Calculus of Classes with numerical predicates we still have elimination of quantifiers.

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

Problem 7

(a) Show that equality is definable in second-order monadic logic without equality.

(b) Show that every formula in second-order monadic logic is equivalent to one in first-order monadic logic with equality.

(c) Show that (the set of valid sentences in) second-order monadic logic is decidable.

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.