Generic Logical Semantics of Justifications
What kind of logical objects are justifications? When asked in a mathematical context, “What is a predicate?,” we have a ready answer: a subset of a Cartesian product of the domain set.
We know a reasonable mathematical answer (within Kolmogorov's model) to the question, “What is probability?”: a function from a ^-algebra of events to [0,1], with some natural conditions imposed. Within an exact mathematical theory, there should be a similar kind of answer to the question, “What is a justification?” In addition to its conceptual value, clarity on this issue should also lead to cleaner mathematical models.We consider this question in its full generality, which, surprisingly, yields a clean and meaningful answer. As in Chapter 2 we assume the language of justification logic consists of two disjoint sets of syntactic objects:
(1) a set of justification terms Tm. Naturally, the set of terms of any Justification Logic considered in this book is covered by this (Definition 2.1).
(2) a set of formulas Fm, built inductively from propositional variables, Var, using Boolean connectives and the justification formula formation rule: if F is a formula and t a justification term (t ∈ Tm), then t:F is again a formula (Definition 2.2).
In classical logic an assignment of truth values to the propositional variables, Var, completely determines the truth values for all propositional formulas, using the familiar Boolean conditions. For a justification language more is needed because the Boolean conditions don't supply truth values for formulas of the form t:F. To handle this, a semantic meaning must be supplied for justification terms, members of Tm. The following places minimal requirements on such a semantics, giving us the simplest ontology for justification logic. The meaning assigned to formulas is a classical truth value, and we retain classical logic behavior for propositional connectives.
We write 0 for false and 1 for true, so that our space of truth values is {0,1). The key item is the meaning of justification terms, and this will be a set of formulas. Eachjustification term is simply interpreted as the set of formulas for which it is a justification. There are loose similarities between this and neighborhood models for modal logics, in which one simply announces arbitrarily how necessitated formulas are to behave.Definition 3.1 (Basic Model) A basic model, typically called *, consists of an interpretation of the members of Var, propositional variables, and an interpretation of the members of Tm, meeting conditions given later. Overloading notation, we use * for a basic model, and also for the interpretations of Var and of Tm in that model.
The interpretation of a propositional in a basic model is a truth value. That is,
The interpretation of each justification term is a set of formulas. That is,
For a justification term t, we write the simpler expression t* for *(t), the interpretation of term t in basic model *.
Just as a truth value assignment to propositional variables extends to a valuation on all classical formulas, a basic model and its mappings do the same for justification formulas.
Definition 3.2 (Evaluation in a Basic Model) Let * be a basic model. It is easy to show that * determines a unique mapping from all formulas to truth
Note that while propositions are interpreted semantically, as truth values, justifications are interpreted syntactically, as sets of formulas. This is a principal hyperintensional feature: a basic model may treat distinct formulas F and
So far, a basic model is nothing but a classical propositional model in which justification assertions t:F are treated as independent propositional atoms.
This analogy will be abandoned when we turn to models for specific justification logics in which the various t:F are no longer independent and have to obey some constraints called closure conditions. In the meantime, this minimal construction already admits a generic justification semantics.
Theorem 3.4 (Basic Model Existence) Any classically consistent set of formulas S has a basic model, that is, there is a basic model in which its members are true.
'cl t:F.
Discussion
(1) Informally, a basic model of a set of formulas S is nothing but a maximal
consistent extension
of S over the classical logic base. What makes S a model rather than a syntactic logical structure is the set-theoretical reading of justification assertions
In the justification logic context,
this replaces logical identities with set-theoretic closure conditions. Instead of reasoning about logical connectives and axioms, we begin by reasoning about nonlogical objects. Specifically, we begin with sets (of formulas) and operations on these sets, with their own set-theoretical intuitions. This proves to be useful.
(2) A special case that falls under the scope of Theorems 3.4 and 3.6 is the conventional multimodal language. Each modality ?i∙ there can be viewed as a justification with reading
In classical logic CL without specific modal axioms, basic models for a modal language are the same as for any justification language with the matching set of justifications. However, adding modal and justification axioms lead to different classes of basic models.
As an example, consider the family of basic models for the multimodal version of K, BM(Km), where these models are in a language with modalities
This is a non-Kripkean semantics for modal logic K, with easy soundness and completeness theorems. It is unclear to what extent this semantics would be useful for modal logic. However, such basic models prove to be a potent tool in justification logics because the latter enjoy evidence tracking capabilities that provide more control over a model.
3.2