A generic set A cannot be implicitly defined. Proof: suppose φ in ℒ(PA+G) defines the class {A}, i.e., (ℕ,B)⊧φ iff B=A. Since (ℕ,A)⊧φ, by the Truth Lemma A⊩*φ, i.e., p⊩*φ for some p with A⊧p. But there certainly exists a generic B≠A also satisfying p, since p makes assertions about only finitely many numbers. (Use the Existence Lemma.) By the Truth Lemma again, we must have (ℕ,B)⊧φ and so φ does not define {A}.
To prove Feferman’s theorem, we just have to perform the Existence Lemma hyperarithmetically. By the Definability Lemma, the forcing relation is hyperarithmetic, i.e., there is a Δ11 formula forces(x,y) in ℒ2(PA) such that p⊩*φ iff ℕ⊧forces(⌜p⌝,⌜φ⌝), for all closed formulas φ in ℒ2(PA+G). The inductive construction of the generic set A proceeds by defining ever longer conditions p0,p1,…, with p0 equal to some arbitrary condition c. The definition of pn+1 from pn looks like this:
if pn⊩*¬φn+1
then pn+1=pn, and
if q≥pn, q⊩*φn+1, and q is the first such condition
then pn+1=q
or in symbols (and omitting the usual ⌜ ⌝ for readability):
| [forces(pn,¬φn+1) →pn+1=pn] ∧ | |
| ∀q[q≥pn ∧forces(q,φn+1) ∧ | |
| ∀r(r<q∧r≥pn → ¬forces(r,φn+1)) | |
| →pn+1=q] |
We conclude that the function pn+1=f(n,pn) is hyperarithmetic. (The formula obviously defines a hyperarithmetic relation; it’s a function because of the negation clause in the definition of forcing.) Now, this is exactly the situation we examined at the end of post 30. We saw that ⋃pn, which is A, is hyperarithmetic.
So Feferman’s theorem is proved: there is a hyperarithmetic set that is not implicitly definable. Feferman actually proved a stronger result: there are an infinite number of “arithmetically independent” sets. I won’t go into details.
We can squeeze a little more out of the proof we gave. Not only is the generic set A hyperarithmetic, but it can be “mutually implicitly defined” with the forcing relation. If we augment ℒ(PA) to ℒ(PA+F+G) by adding two new predicates, then the pair (⊩*,A) can be implicitly defined: there is a closed formula in ℒ(PA+F+G) which holds when and only when F represents the forcing relation and G represents the generic set A. It’s no sweat to code the pair (⊩*,A) into a single B⊆ℕ, say by coding ⊩* in the odd positions and A in the even ones. (So p⊩*φ iff 2〈⌜p⌝,⌜φ⌝〉+1∈B, and x∈A iff 2x∈B.) Thus B is implicitly defined. But B intersected with the even numbers is basically A, and is not implicitly definable. This proves an earlier remark, about how implicit definability is not closed under intersection.
A variation on the theme: Addison’s theorem, which says that the class of arithmetic sets (call it 𝒜) is not an arithmetic class. If 𝒜 were an arithmetic class, that would mean there was a closed formula ψ in ℒ(PA+G) such that
A∈𝒜↔(ℕ,A)⊧ψ
Now, ψ has a certain complexity depth, say d. Although no generic set can be arithmetic, we can construct a “d-generic” arithmetic set, where:
A⊆ℕ is d-generic iff for every closed formula φ in ℒ(PA+G) of complexity depth ≤d, either A⊩*φ or A⊩*¬φ.
We just mimic the original proof of the Existence Lemma, but looking only at formulas of complexity depth ≤d, and using the fact that forcesd is arithmetic, as noted in post 32.
The proof of the Truth Lemma adapts immediately to show that
If A is d-generic, and φ has complexity depth ≤d, then A⊩*φ iff (ℕ,A)⊧φ.
Assume that A is d-generic and arithmetic, where d is the complexity depth of ψ, the formula defining the class 𝒜 of arithmetic sets. Since A is arithmetic, (ℕ,A)⊧ψ. By the adapted Truth Lemma, A⊩*ψ, i.e., for some p with A⊧p, we have p⊩*ψ. Now let B⊧p be generic (not just d-generic). By the original Truth Lemma, this implies that (ℕ,B)⊧ψ and hence B is arithmetic. But we know that no generic set can be implicitly defined, let alone arithmetic. QED
Addison proved a somewhat stronger theorem; see Rogers (Ex.16–73, p.452) for the details.
