In addition, there is a different kind of semantics, so-called modular semantics, which focuses on making more transparent the ontological status of justifications. Within modular semantics propositions receive the usual classical truth values and justifications are interpreted syntactically as sets of formulas. We retain a classical interpretation \(\ast\) of the propositional formulas \(Fm\), which, in the case of a single world, reduces to \[\ast: Fm \mapsto\ \ \{0,1\}\] i.e., each formula gets a truth value 0 (false) or 1 (true), with the usual Boolean conditions: \({\Vdash}A\rightarrow B\) iff \(\not\Vdash A\) or \({\Vdash}B\), etc. The principal issue is how to interpret justification terms. For sets of formulas \(X\) and \(Y\), we define \[X\cdot Y = \{ F \mid G{\rightarrow}F \in X\ \mbox{and} \ G \in Y\ \mbox{for some}\ G\}.\] Informally, \(X\cdot Y\) is the result of applying Modus Ponens once between all members of \(X\) and of \(Y\) (in that order). Justification terms Tm are interpreted as subsets of the set of formulas: \[\ast: Tm \mapsto\ \ 2^{Fm}\] such that \[(s\cdot t)^\ast\supseteq s^\ast\cdot t^\ast \ \ \mbox{and}\ \ \ (s+t)^\ast\supseteq s^\ast\cup t^\ast .\] These conditions correspond to the basic justification logic \(\textsf{J}\); other systems require additional closure properties of \(\ast\). Note that whereas propositions in modular models are interpreted semantically, as truth values, justifications are interpreted syntactically, as sets of formulas. This is a principal hyperintensional feature: a modular model may treat distinct formulas \(F\) and \(G\) as equal in the sense that \(F^\ast = G^\ast\), but still be able to distinguish justification assertions \(t{:}F\) and \(t{:}G\), for example when \(F \in t^\ast\) but \(G\not\in t^\ast\) yielding \({\Vdash}t{:}F\) but \(\not\Vdash t{:}G\). In the general possible world setting, formulas are interpreted classically as subsets of the set \(W\) of possible worlds, \[\ast: Fm \mapsto\ \ 2^W ,\] and justification terms are interpreted syntactically as sets of formulas at each world \[\ast: W\times Tm \mapsto\ \ 2^{Fm}.\] Soundness and completeness of Justification Logic systems with respect to modular models have been demonstrated in Artemov (2012; Kuznets and Studer 2012).