CCC forcing cannot create diamond
ID: ccc-forcing-cannot-create-diamond
For each index, collect the ground subsets which some condition forces to be the corresponding diamond guess. Distinct forced values have incompatible witnessing conditions, so the countable chain condition for forcing makes this a countable family. Every ground subset is guessed by these families on a ground stationary set, by testing each ground club set. The countable-family diamond equivalence then yields diamond in the ground model. A generic guess need not itself be a ground subset; only values forced equal to one are collected.
New to topics? Read the docs here!