For the reverse implication, suppose and . By the existential clause of syntactic forcing, the set
is dense below ; the existential quantifier ranges over forcing names of . Definability of the syntactic forcing relation and axiom schema of separation put in .
To apply genericity, augment it to the globally dense set
A condition compatible with has an extension below , then one in , and an incompatible condition already lies in . Thus is a dense subset of a forcing order in . The generic filter meets it. Since , directedness prevents from containing a condition incompatible with , so some exists.
There is consequently a name with . The assumed truth lemma gives , and hence
Together with part (a), this completes the existential step of the forcing theorem without assuming the desired existential truth lemma in advance.

Articles by others on the same topic (0)

There are currently no matching articles.