Justification Logics in General
The core justification logic J0 is extended to form other justification logics using two quite different types of machinery. First, one can add new operations on justification terms, besides the basic + and ∙, along with axiom schemes governing their use, similar to Sum and Application.
This is directly analogous to the way axiom schemes are added to K to create other modal logics. Second,
Example 2.4. We devote most of this section to the second kind of extension. It is, in fact, the intended role for justification constants that, up to now, have not been used for anything special.
For the time being let us assume we have a justification logic resulting from the addition of function symbols and axiom schemes to J0. The details don't matter for now, but it should be understood that our axioms may go beyond those for J0.
Axioms of justification logics, like axioms generally, are simply assumed and are not analyzed further. The role of justification constant symbols is to
serve as reasons Orjustifications for axioms. If A is an axiom, we can simply announce that constant symbol c plays the role of a justification for it. It may be that some axioms are assumed to have such justifications, but not necessarily all. Suppose we look at Example 2.4 again, and suppose we have decided that (X Λ Y) → X is an axiom for which we have a specific justification, let us say the constant symbol c plays this role. Similarly let us say the constant symbol d represents a justification for (X Λ Y) → Y. Examining the derivation given in Example 2.4, it is easy to see that if we replace the variable u throughout by c, and the variable v throughout by d we still have a derivation, but one of
If we add c.((X Λ Y) → X) and d:((X Λ Y) → Y) to our axioms for J0, we can simply prove the formula
Roughly speaking, a constant specification tells us what axioms we have justifications for and which constants justify these axioms.
As we just saw, we can use a constant specification as a source of additional axioms. But there is an important complication. If A is an axiom and constant symbol c justifies it, c:A conceptually also acts like an axiom, and it too may have its own justification. Then a constant symbol, say d, could come in here too, as a justification for c:A, and thus we might want to assume d:c:A. This repeats further, of course. For many purposes exact details don’t matter much, so how constants are used, and for what purposes, is turned into a kind of parameter of our logics, called a constant specification.Definition 2.5 (Constant Specification) A constant specification CS for a given justification logic is a set of formulas meeting the following conditions.
One reason why constant specifications are treated as parameters can be discovered through a close look at Definition 2.3. It does not really provide an axiomatization for J0, but rather a scheme for axiomatizations. The axioms called Classical in that definition are not fully specified, and in common practice many classical logic axiomatizations are in use. Any set sufficient to derive all tautologies will do. Then many different axiomatizations for J0 would meet the required conditions, and similarly for any justification logic extending J0 as well. Because constants are supposed to be associated with axioms, a variety of constant specifications come up naturally. And because details like this often matter very little, treating constant specifications as a parameter is quite reasonable.
Definition 2.6 (Logic of Justifications with a Constant Specification) Let JL be a justification logic, resulting from the addition of function symbols to the language of J0 and corresponding axiom schemes to those of J0. Let CS be a constant specification for JL. Then JL(CS) is the logic JL with members of CS added as axioms (not axiom schemes), still with modus ponens as the only rule of inference.
Constant specifications allow for great flexibility. A constant specification could associate many constants with a single axiom, or none at all. Allowing for many could be of use in tracking where particular pieces of reasoning come from. Allowing none might be appropriate in dealing with axioms that have some simple form, say X → X, but where the size of X is astronomical. Or again we might want to use the same constant for all instances of a particular axiom schema, or we might want to keep the instances clearly distinguishable. If details don't matter at all for some particular purpose, we might want to associate a single constant symbol with every axiom, no matter what the form. Such a constant would simply be a record that a formula is an axiom, without going into particulars.
Some conditions on constant specifications have shown themselves to be of special interest and have been given names. Here is a list of the most common. There are others.
Definition 2.7 (Constant Specification Conditions) Let CS be a constant specification for a justification logic JL. The following requirements may be placed on CS.
Empty:
This amounts to working with JL itself. Epistemically one
can think of it as appropriate for the reasoning of a completely skeptical agent.
Finite: CS is a finite set of formulas. This is fully representative because any specific derivation in a Justification Logic will be finite and so will involve only a finite set of constants. 
Axiomatically Appropriate: For every axiom A and for every n > 0 there are
The working of justification axiom systems is specified as follows.
Definition 2.8 (Consequence) Suppose JL is a justification logic, CS is a
We conclude this section with some examples of theorems of justification logics.
For these we work with JL(CS) where JL is any justification logic and CS is any constant specification for it that is axiomatically appropriate. We assume JL has been axiomatized taking all tautologies as axioms, though taking “enough” would give similar results once we have Theorem 2.14.Example 2.9 ?P → ?P is a theorem of any normal modal logic. It has more than one proof. We could simply note that it is an instance of a tautology, X → X. Or we could begin with P → P, a simpler instance of this tautology, apply necessitation getting ?(P → P), and then use the K axiom ?(P → P) → (?P → ?P) and modus ponens to conclude ?P → ?P. While these are different modal derivations, the result is the same. But when we mimic the steps in JL(CS), they lead to different results.
Let t be an arbitrary justification term. Then t:P → t:P is a theorem of JL(CS) because it is an instance of a tautology. But also P → P is an instance of a tautology and so, because JL(CS) is assumed axiomatically appropriate, the constant specification assigns some constant to it; say c:(P → P) º CS. Because c:(P → P) → (t:P → [c ■ t]:P) is an axiom, t:P → [c ■ t]:P follows by modus ponens.
In justification logic, instead of a single formula ?P → ?P with two proofs we have two different theorems that contain traces of their proofs. Both t:P → t:P and t:P → [c ■ t]:P say that if there is a reason for P, then there is a reason for P, but they give us different reasons.
One of the first things everybody shows axiomatically when studying modal logic is that
is provable in K, and thus is provable
in every axiom system for a normal modal logic. But the argument from left to right is quite different from the argument from right to left. Because justification theorems contain traces of their proofs, we should not expect a single justification analog of this modal equivalence, but rather separate results for the left-right implication and for the right-left implication.
Example 2.10 Here is a justification derivation corresponding to the usual
Our final example illustrates the use of +, which has not come up so far. It is for handling situations where there is more than one explanation needed for something, as in a proof by cases. At first glance this seems rather minor, but + turns out to play a vital role when we come to realization results.
Example 2.12 (?X V ?F) → ?(X V F) is a theorem of K with an elementary proof that we omit. Let us construct a counterpart in JL(CS), still assuming that CS is axiomatically appropriate and all tautologies are axioms.
The consequents of 4 and 8 both provide reasons for X V Y, but the reasons are different. We have used + to combine them, getting a justification analog of (?X V ?Y) → ?(X V Y).
2.5