Shepherdson’s Representation Theorems

We have already remarked that at the time of Gödel’s proof, the only known way of showing the set P* of Peano Arithmetic to be representable in P.A. involved the assumption of ω-consistency. Well, in 1960, A. Ehrenfeucht and S. Feferman showed that all Σ1-sets can be represented in all simply consistent axiomatizable extensions of the system (R). Hence, all Σ1-sets can be shown to be representable in P.A. under the weaker assumption that P.A. is simply consistent. Their proof combined a Rosser-type argument with a celebrated result in recursive function theory due to John Myhill which goes beyond the scope of this volume. Very shortly after, however, John Shepherdson [1961] found an extremely ingenious alternative proof that is more direct and which we study in this chapter. [In our sequel to this volume, we compare Shepherdson’s proof with the original one. The comparison is of interest in that the two methods are very different and the proofs generalize in different directions which are apparently incomparable in strength.] We recall that for each n > 1, a system S is called a Rosser system for n-ary relations if for any Σ1-relations R1(x1,..., xn) and R2(X1, ..., xn), the relation R1 — R2 is separable from R2 — R1 in S. We wish to prove the following theorem and its corollary (Th. 1 below). Theorem S1—Shepherdson’s Representation Theorem. If S is a simply consistent axiomatizable Rosser system for binary relations (n-ary relations for n = 2), then all Σ1-sets are representable in S. Theorem 1—Ehrenfeucht, Feferman. All Σ1-sets are representable in every consistent axiomatizable extension of the system (R). Shepherdson’s Lemma and Weak Separation For emphasis, we will now sometimes write “strongly separates” for “separates”. We will say that a formula F(v1) weakly separates A from B in S if F(v1) represents some superset of A disjoint from B, We showed in the last chapter (Lemma 1) that strong separation implies weak separation provided that the system S is consistent. We also say that a formula F(v1,. .. ,vn) weakly separates a relation R I (x1 , . .. ,xn) from .R2(x1,... ,xn) if F(v1, ..., vn) represents some relation R’(x1,. .. ,xn) such that R1 ⊆ R1’ and R1 is disjoint from -R2.