We have seen that logic provides many examples of problems which are studied in complexity theory. Of these, the most often considered are satisfiability, validity, and model checking. In order to formulate these problems uniformly, it is convenient to take a logic \(\mathcal{L}\) to be a triple \(\langle \text{Form}_{\mathcal{L}}, \mathfrak{A}, \models_{\mathcal{L}} \rangle \) consisting of a set of formulas \(\text{Form}_{\mathcal{L}}\), a class of structures \(\mathfrak{A}\) in which the members of \(\text{Form}_{\mathcal{L}}\) are interpreted, and a satisfaction relation \(\models_{\mathcal{L}}\) which holds between structures and formulas. We may assume that \(\text{Form}_{\mathcal{L}}\) is specified in the manner typified by propositional logic – i.e. as a set of syntactic primitives and inductive formulation rules. On the other hand, the definitions of both \(\mathfrak{A}\) and \(\models_{\mathcal{L}}\) will vary according to the sort of logic in question – e.g. in the case of classical propositional logic, \(\mathfrak{A}\) will be the class of atomic valuations \(v:\mathbb{N} \rightarrow \{0,1\}\) and \(v \models_{\mathcal{L}} \phi\) holds just in case \(\phi\) is true with respect to \(v\) (as defined by the usual truth table rules), and in the case of modal logic \(\mathfrak{A}\) will typically be a class of Kripke models satisfying a given frame condition and \(\models_{\mathcal{L}}\) is the standard forcing relation \(\mathcal{A},w \Vdash \phi\) which holds between a model, a world, and a formula.