Definition (Forcing language). Fix $M$ a countable transitive model of $\mathsf{\text{ZFC}}$, $\mathbb{P}\in M$ a forcing poset.

We call the language

$$L_{\text{forcing}}:=L_{\in }\cup \{\tau :\mathbb{P}\mathbf{\text{-names}}\}$$

the forcing language (over $M$).