Nice name

Formal definition

Let M ⊨ ZFC be transitive, ( P , < ) a forcing notion in M , and suppose G ⊆ P is generic over M . Then for any P -name in M , τ ,

η is a nice name for a subset of τ if η is a P -name satisfying the following properties:

(1) dom ( η ) ⊆ dom ( τ )

(2) For all P -names σ ∈ M , { p ∈ P | ⟨ σ , p ⟩ ∈ η } forms an antichain.

(3) (Natural addition): If ⟨ σ , p ⟩ ∈ η , then there exists q ≥ p in P such that ⟨ σ , q ⟩ ∈ τ .