forcing relation

If $𝔐$ is a transitive model of set theory and $P$ is a partial order then we can define a forcing relation:

$$p{⊩}_P\varphi ({\tau }_1,\mathrm{\dots },{\tau }_n)$$

($p$ forces $\varphi ({\tau }_1,\mathrm{\dots },{\tau }_n)$)

for any $p\in P$, where ${\tau }_1,\mathrm{\dots },{\tau }_n$ are $P$- names.

Specifically, the relation holds if for every generic filter $G$ over $P$ which contains $p$,

$$𝔐[G]\models \varphi ({\tau }_1[G],\mathrm{\dots },{\tau }_n[G])$$

That is, $p$ forces $\varphi$ if every of $𝔐$ by a generic filter over $P$ containing $p$ makes $\varphi$ true.

If $p{⊩}_P\varphi$ holds for every $p\in P$ then we can write ${⊩}_P\varphi$ to mean that for any generic $G\subseteq P$, $𝔐[G]\models \varphi$.

Title	forcing relation
Canonical name	ForcingRelation
Date of creation	2013-03-22 12:53:28
Last modified on	2013-03-22 12:53:28
Owner	Henry (455)
Last modified by	Henry (455)
Numerical id	5
Author	Henry (455)
Entry type	Definition
Classification	msc 03E35
Classification	msc 03E40
Related topic	Forcing
Defines	forcing relation
Defines	forces