Fix names and a first-order formula . Using the syntactic forcing relation, form in the name
This is a set by the axiom schema of separation in . If and , then the forcing theorem gives both and . Conversely, if satisfies , choose with and . The truth direction of the forcing theorem supplies forcing ; directedness of gives below both and , so .
Thus
Every instance has such a witness, so separation in a generic extension proves Separation.

Articles by others on the same topic (0)

There are currently no matching articles.