# forcing relation

If $\U0001d510$ is a transitive^{} model of set theory^{} and $P$ is a partial order^{} then we can define a *forcing relation*:

$$p{\u22a9}_{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$,

$$\U0001d510[G]\models \varphi ({\tau}_{1}[G],\mathrm{\dots},{\tau}_{n}[G])$$ |

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

If $p{\u22a9}_{P}\varphi $ holds for every $p\in P$ then we can write ${\u22a9}_{P}\varphi $ to mean that for any generic $G\subseteq P$, $\U0001d510[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 |