A forcing name is built by well-founded recursion: every member of a -name is a pair with and itself a -name of lower forcing name rank. In the ground model all such forcing names form the recursively defined class . Its evaluation by a generic filter is
The recursion is on forcing name rank, not on the forcing order. Forcing names need not have a unique evaluation across different generics, and many different forcing names may have the same evaluation.
The forcing truth lemma says that for a formula and ground-model forcing names ,
The forcing relation is the ground-model relation furnished by the forcing theorem. The witnessing condition must belong to the particular generic filter, not merely to the forcing order.
A forcing preserves cofinalities over if every generic extension has
The two values are compared as ordinals, using preservation of ordinals by forcing. Equivalently the forcing asserts that no ground ordinal acquires a smaller cofinality. The assertion concerns all ordinal cofinalities, not just that one specified cardinal remains uncountable.

Articles by others on the same topic (0)

There are currently no matching articles.