8 of Lemma 2.2.4.

Proof. The proof is as for Lemma 2.2.4.

De¬nition 4.2.6 (tableau method). The signed and unsigned tableau meth-

ods carry over to predicate calculus with operations. We modify the tableau

rules as follows.

Signed:

. .

. .

. .

T ∀x A F ∃x A

. .

. .

. .

| |

T A[x/t] F A[x/t]

where t is a variable-free term

. .

. .

. .

T ∃x A F ∀x A

. .

. .

. .

| |

T A[x/a] F A[x/a]

where a is a new parameter

Unsigned:

. .

. .

. .

∀x A ¬ ∃x A

. .

. .

. .

| |

¬ A[x/t]

A[x/t]

where t is a variable-free term

59

. .

. .

. .

∃x A ¬ ∀x A

. .

. .

. .

| |

¬ A[x/a]

A[x/a]

where a is a new parameter

Remark 4.2.7 (soundness and completeness). With the tableau rules as

above, the Soundness Theorem 2.3.9 carries over unchanged to the context of

predicate calculus with operations. The results of Section 2.4 on logical equiv-

alence also carry over. The notion of U -repleteness (De¬nition 2.5.2) is modi-

¬ed to say that, for example, if S contains ∀x A then S contains A[x/t] for all

variable-free L-U -terms t. The conclusion of Hintikka™s Lemma 2.5.3 is modi¬ed

to say that S is satis¬able in the domain of variable-free L-U -terms. The con-

clusion of the Completeness Theorem 2.5.5 is modi¬ed to say that X1 , . . . , Xk

is satis¬able in the domain of variable-free L-V -terms. The Compactness The-

orems 2.6.1 and 2.6.2 carry over unchanged.

Remark 4.2.8 (satis¬ability in a domain). The notion of satis¬ability in

a domain carries over unchanged to the context of predicate calculus with op-

erations. Theorems 2.2.6 and 2.2.11 on isomorphism, and Theorem 2.7.1 on

satis¬ability in in¬nite domains, also carry over. Theorem 2.7.3 carries over in

an appropriately modi¬ed form. See Theorem 4.2.9 and Exercise 4.2.10 below.

Theorem 4.2.9. Let M and M be L-structures. Assume that φ : UM ’ UM

is an onto mapping such that conditions 1 and 2 of De¬nition 4.2.4 hold. Then

as in Theorem 2.2.6 we have vM (A) = vM (A ) for all L-UM -sentences A, where

A = A[a1 /φ(a1 ), . . . , ak /φ(ak )]. In particular, M and M satisfy the same

L-sentences.

Proof. The proof of is similar to that of Theorem 2.7.3.

Exercise 4.2.10. Use Theorem 4.2.9 to show that Corollary 2.7.4 carries over

to the context of predicate calculus with operations.

Remark 4.2.11 (companions and proof systems). In our notion of com-

panion (De¬nition 3.2.3), clauses (1) and (4) are modi¬ed as follows:

(∀x B) ’ B[x/t]

(1)

B[x/t] ’ (∃x B)

(4)

where t is any variable-free term. In our Hilbert-style proof system LH , the

instantiation rules are modi¬ed as follows:

60

(a) (∀x B) ’ B[x/t] (universal instantiation)

(b) B[x/t] ’ (∃x B) (existential instantiation)

where t is any variable-free term. Also, our Gentzen-style proof system LG is

modi¬ed in accordance with the modi¬ed tableau rules. With these changes,

the soundness and completeness of LG and LH carry over.

Exercise 4.2.12 (the Interpolation Theorem). Strengthen the Interpola-

tion Theorem 3.5.1 to say that each operation, predicate and parameter occur-

ring in I occurs in both A and B. (Hint: The version with operations can be

deduced from the version without operations.)

Remark 4.2.13 (predicate calculus with identity). We augment the iden-

tity axioms (De¬nition 4.1.2) as follows:

5. For each n-ary operation f of L, we have an axiom

∀x1 · · · ∀xn ∀y1 · · · ∀yn ((Ix1 y1 & · · · & Ixn yn ) ’ If x1 · · · xn f y1 · · · yn ).

The notions of normal structure and normal satis¬ability are de¬ned as be-

fore. The results of Section 4.1 on predicate calculus with identity carry over

unchanged to predicate calculus with identity and operations.

Remark 4.2.14 (predicate calculus with equality). The predicate calcu-

lus with identity and operations is well suited for the study of algebraic struc-

tures such as number systems, groups, rings, etc. In such a context, one often

writes t1 = t2 instead of It1 t2 , and one refers to predicate calculus with equality

rather than predicate calculus with identity. One also uses customary algebraic

notation, e.g., t1 + t2 instead of +t1 t2 , t1 — t2 or t1 t2 instead of —t1 t2 , etc. To

avoid ambiguity, parentheses are used.

Examples 4.2.15 (groups and rings). Using predicate calculus with iden-

tity and operations, a group may be viewed as an L-structure

G = (UG , fG , iG , eG , IG ).

Here UG is the underlying set of the group, and L is the language {f, i, e, I},

where f is the group composition law (a binary operation), i is group inversion

(a unary operation), e is the group identity element (a 0-ary operation, i.e., a

constant), and I is the identity predicate (a binary predicate). We could refer

to L as the language of groups. It is customary to write G instead of UG , t1 · t2

or t1 t2 instead of f t1 t2 , t’1 instead of it, 1 instead of e, and t1 = t2 instead of

It1 t2 . Thus

G = (G, ·G , ’1 G , 1G , =G )

and G is required to satisfy the group axioms, consisting of the equality axioms

(i.e., the identity axioms for L) plus ∀x ∀y ∀z ((xy)z = x(yz)), ∀x (x’1 x =

xx’1 = 1), ∀x (1x = x1 = x).

Similarly, a ring may be viewed as a structure

61

R = (R, +R , ·R , ’R , 0R , 1R , =R )

where + and · are binary operations, ’ is a unary operation, 0 and 1 are

constants, and = is the equality predicate. We could refer to the language

{+, ·, ’, 0, 1, =} as the language of rings. R is required to satisfy the ring axioms,

consisting of the equality axioms (i.e., the identity axioms) plus ∀x ∀y ∀y ((x +

y) + z = x + (y + z)), ∀x ∀y (x + y = y + x), ∀x (x + 0 = x), ∀x (x + (’x) = 0),

∀x ∀y ∀z ((x · y) · z = x · (y · z)), ∀x (x · 1 = 1 · x = x), ∀x ∀y ∀z (x · (y + z) =

(x · y) + (x · z)), ∀x ∀y ∀z ((x + y) · z = (x · z) + (y · z)).