Thus a1 = a and an+1 = an · a. We say that G is a torsion group if for all a ∈ G

there exists a positive integer n such that an = 1. We say that G is torsion-free

if for all a ∈ G, if a = 1 then an = 1 for all positive integers n.

1. Show that the class of torsion-free groups can be characterized by a set of

sentences. I.e., there is a set of sentences S such that, for all groups G, G

is torsion-free if and only if G satis¬es S.

2. Show that the class of torsion-free groups cannot be characterized by a

¬nite set of sentences.

3. Show that the class of torsion groups cannot be characterized by a set of

sentences. I.e., there is no set of sentences S with the property that, for

all groups G, G is a torsion group if and only if G satis¬es S.

Exercise 4.2.17. Show that the spectrum problem for predicate calculus with

identity and operations is equivalent to the spectrum problem for predicate

calculus with identity and without operations, as previously discussed in Section

4.1. In other words, given a sentence A involving some operations, construct a

sentence A involving no operations, such that spectrum(A) = spectrum(A ).

Hint: Replace each n-ary operation f by an (n + 1)-ary predicate Pf where

Pf x1 . . . xn y expresses If x1 . . . xn y.

4.3 Many-Sorted Predicate Calculus

De¬nition 4.3.1 (many-sorted languages). A many-sorted language con-

sists of

1. a set of sorts σ, „, . . .,

2. a set of predicates P, Q, . . ., each designated as n-ary of type

σ1 — · · · — σn

for some nonnegative integer n and sorts σ1 , . . . , σn ,

3. a set of operations f, g, . . ., each designated as n-ary of type

62

σ1 — · · · — σn ’ σn+1

for some nonnegative integer n and sorts σ1 , . . . , σn , σn+1 .

Let L be a many-sorted language.

De¬nition 4.3.2 (terms, formulas, sentences). For each sort σ, we assume

a ¬xed, countably in¬nite set of variables of sort σ, denoted xσ , y σ , z σ , . . .. Let

U = (U σ , U „ , . . .) consist of a set U σ for each sort σ of L. The L-U -terms are

generated as follows.

1. Each variable of sort σ is a term of sort σ.

2. Each element of U σ is a term of sort σ.

3. If f is an n-ary operaton of type σ1 — · · · — σn ’ σn+1 , and if t1 , . . . , tn

are terms of sort σ1 , . . . , σn respectively, then f t1 . . . tn is a term of sort

σn+1 .

An atomic L-U -formula is an expression of the form P t1 . . . tn , where P is an

n-ary predicate of type σ1 — · · · — σn , and t1 , . . . , tn are terms of sort σ1 , . . . , σn

respectively. The L-U -formulas are generated as in De¬nition 2.1.3, with clause

5 modi¬ed as follows:

5™. If xσ is a variable of sort σ, and if A is an L-U -formula, then ∀xσ A and

∃xσ A are L-U -formulas.

Our notions of substitution, free and bound variables, sentences, etc. are ex-

tended in the obvious way to the many-sorted context. Naturally, the substitu-

tion A[xσ /t] makes sense only when t is a term of sort σ. An L-formula is an

L-U -formula where Uσ = … for each sort σ.

De¬nition 4.3.3 (many-sorted structures). An L-structure M consists of

σ

1. a nonempty set UM for each sort σ of L,

2. an n-ary relation PM ⊆ UM1 — · · · — UMn for each n-ary predicate P of

σ σ

type σ1 — · · · — σn belonging to L,

σ

3. an n-ary function fM : UM1 — · · · — UMn ’ UMn+1 for each n-ary operation

σ σ

of type σ1 — · · · — σn ’ σn+1 belonging to L.

Notions such as isomorphism, valuation, truth, satis¬ability, and results such as

Theorem 4.2.9 on onto mappings, carry over to the many-sorted context in the

obvious way.

De¬nition 4.3.4 (many-sorted domains). We de¬ne a domain for L to be

an indexed family of nonempty sets U = (U σ , U „ , . . .), where σ, „, . . . are the

sorts of L. In this way, the notion of satis¬ability in a domain generalizes to

the many-sorted context.

63

Remark 4.3.5 (tableau method, proof systems). For each sort σ of L, ¬x

a countably in¬nite set V σ = {aσ , bσ , . . .}, the set of parameters of sort σ. Then

the tableau method carries over in the obvious way, generalizing Remark 4.2.7.

In the Completeness Theorem for the tableau method, we obtain satis¬ability

in the domain U = (U σ , U „ , . . .), where U σ is the set of variable-free L-V -terms,

with V = (V σ , V „ , . . .). The soundness and completeness of our proof systems

LH and LG and the Interpolation Theorem also carry over, just as in Section

4.2.

Remark 4.3.6 (identity predicates). For each sort σ of L, L may or may

not contain a binary predicate I σ of type σ — σ designated as the identity

predicate for σ. As identity axioms we may take the universal closures of all

L-formulas of the form

∀xσ ∀y σ (I σ xy ’ (A ” A[x/y]))

where A is atomic. An L-structure M is said to be normal if IM = { a, a : a ∈

σ

UM } for all σ such that I σ belongs to L. The results of Section 4.1 concerning

σ

normal satis¬ability carry over to the many-sorted context. If A is an L-sentence

and σ1 , . . . , σk are the sorts occurring in A, the spectrum of A is the set of

k-tuples of positive integers (n1 , . . . , nk ) such that there exists a normal L-

σ

structure M with UMi of cardinality ni , for i = 1, . . . , k. In this way, the

spectrum problem carries over to many-sorted predicate calculus.

Remark 4.3.7. Our reasons for including many-sorted predicate calculus in

this course are as follows:

1. it is more useful . . . .

FIXME

64

Chapter 5

Theories, Models,

De¬nability

5.1 Theories and Models

De¬nition 5.1.1. A theory T consists of a language L, called the language of

T , together with a set of L-sentences called the axioms of T .

De¬nition 5.1.2. If T is a theory, a model of T is a structure M for the

language of T such that all of the axioms of T are true in M .

De¬nition 5.1.3. Let T be a theory with language L. A theorem of T is any

L-sentence which is a logical consequence of the axioms of T . Equivalently, a

theorem of T is any L-sentence which is is true in all models of T . Two theories

are said to be equivalent if they have the same language and the same theorems.

De¬nition 5.1.4. A theory T is said to be consistent if there exists at least

one model of T . Equivalently, T is consistent if the sentence F is not a theorem

of T .

De¬nition 5.1.5. theories with identity, normal models

5.2 Mathematical Theories

Example 5.2.1 (groups).

Example 5.2.2 (rings).

Example 5.2.3 (¬elds).

Example 5.2.4 (vector spaces).

Example 5.2.5 (ordered structures).

65

5.3 Foundational Theories

Example 5.3.1 (¬rst order arithmetic).

Example 5.3.2 (second order arithmetic).

Example 5.3.3 (set theory).

Remark 5.3.4 (practical completeness).