Let be a Transitive Model. Let 𝟙 be a Forcing Partial Order and denote by the Model Extension of by some . Furthermore, let be the Forcing Language with the Forcing Sentences . A relation on is a forcing relation if for any that is a -Generic Filter over , any formula with Free Variables and any Names (i.e. constants in ) the following equivalence holds: Additionally, we require that is downwards closed i.e.