Let be any set in the extension. The set belongs to . Ground-model choice well-orders it, so fix an enumeration by an ordinal in . In , takeEvaluation gives a surjection from onto . This is a set function by the ZF part of the forcing theorem; no extension choice is needed. For each , take its least preimage ordinal. Distinct have distinct least preimages, which well-order by their inherited ordinal order. Since every extension set has a forcing name, every set in is well-orderable. ThereforeThis choice preservation by well-ordered names tolerates repeated evaluations, because the least-index step removes them canonically.
Articles by others on the same topic
There are currently no matching articles.