Models for J0 and J
So far basic models may seem to have only a tenuous connection with justification logics. Theorem 3.6 gives completeness with respect to classical logic, for instance. But the machinery we have provided is, in fact, sufficiently general.
Recall Definition 2.6—to build a justification logic axiomatically, we start with J0, in which only two axiom schemes are added to classical logic. Then other justification logics can be constructed from J0 with the addition of further axiom schemes. Finally a constant specification, CS, is added whose members act like specific axioms. In this way we get a justification logic with a constant specification, JL(CS). But instead of thinking of JL(CS) as built on J0 we can think of it as built on classical logic itself, by the addition of the J0 axiom schemes, the axiom schemes special to J, and members of CS taken as axioms. Then hjl,∙cs, X, that is, provability in a justification logic (Definition 2.8), can be thought of as derivability in classical logic,
X, where S is the entire set of added axiom schemes and axioms. This way of viewing things, at least potentially, turns any justification logic into something a basic model might be useful for. In this section we start the process of showing just how useful the result can be.
Recall Definition 2.3, of justification logic J0, in which the set Tm of terms is built up from variables and constants constructed using the operations application, ∙, and sum, +. The set Fm of formulas is defined accordingly. The axioms of J0 are those of classical logic CL enhanced by two principles
Then, basic J0-models are the basic models in which both of these principles hold. Importantly, we will soon see that a more structural characterization is possible.
Definition 3.8 For sets of formulas X and Y, we define
Informally, X. Y is the result of applying modus ponens once to all members of X and of Y (in a given order).
Theorem 3.9 BM(J0) is the class of basic models in which the following closure conditions are met
Definition 3.10 Let CS be a constant specification. A basic CS-model is a basic model in which all formulas from CS hold.
Recall from Section 2.6 that we use J(CS) when we are dealing with J0 extended with constant specification CS.
Corollary 3.11 The basic models for J(CS), that is BM(J(CS)), are the basic CS-models for J0. J(CS) is sound and complete with respect to BM(J(CS)).
Note that in the closure conditions of Theorem 3.9, one cannot replace either of inclusions c by equalities = without violating the completeness Theorem 3.6. A verification for each of the two cases follows.
Example 3.12 (Application closure) We designate a justification constant to play a special role. Suggestively we use 0 as this constant. Consider the justification logic
Examples 3.7. all hold for J0 instead of CL because all the interpretations * enjoy the J closure conditions from Theorem 3.9. In particular, in 1, t* = @ for all t and the closure conditions hold vacuously.
3.3