Fundamental Properties of Justification Logics
All justification logics have certain common and useful properties. Some features are identical with those of classical logic; others have twists that are special to justification logics.
This section is devoted to ones we will use over and over. Throughout this section let JL be a justification logic and CS be a constant Specificationfor it.
property if t contains no justification variables and no justification operation or function symbols except ∙. That is, t is built up from justification constants using only ∙. Theorem 2.14 If CS is an axiomatically appropriate constant specification for JL then JL has the strong internalization property relative to CS.
If X is provable using an axiomatically appropriate constant specification so is t:X, and the term t constructed in the preceding proof actually internalizes the steps of the axiomatic proof of X, hence the name internalization. Of course different proofs of X will produce different justification terms. Here is an extremely simple example, but one that is already sufficient to illustrate this point. Example 2.15 Assume JL is a justification logic, CS is an axiomatically appropriate constant specification for it, and all tautologies are axioms of JL.
The problem of finding a “simplest” justification term is related to the problem of finding the “simplest” proof of a provable formula. It is not entirely clear what this actually means.
Corollary 2.16 (Lifting Lemma) Suppose JL is a justification logic that has the internalization property relative to CS (in particular, if CS is axiomatically
Next we move on to the role Ofjustification variables.
We said earlier, rather informally, that variables stood for arbitrary justification terms. In order to make this somewhat more precise, we need to introduce substitution.Definition 2.17 (Substitution) A substitution is a function σ mapping some set of justification variables to justification terms, with no variable in the domain of cannot be wrong. Nonetheless, if the justification is a mathematical proof, factivity is something mathematicians are generally convinced of. If we think of knowledge as justified, true belief, factivity is built in. Philosophers generally understand justified, true belief to be inherent in knowledge, but not sufficient, see Gettier (1963).
The modal axiom scheme ?X → X is called T. The weakest normal modal logic including all instances of this scheme is KT, sometimes abbreviated simply as T. We use JT for J plus Factivity and, as noted earlier, we use JT(CS) when a specific constant specification is needed. Note that the languages of JT and J are the same. There is one more such example, after which additional operation symbols must be brought in.
Consistency is an important special case of Factivity. Modally it can be represented in several ways. One can assume the axiom scheme
In
JD is J plus Consistency. Note that JT extends JD.
Positive Introspection is a common assumption about an agent’s knowledge: If an agent knows something, the agent knows that it is known; an agent can introspect about the knowledge he or she possesses. In logics of knowledge it is formulated as KX → KKX. If one understands ? as representing provability in formal arithmetic, it is possible to prove that a proof is correct: ?X → ??X. To formulate a justification logic counterpart, Artemov introduced a one-place function symbol on justification terms, denoted ! and written in prefix position.
The intuitive idea is that if t is a justification of something, !t is a justification that t is, indeed, such a justification. Note that the basic language of justification logics has been extended, and this must be reflected in any constant specifications being considered.Positive Introspection t:X → !t:t:X
As part of the intuition behind the program to create an arithmetic semantics for intuitionistic logic, justification terms were thought of as representing particular formal proofs. In this context justification terms were called proof terms, and ! was called Proof Checker. Later, when the idea of justification logics had broadened, ! was called Fact Checker. Typical everyday examples of Fact Checker applications are a referee report certifying that a proof in a paper is correct, or a computer output showing a verification that a formal proof is correct.
If Positive Introspection is among the axioms of a justification logic, constant specifications can be considerably simplified. For example, if CS is ax- iomatically appropriate and A is an axiom, we have been requiring that there be some constant symbol a with a:A 2 CS, and also some constant symbol b with b:a:A 2 CS, and also some constant symbol c with c:b:a:A 2 CS, and so on. But with Positive Introspection we really only need the first of these: there is some a with a:A 2 CS. We don't need to postulate the existence of b because we have that a:A → !a:a:A, and so we can use !a where we would have used b. Similarly we can use !(!a) where we would have used c. And so on. The formulation and proof of Theorem 2.14 need some obvious modification, but it is easy. In fact, the first justification logic LP had just such a formulation. The simplification is nice, but is not a deep issue.
The addition of ?X → ??X to K is known as K4. We use J4 for the justification counterpart, similar to what we did with JD and KD earlier.
LP is a justification logic that has been mentioned many times so far.
We are finally in a position to say what it is. Axiomatically it is JT4, that is, J plus Factivity (and hence Consistency) plus Positive Introspection (and so with ! added to the language). For historical reasons instead of JT4 the name LP is commonly used standing, as we have already noted, for logic of proofs. It is a counterpart of the modal logic S4, sometimes known as KT4.In Examples 2.10-2.12 we gave some instances of modal theorems and justification counterparts. Here is one more such example. This time the modal logic is S4, and the justification logic is LP(CS) where CS is an axiomatically appropriate constant specification. The example is taken from Artemov (2001), and like Example 2.12 it illustrates the uses of the + operator, as well as !.
Example 2.21 We begin by deriving (?X V ?F) → ?(?X V ?F) in S4. Then we carry out a similar derivation in LP(CS) of a formula that, in a sense, embodies the modal argument. Here is the S4 derivation.
And now the corresponding derivation in LP(CS). In 2 it is assumed that a and b are constants that are assigned to the axioms shown in 1 by the constant
specification we are using for LP. Also x and ó are justification variables.
Informally this says that, in LP, if we have a justification of one or X or Y, then we have a justification of that fact.
2.7