I J

M, F A & B, F A ’ N M, F A & B, F B ’ N

I ∨J

M, F A & B ’’ N

I J

M ’ T A & B, T A, N M ’ T A & B, T B, N

I &J

M ’’ T A & B, N

I I

M, T ¬ A, F A ’ N M ’ F ¬ A, T A, N

I I

M, T ¬ A ’ N M ’ F ¬ A, N

I I

M, F ¬ A, T A ’ N M ’ T ¬ A, F A, N

I I

M, F ¬ A ’ N M ’ T ¬ A, N

5 In the special case when M and N have no predicates in common, we require instead

that at least one of the signed sequents M ’ and ’ N be logically valid. This amounts to

requiring that at least one of T, F be an interpolant for M ’ N .

51

I

M, F ∀x A, F A[x/a] ’ N

I

M, F ∀x A ’ N

where a does not occur in the conclusion.

I

M ’ T ∀x A, T A[x/a], N

I

M ’ T ∀x A, N

where a does not occur in the conclusion.

I

M, T ∀x A, T A[x/a] ’ N

K

M, T ∀x A ’ N

where K = I if a occurs in M, T ∀x A, otherwise K = ∀z I[a/z] where z is a

new variable.

I

M ’ F ∀x A, F A[x/a], N

K

M ’ F ∀x A, N

where K = I if a occurs in F ∀x A, N , otherwise K = ∃z I[a/z] where z is a new

variable.

This completes the proof.

52

Chapter 4

Extensions of Predicate

Calculus

4.1 Predicate Calculus with Identity

De¬nition 4.1.1. A language with identity consists of a language L with a

particular binary predicate, I, designated as the identity predicate.

De¬nition 4.1.2. Let L be a language with identity. The identity axioms for

L are the following sentences:

1. ∀x Ixx (re¬‚exivity)

2. ∀x ∀y (Ixy ” Iyx) (symmetry)

3. ∀x ∀y ∀z ((Ixy & Iyz) ’ Ixz) (transitivity)

4. For each n-ary predicate P of L, we have an axiom

∀x1 · · · ∀xn ∀y1 · · · ∀yn ((Ix1 y1 & · · · & Ixn yn ) ’ (P x1 · · · xn ” P y1 · · · yn ))

(congruence).

Exercise 4.1.3. Show that the identity predicate is unique in the following

sense. If L contains two identity predicates I1 and I2 , then ∀x ∀y (I1 xy ” I2 xy)

is a logical consequence of the identity axioms for I1 and I2 .

Let L be a language with identity.

De¬nition 4.1.4. An L-structure M is said to be normal if the identity pred-

icate denotes the identity relation, i.e., IM = { a, a : a ∈ UM }.

Note that any normal L-structure automatically satis¬es the identity axioms

for L. Conversely, we have:

53

Theorem 4.1.5. Let M be an L-structure satisfying the identity axioms for

L. For each a ∈ UM put a = {b ∈ UM : vM (Iab) = T}. Then we have a normal

L-structure M and an onto mapping φ : UM ’ UM as in Theorem 2.7.3, de¬ned

by putting UM = {a : a ∈ UM }, and PM = { a1 , . . . , an : a1 , . . . , an ∈ PM }

for all n-ary predicates P .

Proof. This is straightforward, using the fact that IM is a congruence with

respect to each of the relations PM , P ∈ L.

Theorem 4.1.6. If M is an L-structure satisfying the identity axioms for L,

then we have a normal L-structure M satisfying the same sentences as M .

Proof. This is immediate from Theorems 4.1.5 and 2.7.3.

Let S be a set of L-sentences.

De¬nition 4.1.7. S is normally satis¬able if there exists a normal L-structure

which satis¬es S.

Corollary 4.1.8. S is normally satis¬able if and only if

S ∪ {identity axioms for L}

is satis¬able.

We also have the Compactness Theorem for normal satis¬ability:

Corollary 4.1.9. S is normally satis¬able if and only if each ¬nite subset of S

is normally satis¬able.

Proof. This is immediate from Corollary 4.1.8 plus the Compactness Theorem

for predicate calculus without identity (Theorems 2.6.1 and 2.6.2).

Regarding normal satis¬ability in particular domains, we have:

Example 4.1.10. Given a positive integer n, we exhibit a sentence En which

is normally satis¬able in domains of cardinality n but not in domains of any

other cardinality. The sentence

∃x1 · · · ∃xn (∀y (Ix1 y ∨ · · · ∨ Ixn y) & ¬ (Ix1 x2 ∨ Ix1 x3 ∨ · · · ∨ Ixn’1 xn ))

has this property. Intuitively, En says that there exist exactly n things.

On the other hand, we have:

Theorem 4.1.11.

1. If S is normally satis¬able in arbitrarily large ¬nite domains, then S is

normally satis¬able in some in¬nite domain.

2. If S is normally satis¬able in some in¬nite domain, then S is normally

satis¬able in all in¬nite domains of cardinality ≥ the cardinality of S.

54

Proof. Use the Compactness Theorem.

FIXME

De¬nition 4.1.12. Let A be a sentence of the predicate calculus with identity.

The spectrum of A is the set of positive integers n such that A is normally

satis¬able in a domain of cardinality n. A spectrum is a set X of positive

integers, such that X = spectrum(A) for some A.

Remark 4.1.13. The spectrum problem is the problem of characterizing the

spectra, among all sets of positive integers. This is a famous and apparently

di¬cult open problem.1 In particular, it is unknown whether the complement

of a spectrum is necessarily a spectrum.

Exercises 4.1.14. Prove the following.

1. If X is a ¬nite or co¬nite2 set of positive integers, then X is a spectrum.

2. The set of even numbers is a spectrum.

3. The set of odd numbers is a spectrum.

4. If r and m are positive integers, {n ≥ 1 : n ≡ r mod m} is a spectrum.

5. If X and Y are spectra, X ∪ Y and X © Y are spectra.

Exercise 4.1.15. Prove that, for any sentence A of the predicate calculus with

identity, at least one of spectrum(A) and spectrum(¬ A) is co¬nite. (Hint: Use

part 1 of Theorem 4.1.11.)

Example 4.1.16. We show that the set {n ≥ 1 : n is even} is a spectrum.

Let U be a nonempty set. A binary relation R ⊆ U 2 is said to be an

equivalence relation on U if it is re¬‚exive, symmetric, and transitive, i.e., if the

structure (U, R) satis¬es (1) & (2) & (3):