Use standard notation for forcing: means that is stronger. A generic filter is nonempty, upward closed and downward directed, and meets every dense subset of a forcing order in the ground model. Names below are forcing names in , with pairs ordered as .
The semantic forcing relation is
Here is the evaluation of a forcing name. Countability of supplies such generic filters through every condition by the Rasiowa–Sikorski lemma.
Define the syntactic forcing relation by mutual well-founded recursion on the forcing names for the atomic cases, then induction on the first-order formula. Its membership clause is
For equality, first abbreviate
and set exactly when both inclusions hold. Each recursive call lowers the rank of at least one forcing name without raising the other. This makes the mutual recursion well-founded.
For a basis of connectives consisting of logical conjunction, negation and existential quantification, the remaining clauses are
The last line is the existential clause of syntactic forcing; witnesses need only occur densely, rather than be forced by itself with one preselected name. Other connectives are defined by logical abbreviations. The recursion gives a definable relation inside for each fixed first-order formula, with quantification over the class of its names. If has no greatest element, use canonical forcing names , which still evaluate to . It also proves monotonicity: strengthening a condition preserves what it forces. The forcing theorem identifies the two relations and supplies the truth lemma.

Articles by others on the same topic (0)

There are currently no matching articles.