A Handful of Less Common Justification Logics
In Section 2.6 we looked at the oldest and most familiar of the justification logics. Because those early justification logics are sublogics of LP, and that is interpretable in formal arithmetic, all justification logics considered in that section are also interpretable in arithmetic.
The possibility of direct arithmetic interpretability disappears as the family of justification logics grows. In this section we take a look at a broader and less familiar group of logics. For each we begin with a modal logic, then introduce a justification counterpart. Fitting Semantics for these will be discussed in Chapter 4. In Section 4.3 specific models will be presented and soundness shown. In Section 4.5 completeness will be proved. Several interesting issues are illustrated by our particular logics, and these issues will be discussed at appropriate points.2.7.1 K43 and J43
Modal logic K43 is one of a family, K4n, from Chellas (1980). K43 extends K with the schema ?X → ???X. (The familiar K4 is K42 and is in this family.) There is more than one way of constructing a justification counterpart for K43, something that is also true of K4 itself. This is a point that will be discussed later. Here we adopt the following justification version. Let ! and !! be one- place function symbols. (Please note that we are using !! as a single symbol, and not as an iteration of !.) Ourjustification counterpart for K43 results from adding to J the following axiom schema
We call this justification logic J43.
Unlike with K4 and K43, this does not say that J4 extends J43.
What it does say is that J43 translates into, or embeds into, J4 by replacing !!r by !(!r).2.7.2 S5 and JT45
S5 is perhaps the most common modal logic used in applications. One standard axiomatization is to add the scheme of negative introspection to S4: 
Written epistemically we have
It is the
strong assumption that if you don't know something, you know you don't know it. Despite its strength, it is commonly assumed in epistemic logic, perhaps because it has the effect of simplifying the corresponding possible world semantics.
A justification counterpart for S5, now called JT45, was introduced independently in Pacuit (2005, 2006) and Rubtsova (2006b). A one-place function symbol ?, whose role is analogous to that of!, is added to the LP language, and like !, it is written in prefix position. Thejustification axiom scheme added to LP is the following.
We will see that the semantics created for JT45 played an important role in understanding the behavior of the evidence function, which will be introduced in Chapter 4. We also note that while the behavior of “?” doesn't allow for a direct arithmetic interpretation, in Artemov et al. (1999) an alternative formulation of modal S5 was used to produce a different explicit counterpart, in which “?” was emulated by other means, and which does have an arithmetical provability interpretation.
2.7.3 Sahlqvist Examples
Sahlqvist formulas are important in modal logic, but we do not discuss their general significance here; an excellent treatment can be found in Blackburn et al. (2001). In example 3.5.5, section 3.6 of that book a few simple instances are discussed. We begin with the first of these examples.
2.7.4 S4.2 and JT4.2
The modal logic S4.2 is from Geach (1973).
It is the paradigm example of a broader class of logics that we will examine in detail in Chapter 8. Axiomati-
We call this justification logic JT4.2.
Although we primarily have a formal interest here, a few motivating words
2.7.5 KX4 and JX4
For a justification counterpart we start with LP again. We drop the Factivity axiom scheme, t:X → X. To replace it we introduce a binary function symbol c, which we write in infix position, and we add the following scheme.
We call the resulting justification logic JX4. This logic has interesting features, which are explored in Fitting (2017).