Definition (Semantic forcing predicate). p⊩M,ℙφ: Forall G ℙ-generic over M with p∈G, M[G]⊨φ.
“p forces φ”
We often omit M,ℙ.