Here are the key facts about forcing, as we’ve defined it. As before, φ is a closed formula in ℒ(PA+G).
- Extension Lemma:
- If p⊩*φ and q≥p, then q⊩*φ.
- Truth Lemma:
- If A is generic, then A⊩*φ iff (ℕ,A)⊧φ.
- Empty Condition Lemma:
- If φ belongs to ℒ(PA) (no G’s), then ∅⊩*φ iff ℕ⊧φ.
- Definability Lemma:
- The relation p⊩*φ is implicitly definable, and hence hyperarithmetic. (Of course, the pairs (p,φ) have to be suitably coded.) Also, forcing for φ of complexity depth ≤d is arithmetic, for every d.
- Existence Lemma:
- There exists a generic set satisfying any given condition p0.
The proofs of the first three lemmas amount to turning the “complexity induction” crank, with an occasional wrinkle. I repeat the inductive clauses for convenience.
- p⊩* s=t ↔ ℕ⊧s=t, where s and t are closed terms in ℒ(PA).
- p⊩* G(n) ↔ p(n)=1.
- p⊩* α∨β ↔ p⊩*α or p⊩*β.
- p⊩* ¬φ ↔ there is no q≥p with q⊩*φ.
- p⊩* ∃xφ(x) ↔ for some n∈ℕ, p⊩*φ(n).
Start with the Extension Lemma. Suppose q≥p. Atomic sentences come in two varieties, s=t and G(n), and clauses (1) and (2) of the definition of ⊩* dispose of both cases immediately. For ¬φ, “no extension of p does foo” implies “no extension of q does foo” because all extensions of q are extensions of p. Clause (3) makes short work of the case α∨β, and clause (5) of the case ∃xφ(x).
Clause (4) and the Extension Lemma make a nice couple. Clause (4) says that p⊩*¬φ is equivalent to “no extension of p strongly forces φ’’, while the Extension Lemma says that p⊩*φ is equivalent to “every extension of p strongly forces φ’’. If some but not all extensions of p strongly force φ, then p strongly forces neither φ nor its negation. Contrast this with the definition of a generic set.
The Extension Lemma also tells us that we cannot have both A⊩*φ and A⊩*¬φ, for any subset A (generic or not). Proof: if not, then we have p1⊩*φ and p2⊩*¬φ for conditions p1 and p2 both satisfied by A. But p1 and p2 have a common extension, say q, so we would have q⊩*φ and q⊩*¬φ. As we’ve seen, this can’t happen.
Now combine the previous paragraph with the definition of generic, and we have the important fact:
For a generic A, A⊩*¬φ iff not A⊩*φ.
This makes the proof of Truth Lemma entirely routine. For the negation case:
A⊩*¬φ ⇔ not A⊩*φ ⇔ not (ℕ,A)⊧φ ⇔ (ℕ,A)⊧¬φ
with the middle ⇔ being the inductive hypothesis. The other cases are handled in the same manner.
Next, the Empty Condition Lemma. The only case not utterly trivial is negation. The key is an “all or nothing” property for φ in ℒ(PA): either all conditions strongly force φ, or no conditions strongly force φ. Given this, the induction is routine. The proof of the all or nothing property is itself an induction. Only negation calls for attention. Observe that if all conditions strongly force φ, then no conditions strongly force ¬φ, and if no conditions strongly force φ, then all conditions strongly force ¬φ. So the all or nothing property for φ entails it for ¬φ.
The Definability Lemma: The clauses of the definition of ⊩* lend themselves to an implicit definition of the class {〈⌜p⌝,⌜φ⌝〉: p⊩*φ}. Here 〈,〉 is a recursive pairing function and ⌜p⌝ is the code for the condition as described in post 30 (length plus binary). It’s completely analogous to the implicit definition for truth we gave in post 29 (using the predicate letter T) : we add a new predicate forces and write out the clauses in the augmented language. We can also write a definition forcesd in ℒ(PA) of forcing for all closed φ in ℒ(PA)+G of depth (or degree) less than or equal to d. Here you first inductively define forcesd+1 in terms of forcesd. Then you repeatedly expand things out. So, expanding all occurrence of forcesd in forcesd+1 leaves you with a definition using only forcesd−1, and so on down. See the Logic Notes for more details (the definition of trued).
Finally, the Existence Lemma. Enumerate all the closed formulas of ℒ(PA)+G, say {φn:n=1,2,…}. We define a sequence of conditions p0≤p1≤p2≤… so that for each n>0, either pn⊩*φn or pn⊩*¬φn. This is easy: p0 is given to us. For pn+1, either pn⊩*¬φn+1 or not (pn⊩*¬φn+1); in the latter case, some extension q≥pn strongly forces φn+1. In the first case let pn+1=pn, in the second let pn+1 be the first extension of pn that strongly forces φn+1. (For “first”, we can use any definable linear ordering of the conditions; the easiest is just to order them by their codes.) Now let A=⋃pn, a set satisfying all the conditions. (Fill out the bitstring for A with trailing 0’s in case the pn’s have an upper bound in length—but this can’t happen, see next paragraph.) Obviously A is generic and satisfies p0.
If the pn’s did have an upper length bound, then our construction would give a generic finite set A. Say all elements of A are less than n0, so (ℕ,A)⊧∀n[G(n)→n<n0]. By the Truth Lemma, some p⊩*∀n[G(n)→n<n0]. Now extend p to a q with a 1 in a spot after n0, i.e., q(n1)=1 with n1>n0. By the Extension Lemma q⊩*∀n[G(n)→n<n0]. Now use the Existence Lemma with p0=q, constructing a generic set B⊧q. By the Truth Lemma applied to B, (ℕ,B)⊧∀n[G(n)→n<n0]. So all elements of B are less than n0, but n1 is an element of B, contradiction.
This is a typical use of the lemmas. Exercise: adapt the argument to show that any generic set contains and omits an infinite number of primes.
Diagonal Argument 