|
If
 is a transitive model of set theory and  is a partial order then we can define a forcing relation:
( forces
 )
for any  , where
 are  - names.
Specifically, the relation holds if for every generic filter  over  which contains  ,
That is,  forces  if every extension of
 by a generic filter over  containing  makes  true.
If
 holds for every  then we can write
 to mean that for any generic
 ,
![$ \mathfrak{M}[G]\vDash\phi$](http://images.planetmath.org:8080/cache/objects/3238/l2h/img23.png "$ \mathfrak{M}[G]\vDash\phi$") .
| 
![$\displaystyle \mathfrak{M}[G]\vDash \phi(\tau_1[G],\ldots,\tau_n[G])$](http://images.planetmath.org:8080/cache/objects/3238/l2h/img12.png "$\displaystyle \mathfrak{M}[G]\vDash \phi(\tau_1[G],\ldots,\tau_n[G])$"){kind=small}