Forcing

Definition

A forcing notion is a partial order $(P, \le)$ with a greatest element $1$. Its elements are called conditions, and $q \le p$ is read "$q$ is stronger than $p$".

Let $M$ be a countable transitive model of ZFC with $P \in M$. A $P$-name is a set $\tau$ of pairs $(\sigma, p)$, where $\sigma$ is a $P$-name and $p \in P$; this is a definition by recursion on rank. For a filter $G \subseteq P$, the value of a name is defined by recursion: $$\tau^G = \set{\sigma^G : (\sigma, p) \in \tau \text{ for some } p \in G}.$$ For a generic filter $G$ over $M$, the forcing extension is $M[G] = \set{\tau^G : \tau \in M \text{ is a } P\text{-name}}$. Let $p \in P$, let $\varphi(x_1, \ldots, x_n)$ be a formula, and let $\tau_1, \ldots, \tau_n \in M$ be names. The condition $p$ forces $\varphi(\tau_1, \ldots, \tau_n)$, written $p \Vdash \varphi(\tau_1, \ldots, \tau_n)$, if $M[G] \models \varphi(\tau_1^G, \ldots, \tau_n^G)$ for every generic $G$ over $M$ with $p \in G$.