Beginning Justification Logics

Justification logics, syntactically, are like modal logics except that justification terms take the place of ?. Justification terms are intended to represent reasons or justifications for formulas.

Definition 2.1 (Justification Term) The set Tm of justification terms is built up as follows.

(1) There is a set of justification variables, x, y,..., x₁, y₁,.... Everyjustifi- cation variable is a justification term.

(2) There is a set of justification constants, a, b,..., a₁, b₁,.... Every justi­fication constant is a justification term.

(3) There are binary operation symbols, + and ■.If u and v are justification terms, so are (u + v) and (u ■ v).

(4) There may be additional function symbols, f, g,..., f₁, g₁,..., of various arities. Which ones are present depends on the logic in question. If f is an n- placejustification function symbol of the logic, and t₁,..., t_n are justification terms, f(t₁,..., t_n) is a justification term.

Neither + nor ■ is assumed to be commutative or associative, and there is no distributive law. We do, however, allow ourselves the notational convenience of omitting parentheses with multiple occurrences of ■, assuming associativity to the left. Thus, for instance, a ■ b ■ c ■ d is short for (((a ■ b) ■ c) ■ d). We make the same assumption concerning +, though it actually plays a much lesser role. Also we will generally assume that ■ binds more strongly than +, writing a∙b+c instead of (a ■ b) + c for instance.

Definition 2.2 (Justification Formula) The set of justification formulas, Fm, is built in the usual recursive way, as follows.

(1) There is a set Var of propositional variables, P, Q,..., P₁, Q₁,... (these are also known as propositional letters). Every propositional variable is a justification formula.

(2) ? (falsehood) is a justification formula.

(3) If X and Y are justification formulas, so is (X → Y).

(4) If t is a justification term and X is a justification formula, then t:X is a justification formula.

We will sometimes use other propositional connectives,which we

can think of as defined connectives, or primitive as convenient. Outer parenthe­ses may be omitted in formulas if no confusion will result. If justification term t has a complex structure we generally will write [t]:X, using square brackets as a visual aid. Square brackets have no theoretical significance.

In a modal formula, ? is supposed to express that something is necessary, or known, or obligatory, or some such thing, but it does not say why. A justifi­cation term encodes this missing information; it provides the why absent from modal formulas. This is what their structure is for. Justification variables stand for arbitrary justification terms, and substitution for them is examined begin­ning with Definition 2.17. Justification constants stand for reasons that are not further analyzed—typically they are reasons for axioms. Their role is discussed in more detail once constant specifications are introduced, in Definition 10.32. The ■ operation corresponds to modus ponens. If X → Y is so for reason s and X is so for reason t, then Y is so for reason s ■ t. (Reasons are not unique—Y may be true for other reasons too.) The + operation is a kind of weakening. If X is so for either reason s or reason t, then s + t is also a reason for X. Other operations on justification terms, if present, correspond to features peculiar to particular modal logics and will be discussed as they come up.

2.3