Our unexplained notation is that of Rogers [4]. Let P ⊆ 2N × 2N. We call a sequence <An: n ∈ N> of subsets of N a P-sequence iff ∀n(An+1 = the unique B such that P(An, B)).

Theorem. Let P ⊆ 2N × 2N be arithmetical. Then there is no P-sequence <An: n ∈ N> such that ∀n(A′n+1 ≤T An).

This theorem improves a result of Friedman [2] who showed that for no arithmetical P is there a P-sequence <An: n ∈ N> such that An + 1 is a code for an ω-model of the relative arithmetic comprehension schema, and An + 1 is present in the model coded by An, for all n. Other related results are those of Harrison [3], who showed there is a sequence <An: n ∈ N> such that ∀n<A′n + 1 ≤T An>, and of Enderton and Putnam [1], who showed there is no sequence <An: n ∈ N> with ∀n(A′n + 1 ≤T An) and A0 hyperarithmetic.

Our theorem is closely connected to Gödel's second incompleteness theorem. Its proof is a recursion theoretic parallel to the proof of Gödel's theorem. In §2 we draw a version of Gödel's theorem as a corollary to ours.