To specify these problems formally, a suitable encoding of the members of \(\text{Form}_{\mathcal{L}}\) and \(\mathfrak{A}\) as finite binary strings must be provided. Although this is typically unproblematic in the case of \(\text{Form}_{\mathcal{L}}\), \(\mathfrak{A}\) may sometimes include infinite structures. In this case, the model checking problem is only considered for finite structures (which we must also assume are encoded as finite strings – e.g. in the manner described by Marx 2007). And in cases where a logic is standardly characterized proof theoretically rather than semantically – i.e. as the set of formulas derivable from some set of axioms of \(\Gamma_{\mathcal{L}}\) rather than the class of formulas true in all structures – the validity problem is understood to coincide with the problem of deciding whether \(\phi\) is derivable from \(\Gamma_{\mathcal{L}}\). In such cases, the satisfiability and model checking problems are generally not considered.