Forcing (mathematics) - Forcing

Forcing

Given a generic filter G⊆P, one proceeds as follows. The subclass of P-names in M is denoted M(P). Let M={val(u,G):u∈M(P)}. To reduce the study of the set theory of M to that of M, one works with the forcing language, which is built up like ordinary first-order logic, with membership as binary relation and all the names as constants.

Define p φ(u₁,…,u_n) (read "p forces φ in model M with poset P") where p is a condition, φ is a formula in the forcing language, and the u_i are names, to mean that if G is a generic filter containing p, then M ⊨ φ(val(u₁,G),…,val(u_n,G)). The special case 1 φ is often written P φ or φ. Such statements are true in M no matter what G is.

What is important is that this "external" definition of the forcing relation p φ is equivalent to an "internal" definition, defined by transfinite induction over the names on instances of u ∈ v and u = v, and then by ordinary induction over the complexity of formulas. This has the effect that all the properties of M are really properties of M, and the verification of ZFC in M becomes straightforward. This is usually summarized as three key properties:

• Truth: M ⊨ φ(val(u₁,G),…,val(u_n,G)) if and only if it is forced by G, that is, for some condition p ∈ G, p φ(u₁,…,u_n).
• Definability: The statement "p φ(u₁,…,u_n)" is definable in M.
• Coherence: If p φ(u₁,…,u_n) and q ≤ p, then q φ(u₁,…,u_n).

We define the forcing relation in V by induction on complexity, in which we simultaneously define forcing of atomic formulas by ∈-induction.

1. p a ∈ b if for any q ≤ p there is r ≤ q such that there is (s, c) ∈ b such that r ≤ s and r a = c.

2. p a = b if p a ⊆ b and p b ⊆ a

where

p a ⊆ b if for all q ≤ p and for all (r,c) ∈ a if q ≤ r then q c ∈ b.

3. p ¬ f if there is no q ≤ p such that q f.

4. p f ∧ g if p f and p g.

5. p ∀ x f if p f(a) for any name a where f(a) is result of replacing all free occurrences of x in f by a.

In 1–5 p is an arbitrary condition. In 1 and 2 a and b are arbitrary names and in 3–5 f and g are arbitrary formulas. This definition provides the possibility of working in V without any countable transitive model M. The following statement gives announced definability:

p f if and only if M ⊨ p f.

(Where no confusion is possible we simply write .)