De¬nition 5.4.1. explicit de¬nability over M

De¬nition 5.4.2. implicit de¬nability over M

Exercise 5.4.3. Show that any relation which is explicitly de¬nable over M is

implicitly de¬nable over M .

Exercise 5.4.4. Let R = (R, +, ’, ·, 0, 1, <, =) be the ordered ¬eld of real num-

bers. Show that the relations y = sin x and y = ex are implicitly de¬nable over

R. It can be shown that these relations are not explicitly de¬nable over R.

Exercise 5.4.5. Show that if M is saturated, then any relation which is im-

plicitly de¬nable over M is explicitly de¬nable over M .

Remark 5.4.6. Beth De¬nability Theorem

5.5 De¬nitional Extensions of Theories

Theorem 5.5.1 (adding a new predicate).

Theorem 5.5.2 (adding a new operation).

De¬nition 5.5.3. We say that T1 is interpretable in T2 if T1 is a subtheory of

a de¬nitional extension of T2 .

Example 5.5.4. First order arithmetic is interpretable in second order arith-

metic. First and second order arithmetic are interpretable in set theory.

5.6 The Beth De¬nability Theorem

Theorem 5.6.1 (the Beth De¬nability Theorem).

Proof. This is an application of the Interpolation Theorem, Section 3.5.

66

Chapter 6

Arithmetization of

Predicate Calculus

6.1 Primitive Recursive Arithmetic

De¬nition 6.1.1. To each natural number n we associate a PRA-term n as

follows: 0 = 0, n + 1 = S(n). These terms are known as numerals.

Theorem 6.1.2. Let f be a k-ary primitive recursive function. Then for all

k-tuples of natural numbers m1 , . . . , mk we have

f m1 · · · mk = f (m1 , . . . , mk ) .

PRA

Proof.

6.2 Interpretability of PRA in Z1

6.3 G¨del Numbers

o

Let L be a countable language. Assume that to all the sorts σ, predicates P ,

and operations f of L have been assigned distinct positive integers #(σ), #(P ),

#(f ) respectively.

De¬nition 6.3.1 (G¨del numbers). To each term t and formula A of L we

o

assign a positive integer, the G¨del number of t or of A, denoted #(t) or #(A),

o

67

respectively.

2 · 3#(σ) · 5i

σ

#(vi ) =

22 · 3#(σ) · 5i

#(aσ ) =

i

#(t1 ) #(t )

#(f t1 · · · tn ) 23 · 3#(f ) · p2 · · · pn+1

n

= if f is an n-ary operation

#(t1 ) #(t )

#(P t1 · · · tn ) = 24 · 3#(P ) · p2 · · · pn+1

n

if P is an n-ary predicate

25 · 3#(A)

#(¬ A) =

26 · 3#(A) · 5#(B)

#(A & B) =

#(A ∨ B) 27 · 3#(A) · 5#(B)

=

#(A ’ B) 28 · 3#(A) · 5#(B)

=

#(A ” B) 29 · 3#(A) · 5#(B)

=

210 · 3#(v) · 5#(A)

#(∀v A) =

211 · 3#(v) · 5#(A)

#(∃v A) =

De¬nition 6.3.2. The language L is said to be primitive recursive if the fol-

lowing items are primitive recursive.

≡

Sort(x) x = #(σ) for some sort σ

≡

Pred(x) x = #(P ) for some predicate P

≡

Op(x) x = #(f ) for some operation f

arity(#(P )) = n if P is an n-ary predicate

arity(#(f )) = n if f is an n-ary operation

if 1 ¤ i ¤ n and P is an n-ary predicate of

sort(#(P ), i) = #(σi )

type σ1 — · · · — σn

if 1 ¤ i ¤ n + 1 and f is an n-ary operation

sort(#(f ), i) = #(σi )

of type σ1 — · · · — σn ’ σn+1

Lemma 6.3.3. If L is primitive recursive, then the following are primitive re-

cursive.

≡

Var(x) x = #(v) for some variable v

≡

Param(x) x = #(a) for some parameter a

≡

Term(x) x = #(t) for some term t

≡

ClTerm(x) x = #(t) for some closed term t

≡

AtFml(x) x = #(A) for some atomic formula A

≡

Fml(x) x = #(A) for some formula A

sort(#(t)) = #(σ) if t is a term of sort σ

Proof. We have

≡ (x)0 = 1 & x = 2(x)0 · 3(x)1 · 5(x)2 & Sort((x)1 )

Var(x)

68

and

≡ (x)0 = 2 & x = 2(x)0 · 3(x)1 · 5(x)2 & Sort((x)1 ) .

Param(x)

To show that the predicate Term(x) is primitive recursive, we ¬rst show that the

function sort(x) is primitive recursive, where sort(#(t)) = #(σ) if t is a term of

sort σ, sort(x) = 0 otherwise. Put lh(x) = least w < x such that (x)w = 0. We

then have

±

if Var(x) ∨ Param(x) ,

(x)1

·

sort((x)1 , lh(x) ’ 1) if (x)0 = 3 & Op((x)1 ) & (+) ,

sort(x) =