Timeline for Definability of the ground model in its class-forcing extension

5 events

when toggle format	what		by	license	comment
Mar 1, 2021 at 20:05	comment	added	Johannes Schürz		Cohen forcing on $\alpha$ squared, which is obviously a complete subforcing of $P \times P$, and $G(\alpha) \times H(\alpha) \subseteq \mathbb{C}_\alpha \times \mathbb{C}_\alpha$ is the generic filter added by $G \times H$.
Mar 1, 2021 at 6:32	comment	added	Seba Thei		What is $C_\alpha \times C_\alpha$?
Feb 28, 2021 at 23:31	comment	added	Johannes Schürz		Since $P \times P$ has the Ord-c.c. (all antichains are sets, which in particular implies that this forcing behaves quite nicely, e.g. the Forcing relation is definable and the Forcing theorem holds) there exists a regular $\alpha$ such that $p \in P\restriction \alpha \times P\restriction \alpha$ and $\dot{a}$ is a $ P\restriction \alpha \times P\restriction \alpha$-name. Now we define an automorphism on $\mathbb{C}_\alpha \times \mathbb{C}_\alpha $ such that $\pi(p_1,p_2):=(p_2, p_1)$. Now $\pi$ fixes $p$ and $\dot{a}$, but $\pi(G(\alpha))=H(\alpha)$.
Feb 28, 2021 at 20:25	history	edited	gmvh		Added top-level tag
Feb 28, 2021 at 18:42	history	asked	Seba Thei	CC BY-SA 4.0