 as modal formulas are evaluated at certain points. The intuition is that the modal operator \(\square\) is a kind of universal quantifier and modal structures are first-order relational structures with a binary relation and a collection of subsets of the universe. In a first-order language, to talk about these structures one needs a binary relation symbol, \(S\), as well as a collection of unary relation symbols. This language is called first-order correspondence language because every basic modal formula corresponds to a first-order formula. The standard translation of a modal formula \(\varphi\) is a first-order formula with one free variable expressing the semantics of modal formulas: