Let be the Language of set theory. Fix a countable Transitive Model. Let be Forcing Partial Order. Add all Names in as constant symbols to . The new language obtained is the forcing language, denoted by .