where

·

lh(x)’1

· (x)i

arity((x)1 ) = lh(x) ’ 2 & x =

(+) pi

i=0

·

& (∀i < lh(x) ’ 2) (sort((x)i+2 ) = sort((x)1 , i + 1)) .

Then

Term(x) ≡ sort(x) > 0 .

For closed terms, de¬ne clsort(x) like sort(x) replacing Var(x) ∨ Param(x) by

Param(x). We then have

ClTerm(x) ≡ clsort(x) > 0 .

For formulas we have

≡

AtFml(x) ((x)0 = 4 & Pred((x)1 ) & (+))

and

≡ AtFml(x) ∨ ((x)0 = 5 & x = 2(x)0 · 3(x)1 & Fml((x)1 ))

Fml(x)

∨ (6 ¤ (x)0 ¤ 9 & x = 2(x)0 · 3(x)1 · 5(x)2 & Fml((x)1 ) & Fml((x)2 ))

∨ (10 ¤ (x)0 ¤ 11 & x = 2(x)0 · 3(x)1 · 5(x)2 & Var((x)1 ) & Fml((x)2 ))

and this completes the proof.

Lemma 6.3.4 (substitution). There is a primitive recursive function sub(x, y, z)

such that for any formula A and any variable v and any closed term t,

sub(#(A), #(v), #(t)) = #(A[v/t]) .

Proof.

±

z if x = y

(x)0 ·

2 lh(x)’1

sub((x)i ,y,z)

· 3(x)1 · if 3 ¤ (x)0 ¤ 4

pi

i=2

(x)0

2 · 3sub((x)1 ,y,z) if (x)0 = 5

sub(x, y, z) =

2(x)0 · 3sub((x)1 ,y,z) · 5sub((x)2 ,y,z) if 6 ¤ (x)0 ¤ 9

(x)

2 0 · 3(x)1 · 5sub((x)2 ,y,z) if 10 ¤ (x)0 ¤ 11 & (x)1 = y

x otherwise.

69

Lemma 6.3.5. If L is primitive recursive, then the predicate

Snt(x) ≡ x = #(A) for some sentence A

is primitive recursive.

Proof. Recall that, by Exercise 2.1.10, a formula A is a sentence if and only if

σ

A[v/a] = A for all variables v occurring in A. Note also that if y = #(vi ) then

2y = #(aσ ). Thus we have

i

Snt(x) ≡ Fml(x) & (∀y < x) (Var(y) ’ x = sub(x, y, 2y)) .

Lemma 6.3.6. There is a primitive recursive function num(x) such that

num(n) = #(n)

for any nonnegative integer n.

Proof. The recursion equations for num(x) are

num(0) = #(0) ,

23 · 3#(S) · 5num(x) .

num(x + 1) =

6.4 Unde¬nability of Truth

In this section, let T be a theory which includes PRA. For example, we could

take T to be PRA itself. Or, by Section 6.2, we could take T to be an appropriate

de¬nitional extension of Z1 or Z2 or ZFC.

Lemma 6.4.1 (Self-Reference Lemma). Let L be the language of T . Let

A(x) be an L-formula with a free number variable x. Then we can ¬nd an

L-formula B such that

B ” A(#(B)) .

T

The free variables of B are those of A(x) except for x. In particular, if x is the

only free variable of A, then B is an L-sentence.

Proof. Put d(z) = sub(z, #(x), num(z)). Thus d is a 1-ary primitive recursive

function such that, if A(x) is any L-formula containing the number variable x

as a free variable, then d(#(A)) = #(A(#(A))). Now given A(x) as in the

hypothesis of the lemma, let D(x) be the formula A(d (x)), and let B be the

formula A(d (#(D))), i.e., D(#(D)). Note that d(#(D)) = #(B). It follows

that PRA d(#(D)) = #(B). Since T includes PRA, it follows that T

A(d (#(D))) ” A(#(B)). In other words, T

d(#(D)) = #(B). Hence T

B ” A(#(B)). This completes the proof.

70

De¬nition 6.4.2. If M is any model of T , let TrueM be the set of G¨del

o

numbers of sentences that are true in M , i.e.,

TrueM = {#(B) : B is a sentence and vM (B) = T} .

De¬nition 6.4.3. An ω-model of T is a model M of T such that the number

domain of M is ω = {0, 1, 2, . . .} and 0M = 0 and SM (n) = n + 1 for all n ∈ ω.

More generally, if M is any model of T , we may assume that ω is identi¬ed

with a subset of the number domain of M in such a way that 0M = 0 and

SM (n) = n + 1 for each n ∈ ω. Thus each n ∈ ω is identi¬ed with with the

element of M that is denoted by n, i.e., n = vM (n).

Theorem 6.4.4 (unde¬nability of truth). If M is an ω-model of T , then

TrueM is not explicitly de¬nable over M . More generally, if M is any model of T ,

then the characteristic function of TrueM is is not included in the characteristic

function of any subset of M that is explicitly de¬nable over M .

Proof. Let X be a subset of the number domain of M which is explicitly

de¬nable over M . Let A(x) be an L-formula with a free number variable x and

no other free variables, such that A(x) explicitly de¬nes X over M . Applying

Lemma 6.4.1 to the negation of A(x), we obtain an L-sentence B such that

T B ” ¬ A(#(B)). Since M is a model of T , it follows that #(B) ∈ TrueM

if and only if #(B) ∈ X. Hence the characteristic function of TrueM is not

/

included in the characteristic function of X, q.e.d.

Corollary 6.4.5. Let M = (ω, +, ·, 0, 1, =) be the standard model of ¬rst order

arithmetic, Z1 . Then TrueM is not explicitly de¬nable over M . This1 may be

paraphrased by saying that arithmetical truth is not arithmetically de¬nable.

Remark 6.4.6. With M = (ω, +, ·, 0, 1, =) as above, it can be shown that

TrueM is implicitly de¬nable over M . (See also Exercise 6.4.7.) Thus the Beth

De¬nability Theorem does not hold for de¬nability over this particular model.

Exercise 6.4.7. Let M be an ω-model of Z1 or Z2 or ZFC. Let SatM be the

satisfaction relation on M . Show that SatM is implicitly de¬nable over M .

6.5 The Provability Predicate

In this section, let L be a primitive recursive language, and let T be an L-

theory which is primitive recursively axiomatizable. For example, T could be

PRA itself, or T could be any of the mathematical or foundational theories

discussed in Sections 5.2 and 5.3.

De¬nition 6.5.1. Choose a primitive recursive predicate AxT for the set of

G¨del numbers of axioms of T . In terms of AxT show that various predicates

o

1 This result is due to Tarski [3].