Start with a model of ZFC+, which also satisfies Generalized continuum hypothesis, and add one Cohen real by the countable forcing of finite binary sequences. Its countable chain condition for forcing preserves cardinals. For every infinite ground cardinal , a nice forcing name for a subset of is specified by countable forcing antichains of a countable forcing. The number of such forcing names is at most
in the ground model. The ground subsets already supply the preserved lower bound . Thus the extension still satisfies for every infinite cardinal, namely Generalized continuum hypothesis.
The Cohen real is not in the ground model: for each ground real it is dense to disagree at a new coordinate. Forcing leaves the ordinals unchanged, and constructible levels are absolute, so the extension has the same constructible universe as the ground model. The new real is therefore not constructible. We obtain
The forcing theorem makes this a relative-consistency construction. Thus, if ZFC is consistent, ZFC+Generalized continuum hypothesis does not prove . This is the one-Cohen-real preservation of GCH argument, not a claim that every arbitrary GCH-preserving forcing leaves unchanged.
Use -completeness in its usual forcing sense: every decreasing chain in a partial order of stronger conditions of length less than has a common stronger bound. Let and choose forcing that it functions the ground ordinal into the ground set . Below any stronger condition , recursively decide each value of in order. At a successor step the deciding conditions are dense, and at a limit stage use -completeness. After all steps take another common bound. The recursion and its choices can be performed in , using ground choice and closure, and it records a function in .
Thus below every stronger than there is a condition forcing for some ground . The set of such whole-function deciding conditions belongs to and is dense below . Genericity with makes meet : adjoin the conditions incompatible with to obtain a globally dense subset of a forcing order, and use directedness to rule out the incompatible alternative. A condition in then gives .
The reverse inclusion follows because ground functions remain functions with the same domain and values. Therefore
This closed forcing adds no short ground-valued sequences argument needs density of complete decisions. A single arbitrarily constructed lower bound need not belong to , and would not by itself prove the claim.
A cardinal-preserving forcing over leaves every ground-model cardinal number a cardinal in every generic extension. In the present notation, for every -generic filter and every ordinal ,
Set forcing preserves ordinals, and an old bijection witnessing that an ordinal is not a cardinal remains available. Thus this condition also means that the two models have exactly the same cardinals. Cardinality here is computed inside the respective models, not from their external sizes.
A well-pruned set-theoretic tree that is an Aronszajn tree and a Suslin tree gives a forcing with the countable chain condition for forcing: stronger nodes extend weaker ones. The dense subsets of a forcing order of nodes at or above each level cannot all be met by a filter in an ordered set, since that would produce a cofinal branch. Thus fails. When the continuum exceeds , full Martin axiom includes this instance.