Computability Theory

116 Computability Theory

Proof. For any k-ary primitive recursive relation R, the graph of its characteristic func-

tion is defined in arithmetic by some expression ρ(x

1

, . . . , x

k

, x

k+1

). Then, R is defined

in arithmetic by the expression ρ(x

1

, . . . , x

k

, S0). a

Corollary: Every 6

1

relation is definable in arithmetic.

Proof. We showed on page 82 that any 6

1

relation had the form {Es | ∃t Q(Es, t)} for a

primitive recursive relation Q. We know that Q is definable; add one more quantifier

to define {Es | ∃t Q(Es, t)} in arithmetic. a

Digression: Work by Martin Davis, Yuri Matiyacevich, Hilary Putnam, and Julia

Robinson has shown that any 6

1

relation is definable ...