Keywords

1 Introduction

Justification logic replaces the \(\Box \)-operator from modal logic with explicit evidence terms [5, 11, 30]. That is, instead of formulas \(\Box A\), justification logic features formulas t : A, where t encodes evidence for A. Depending on the context, the term t may represent a formal proof of A [5, 29] or stand for an informal justification (like direct observation, public announcement, private communication, and so on) for an agent’s knowledge or belief of A. With the introduction of possible world models, justification logic has become an important tool to discuss and analyze epistemic situations [6, 7, 14, 15, 36].

The terms of justification logic represent explicit evidence for an agent’s belief or knowledge. Within justification logic, we can reason about this evidence. For instance, we can track different pieces of evidence pertaining to the same fact, which is essential for distinguishing between factive and non-factive justifications. This is applied nicely in Artemov’s analysis of Russel’s Prime Minister example [8]. Evidence terms can also represent the reasoning process of an agent. Therefore, agents represented by justification logic systems are not logically omniscient according to certain complexity based logical omniscience tests [12,13,14].

In traditional justification logic, terms are built using the binary operations \(+\) (called sum) and \(\cdot \) (called application) and maybe other additional operations. Thus terms have the syntactic form of polynomials and are, in the context of the Logic of Proofs, indeed called proof polynomials.

This syntactic structure of polynomials is essentially used in the proof of realization, which provides a procedure that, given a theorem of a modal logic, constructs a theorem of the corresponding justification logic by replacing each occurrence of \(\Box \) with an adequate justification term [5].

The main contribution of the present paper is to look at the syntactic structure of justification terms algebraically, that is, we interpret justifications by a semiring structure. The motivation for this is threefold:

  1. 1.

    It provides an appropriate semantics for variables in evidence terms. It was always the idea in justification logic that terms with variables justify derivations from assumptions. The variables represent the input values, i.e., (arbitrary) proofs of the assumptions [5]. But this was not properly reflected in the semantics where usually variables are treated like constants: to each term (no matter whether it contains variables or not) some set of formulas is assigned. In our semiring semantics, ground terms (i.e. terms not containing variables) are interpreted as elements of a semiring and terms with variables are interpreted as polynomial functions on the given semiring of justifications. Thus terms with variables are adequately represented and the role of variables is clarified.

  2. 2.

    The algebraic structure of terms makes it possible to compute with justifications. Depending on the choice of the semiring, we can use the term structure to model levels of trust (Viterbi semiring), costs of obtaining knowledge (tropical semiring), probabilistic evidence (powerset semiring), fuzzy justifications (Łukasiewicz semiring), and so on.

  3. 3.

    Considering \(\omega \)-continuous semirings, i.e. semirings in which certain fixed points exist, may provide a solution to the problem of realizing modal fixed point logics like the logic of common knowledge. In these logics, some modal operators can be interpreted as fixed points of monotone operations. It seems likely that their realizations also should be fixed points of certain operations on semirings.

1.1 Related Work

Our approach is heavily inspired by the semiring approach for provenance in database systems [25]. There the idea is to label database tuples and to propagate expressions in order to annotate intermediate data and final outputs. One can then evaluate the provenance expressions in various semirings to obtain information about levels of trust, data prices, required clearance levels, confidence scores, probability distributions, update propagation, and many more [26].

This semiring framework has been adapted to many different query languages and data models. The core theoretical work of those approaches includes results on query containment, the construction of semirings, and fixed points [3, 4, 19,20,21, 23, 24].

There are only few systems available where justification terms are equipped with additional structure. Two prominent examples are based on \(\lambda \)-terms (in contrast to the combinatory terms of the Logic of Proofs). The reflective lambda calculus [2] includes reduction rules on proof terms. The intensional lambda calculus [10] has axioms for evidence equality and also features a reduction relation on the terms.

2 The Syntax of \(\mathsf {SE}\)

We begin by defining the justification language as usual except that we limit the number of variables by some arbitrary but fixed number n. That is, we use a countable set of constants \(\mathsf {JConst}= \{0,1,c_1,c_2,...\}\) that includes two distinguished elements 0 and 1. Further we have a finite set of variables \(\mathsf {JVar}= \{x_1,...,x_n\}\).

Definition 1 (Justification Term)

Justification terms are

$$ c \in \mathsf {JConst},\ x \in \mathsf {JVar},\ s \cdot t,\ \textit{ and }\ s+t, $$

where s and t are justification terms. The set of all justification terms is called \(\mathsf {Tm}\). A justification term that does not contain variables is called ground term. \(\mathsf {GTm}\) denotes the set of all ground terms.

Often we write only term for justification term. Further, we need a countable set of atomic propositions \(\mathsf {Prop}= \{P_1,P_2,...\}\).

Definition 2 (Formulas)

Formulas are \(\perp \), P, \(A \rightarrow B\) and t : A, where t is a justification term, \(P \in \mathsf {Prop}\) and A, B are formulas. The set of all formulas is called \(\mathsf {Fml}\).

The remaining logical connectives \(\lnot \), \(\wedge \), \(\vee \), and \(\leftrightarrow \) are abbreviations as usual, e.g., \(\lnot A\) stands for \(A \rightarrow \bot \).

Now we can define a deductive system for the logic \(\mathsf {SE}\) about the semirings of evidence. It consists of the following axioms:

figure a

The rules of \(\mathsf {SE}\) are:

$$ {\mathbf {MP}} \quad \dfrac{A \qquad A \rightarrow B}{B} $$

and

$$ {\mathbf {jv}} \quad \dfrac{A(x)}{A(t)} $$

where x is a variable, t is a term, and A(t) denotes the result of substituting t for x in A(x).

The axiom schemes a+, c+, 0+, am, a0, a1, dl and dr are called semiring axioms. In the axiom scheme j+, we find an important difference to traditional justification logic where \(\vee \) is used instead of \(\wedge \), see also Sect. 4 later. The idea for \(\mathbf{j}+ \) is to read \(s+t:A\) as both s and t justify A. This is useful, e.g., in the context of uncertain justifications where having two justifications is better than just having one. The rule jv shows the role of variables in \(\mathsf {SE}\), which differs from traditional justification logic. In our approach a formula A(x) being valid means that A(x) is valid for all justifications x.

Let us mention two immediate consequences of our axioms. First a version of axiom 0+ with \(x+0\) is replaced by \(0+x\) is provable. Second, the direction from right to left in axiom a+ is also provable.

Lemma 1

The following formulas are derivable in \(\mathsf {SE}\):

$$ 0+x:A \leftrightarrow x:A \qquad \textit{and}\qquad x+(y+z):A \leftrightarrow (x+y)+z:A. $$

A theory is just any set of formulas.

Definition 3 (Theory)

A theory T is a subset of \(\mathsf {Fml}\). We use \(T \vdash _{\mathsf {SE}} F\) to express that F is derivable from T in \(\mathsf {SE}\).

Often we drop the subscript \(_{\mathsf {SE}}\) in \(\vdash _{\mathsf {SE}}\) when it is clear from the context. Moreover, we use \(\vdash _{\mathsf {CL}}\) for the derivability relation in classical propositional logic.

A theory can compensate for the absence of constant specifications. Usually, systems of justification logic are parametrized by a constant specification, i.e., a set containing pairs of constants and axioms. One then has a rule saying that a formula c : A is derivable if (c, A) is an element of the constant specification. Here we do not adopt this approach but simply use a theory that includes c : A.

Theorem 1 (Conservativity)

The logic \(\mathsf {SE}\) is a conservative extension of the classical propositional logic \(\mathsf {CL}\), i.e., for all formulas A of the language of \(\mathsf {CL}\), we have

$$ \vdash _{\mathsf {SE}} A \quad \textit{iff}\quad \vdash _{\mathsf {CL}} A. $$

Proof

The claim from right to left is trivial as \(\mathsf {SE}\) extends \(\mathsf {CL}\). For the direction from left to right, we consider a mapping \(^\circ \) from \(\mathsf {Fml}\) to formulas of \(\mathsf {CL}\) that simply drops all occurrences of t : . In particular, for any \(\mathsf {CL}\)-formula A, we have \(A^\circ = A\). Now it is easy to prove by induction on the length of \(\mathsf {SE}\) derivations that for all \(A \in \mathsf {Fml}\),

$$ \vdash _{\mathsf {SE}} A \quad \text {implies}\quad \vdash _{\mathsf {CL}} A^\circ . $$

Simply observe that for any axiom A of \(\mathsf {SE}\), \(A^\circ \) is a propositional tautology, and that the rules of \(\mathsf {SE}\) respect the \(^\circ \)-translation.    \(\square \)

Now consistency of \(\mathsf {SE}\) follows immediately.

Corollary 1

(Consistency of \(\mathsf {SE}\)). The logic \(\mathsf {SE}\) is consistent.

Proof

Assume towards contradiction that \(\vdash _{\mathsf {SE}} \perp \). It follows \(\vdash _{\mathsf {CL}} \perp \) by conservativity of \(\mathsf {SE}\) over \(\mathsf {CL}\), which is a contradiction.    \(\square \)

3 The Semantics of \(\mathsf {SE}\)

Our semantics of \(\mathsf {SE}\) is similar to traditional semantics for justification logic in the sense that t : A is given meaning by simply making use of an evidence relation that assigns a set of formulas to each evidence term. The novelty of our approach is the requirement that the interpretation of the terms forms a semiring.

Definition 4 (Semiring)

\(K = (S, +, \cdot , 0, 1)\), where S is the domain, is a semiring, if for all \(a,b,c \in S\):

  1. 1.

    \((a+b)+c = a+(b+c)\),    \(a+b=b+a\)    and    \(a+0=0+a=a\)

  2. 2.

    \((a\cdot b)\cdot c = a\cdot (b\cdot c)\)    and    \(a\cdot 1 = 1\cdot a = a\)

  3. 3.

    \((a+b)\cdot c = a\cdot c + b\cdot c\)    and    \(c\cdot (a+b) = c\cdot a + c\cdot b\)

  4. 4.

    \(a \cdot 0 = 0 \cdot a = 0\)

Thus, unlike in a ring, there is no inverse to \(+\). We also do not require \(\cdot \) to be commutative.

Note that we use \(+\) and \(\cdot \) both as symbols in our language of justification logic and as operations in the semiring. It will always be clear from the context which of the two is meant.

For the following, assume we are given a semiring \(K = (S, +, \cdot , 0, 1)\). We use a function \(I: \mathsf {JConst}\rightarrow S\) to map the constants of the language of \(\mathsf {SE}\) to the domain S of the semiring. We call this function I an interpretation if \(I(0)=0\) and \(I(1)=1\). We now extend I to a homomorphism such that \(I: \mathsf {Tm}\rightarrow S[\mathsf {JVar}]\), where \(S[\mathsf {JVar}]\) is the polynomial semiring in \(\mathsf {JVar}\) over S by setting:

  1. 1.

    \(I(x):=x\) for variables x

  2. 2.

    \(I(s+t) := I(s)+I(t)\) for terms s, t

  3. 3.

    \(I(s\cdot t) := I(s) \cdot I(t)\) for terms s, t

Let \(K = (S, +, \cdot , 0, 1)\) be a semiring with domain S. We define \(\mathsf {Fml_S}\) as the set of formulas where we use elements of S instead of justification terms.

  1. 1.

    \(\perp \in \mathsf {Fml_S}\)

  2. 2.

    \(P \in \mathsf {Fml_S}\), where \(P \in \mathsf {Prop}\)

  3. 3.

    \(A \rightarrow B \in \mathsf {Fml_S}\), where \(A \in \mathsf {Fml_S}\) and \(B \in \mathsf {Fml_S}\)

  4. 4.

    \(s:A \in \mathsf {Fml_S}\), where \(A \in \mathsf {Fml_S}\) and \(s \in S\)

Definition 5 (Evidence relation)

Let S be the domain of a semiring. We call \(J \subseteq S \times \mathsf {Fml_S}\) an evidence relation if for all \(s,t \in S\) and all \(A,B \in \mathsf {Fml_S}\):

  1. 1.

    \(J(s, A \rightarrow B)\) and J(t, A) imply \(J(s\cdot t,B)\)

  2. 2.

    J(s, A) and J(t, A) imply \(J(s+t,A)\)

Definition 6 (Valuation)

A valuation v is a function from \(\mathsf {JVar}\) to S.

The polynomial I(t) can be viewed as a function \(t_I: S^n \rightarrow S\). Hence, given an interpretation \(I: \mathsf {JConst}\rightarrow S\) and a valuation v, every \(t \in \mathsf {Tm}\) can be mapped to an element \(t_I(v(x_1),...,v(x_n))\) in S, which we denote by \(t_I^v\). By abuse of notation, we only mention the variables that occur in the term t. For a variable x we have

$$ v(x) = x_I(v(x)) = x_I^v. $$

Given the definition of the polynomial function \(t_I\), we find, e.g.,

$$\begin{aligned} x_I^v \cdot y_I^v = x_I(v(x)) \cdot y_ I(v(y)) = (x \cdot y)_I (v(x) , v(y)) = (x \cdot y)_I^v. \end{aligned}$$
(1)

For \(A \in \mathsf {Fml}\) we define \(A_I^v \in \mathsf {Fml_S}\) inductively:

  1. 1.

    \(\perp _I^v := \perp \)

  2. 2.

    \(P_I^v := P\), where \(P \in \mathsf {Prop}\)

  3. 3.

    \((A \rightarrow B)_I^v := A_I^v \rightarrow B_I^v\), where \(A \in \mathsf {Fml}\) and \(B \in \mathsf {Fml}\)

  4. 4.

    \((s:A)_I^v := s_I^v : A_I^v\), where \(A \in \mathsf {Fml}\) and \(s \in \mathsf {Tm}\)

Let \(A(x_1,\ldots ,x_n) \in \mathsf {Fml}\). Then \(A_I\) denotes the function \(A_I : S^n \rightarrow \mathsf {Fml_S}\) with \(A_I(y_1,...,y_n)=A_I^v\) where v is such that \(v(x_i)=y_i\).

Definition 7 (Semiring model)

A semiring model is a tuple \(M = (K, *, I, J)\) where

  1. 1.

    \(K= (S, +, \cdot , 0, 1)\) is a semiring

  2. 2.

    \(*\) is a truth assignment for atomic propositions, i.e., \(*: \mathsf {Prop}\rightarrow \{\mathbb {F},\mathbb {T}\}\)

  3. 3.

    I is an interpretation, i.e., \(I: \mathsf {JConst}\rightarrow S\)

  4. 4.

    J is an evidence relation.

First we define truth in a semiring model for a given valuation. Because variables represent arbitrary justifications, we require a formula to be true for all valuations in order to be true in a semiring model. This means a formula with variables is interpreted as universally quantified.

Definition 8 (Truth in a semiring model)

Let \(M= (K, *, I, J)\) be a semiring model, v a valuation and A a formula. \(M, v \Vdash A\) is defined as follows:

  • \(M, v \nVdash \perp \)

  • \(M, v \Vdash P\)    iff \(\quad P^*=\mathbb {T}\)

  • \(M, v \Vdash A \rightarrow B\)    iff    \(M,v \nVdash A\) or \(M,v \Vdash B\)

  • \(M, v \Vdash s:A\)    iff    \(J(s_I^v,A_I^v)\)

Further we set \(M \Vdash A\)    iff    \(M, v \Vdash A\) for all valuations v.

For a semiring model M and a theory T, \(M \Vdash T\) means \(M \Vdash A\) for all \(A \in T\).

Definition 9 (Truth in a theory)

A theory T entails a formula F, in symbols \(T \Vdash F\), if for each semiring model M we have that \(M \Vdash T\) implies \(M \Vdash F\).

By unfolding the definitions, we immediately get the following lemma, which is useful to establish soundness of \(\mathsf {SE}\).

Lemma 2

Let \(M=(K,*,I,J)\) be a semiring model and let v and w be valuations with \(v(x_i)=(t_i)_I^w\) for variables \(x_i\) and terms \(t_i\). Then

$$ M,v \Vdash A(x_1,...,x_n) \quad \textit{iff}\quad M,w \Vdash A(t_1,...,t_n). $$

Proof

By induction on the structure of A.

  • Case \(A=\perp \). We have \(M,v \nVdash \perp \) and \(M,w \nVdash \perp \).

  • Case \(A=P\). We have \(M,v \Vdash P \Leftrightarrow P^*=1 \Leftrightarrow M,w \Vdash P\).

  • Case \(A=B \rightarrow C\). We have \(M,v \Vdash (B \rightarrow C)(x_1,...,x_n)\)

    \(\Leftrightarrow M,v \Vdash B(x_1,...,x_n) \rightarrow C(x_1,...,x_n)\)

    \(\Leftrightarrow M,v \nVdash B(x_1,...,x_n)\) or \(M,v \Vdash C(x_1,...,x_n)\)

    \({\mathop {\Leftrightarrow }\limits ^{\text {I.H.}}} M,w \nVdash B(t_1,...,t_n)\) or \(M,w \Vdash C(t_1,...,t_n)\)

    \(\Leftrightarrow M,w \Vdash B(t_1,...,t_n) \rightarrow C(t_1,...,t_n) \Leftrightarrow M,w \Vdash (B \rightarrow C)(t_1,...,t_n)\).

  • Case \(A=s:B\). We have \(M,v \Vdash (s:B)(x_1,...,x_n)\)

    \(\Leftrightarrow M,v \Vdash s(x_1,...,x_n):B(x_1,...,x_n) \)

    \(\Leftrightarrow J(s(x_1,...,x_n)_I^v, B(x_1,...,x_n)_I^v) \)

    \(\Leftrightarrow J(s_I(v(x_1),...,v(x_n)), B_I(v(x_1),...,v(x_n))) \)

    \(\Leftrightarrow J(s_I((t_1)_I^w,...,(t_n)_I^w), B_I((t_1)_I^w,...,(t_n)_I^w))\)

    \(\Leftrightarrow J(s(t_1,...,t_n)_I^w, B(t_1,...,t_n)_I^w) \Leftrightarrow M,w \Vdash s(t_1,...,t_n):B(t_1,...,t_n)\)

    \(\Leftrightarrow M,w \Vdash (s:B)(t_1,...,t_n)\).    \(\square \)

Theorem 2 (Soundness)

Let T be an arbitrary theory. Then:

$$ T \vdash F \quad \textit{implies}\quad T \Vdash F. $$

Proof

As usual by induction on the length of the derivation of F. Let \(M=(K,*,I,J)\) be a semiring model such that \(M \Vdash T\). To establish our claim when F is an axiom or an element of T, we let v be an arbitrary valuation and show \(M,v \Vdash F\) for the following cases:

  1. 1.

    \(F \in T\). Trivial.

  2. 2.

    CL. Trivial.

  3. 3.

    j. Assume \(M,v \Vdash x:(A \rightarrow B)\) and \(M,v \Vdash y:A\). That is \(J(x_I^v, (A \rightarrow B)_I^v)\) and \(J(y_I^v, A_I^v)\) hold, which by Definition 5 implies \(J(x_I^v \cdot y_I^v, B_I^v)\). Hence by (1) we get \(J((x \cdot y)_I^v, B_I^v)\), which yields \( M,v \Vdash x \cdot y:B\).

  4. 4.

    j+. Similar to the previous case.

  5. 5.

    a+. Assume \(M,v \Vdash (x+y)+z:A\). That is \(J(((x+y)+z)_I^v, A_I^v)\). Because of

    $$ ((x+y)+z)_I^v = (v(x) + v(y)) + v(z) = v(x) + (v(y) + v(z)) = (x+(y+z))_I^v, $$

    we get \(J((x+(y+z))_I^v, A_I^v)\), which yields \(M,v \Vdash x+(y+z):A\).

  6. 6.

    The remaining axioms are treated similarly to the previous case.

The case when F has been derived by MP follows by I.H. as usual. For the case when \(F = A(t)\) has been derived from A(x) by jv, we find by I.H. that \(M \Vdash A(x)\), which is

$$\begin{aligned} M,v \Vdash A(x) \text { for all valuations }v. \end{aligned}$$
(2)

Given the term t and an arbitrary valuation w, we find that there exists a valuation v such that \(t_I^w=v(x)\). By Lemma 2 we get

$$ M,v \Vdash A(x) \quad \text {iff} \quad M,w \Vdash A(t). $$

Thus using (2), we obtain \(M,w \Vdash A(t)\). Since w was arbitrary, we conclude \(M \Vdash A(t)\).    \(\square \)

For the completeness proof, we consider the free semiring over \(\mathsf {JConst}\cup \mathsf {JVar}\). We have for \(s,t \in \mathsf {Tm}\):

  • [t] is the equivalence class of t with respect to the semiring equalities, see Definition 4;

  • \([s]+[t]:=[s+t]\);

  • \([s]\cdot [t] := [s\cdot t]\);

  • \(S_{\mathsf {Tm}} := \{[t]: t \in \mathsf {Tm}\}\);

  • \(K_{\mathsf {Tm}} := (S_{\mathsf {Tm}}, +, \cdot , [0], [1])\) is the free semiring over \(\mathsf {JConst}\cup \mathsf {JVar}\).

The following lemma states that our truth definition respects the semiring equalities.

Lemma 3

Let T be a theory and s, t be ground terms with \([s]=[t]\). For each formula A we have

$$ T \vdash _{\mathsf {SE}} s:A \quad \textit{iff}\quad T \vdash _{\mathsf {SE}} t:A. $$

Lemma 4

Assume that we are given an interpretation \(I: \mathsf {JConst}\rightarrow S_\mathsf {Tm}\) with \(I(c) = [c]\), a term \(s(x_1,...,x_n)\), and a valuation \(v: \mathsf {JVar}\rightarrow S_\mathsf {Tm}\) with \(v(x_i) =[t_i]\). Then we have

$$ s(x_1,...,x_n)_I^v = [s(t_1,...,t_n)]. $$

Proof

Induction on the structure of s:

  • \(c_I^v = [c]\) by definition of I.

  • \((x_i)_I^v = [t_i]\) by definition of v.

  • \((s_1+s_2)_I^v = (s_1)_I^v+(s_2)_I^v\). By I.H. we have

    $$ (s_1)_I^v = [s_1(t_1,...,t_n)] \quad \text {and}\quad (s_2)_I^v = [s_2(t_1,...,t_n)]. $$

    Thus \( (s_1)_I^v+(s_2)_I^v = [s_1(t_1,...,t_n)]+[s_2(t_1,...,t_n)] = [(s_1+s_2)(t_1,...,t_n)]\).

  • \((s_1 \cdot s_2)_I^v = (s_1)_I^v \cdot (s_2)_I^v\). By I.H. we have

    $$ (s_1)_I^v = [s_1(t_1,...,t_n)] \quad \text {and}\quad (s_2)_I^v = [s_2(t_1,...,t_n)]. $$

    Thus \((s_1)_I^v \cdot (s_2)_I^v = [s_1(t_1,...,t_n)] \cdot [s_2(t_1,...,t_n)] = [(s_1 \cdot s_2)(t_1,...,t_n)]\)    \(\square \)

We extend the notion of equivalence to formulas by defining the function

$$ [\cdot ]: \mathsf {Fml}\rightarrow \mathsf {Fml}_{S_\mathsf {Tm}}$$

as follows:

  • \([\perp ] := \perp \)

  • \([P] := P\)

  • \([A \rightarrow B] := [A] \rightarrow [B]\)

  • \([t:A] := [t]:[A]\)

Intuitively [A] is the formula where each justification term is replaced by its equivalence class in the free semiring. Observe that if \(I(c)=[c]\) and \(v(x)=[x]\), then \([A]=A_I^v\). Now we extend Lemma 4 to formulas.

Lemma 5

Assume that we are given the interpretation \(I: \mathsf {JConst}\rightarrow S_\mathsf {Tm}\) with \(I(c) = [c]\), a formula \(A(x_1,...,x_n)\), and a valuation \(v: \mathsf {JVar}\rightarrow S_\mathsf {Tm}\) with \(v(x_i) =[t_i]\). Then we have

$$ A(x_1,...,x_n)_I^v = [A(t_1,...,t_n)]. $$

Proof

Induction on the structure of A:

  • \(\perp _I^v = \perp = [\perp ]\)

  • \(P_I^v = P = [P]\)

  • \((A \rightarrow B)(x_1,...,x_n)_I^v = A(x_1,...,x_n)_I^v \rightarrow B(x_1,...,x_n)_I^v\)

    \({{\mathop {=}\limits ^{\text {I.H.}}} [A(t_1,...,t_n)] \rightarrow [B(t_1,...,t_n)] = [(A \rightarrow B)(t_1,...,t_n)]}\)

  • \((s:A)(x_1,...,x_n)_I^v = s(x_1,...,x_n)_I^v:A(x_1,...,x_n)_I^v\)

    \({{\mathop {=}\limits ^{\text {I.H. and L. 4}}} [s(t_1,...,t_n)]:[A(t_1,...,t_n)] = [(s:A)(t_1,...,t_n)]}\)    \(\square \)

Let \(\mathsf {Prop}2\) be an infinite set of atomic propositions with \(\mathsf {Prop}\cap \mathsf {Prop}2 = \emptyset \). Then there exists an bijective function \(f: S_{\mathsf {Tm}} \times \mathsf {Fml}_{S_\mathsf {Tm}}\rightarrow \mathsf {Prop}2\). We assume f to be fixed for the rest of this section. Based on this function we define a translation \('\) that maps formulas of \(\mathsf {Fml}\) to pure propositional formulas containing atomic propositions from \(\mathsf {Prop}\cup \mathsf {Prop}2\).

  1. 1.

    \(\perp ' := \perp \)

  2. 2.

    \(P' := P\)

  3. 3.

    \((A \rightarrow B)' := A' \rightarrow B'\)

  4. 4.

    \((t:A)' := f([t],[A])\)

Let T be a theory. We define first \(N := \{A' \mid A \in T\) or A is an axiom of \(\mathsf {SE}\}\) and then the corresponding theory:

$$\begin{aligned} T' := \{A(t_1,...,t_n)' \mid A(x_1,...,x_n)' \in N, t_i \in \mathsf {Tm}\}. \end{aligned}$$

Suppose \(A(x_1,...,x_n)' \in T'\). Then there exist a formula \(B(x_1,...,x_n)' \in N\) and justification terms \(s_1,...,s_n\) such that \(B(s_1,...,s_n)' = A(x_1,...,x_n)'\). This implies \(B(s_1(t_1,...,t_n),...,s_n(t_1,...,t_n))' = A(t_1,...,t_n)'\). Now we have \(A(t_1,...,t_n)' \in T'\). Therefore the following implication is proved:

$$\begin{aligned} A(x)' \in T' \Rightarrow A(t)' \in T' \end{aligned}$$
(3)

In fact this does not only hold for formulas in \(T'\) but also for all formulas derived from \(T'\) by classical propositional logic.

Lemma 6

If \(T' \vdash _{\mathsf {CL}} A(x)'\) then \(T' \vdash _{\mathsf {CL}} A(t)'\).

Proof

Induction on the derivation of \(A(x)'\). Note that \(T'\) contains all the axioms of \(\mathsf {CL}\). So we can omit this case.

  1. 1.

    If \(A(x)' \in T'\) then \(A(t)' \in T'\) by the above observation and thus \(T' \vdash _{\mathsf {CL}} A(t)'\).

  2. 2.

    If \(A(x)'\) is obtained by MP from B and \(B \rightarrow A(x)'\) then B can be written as \(C(x)'\) because f is surjective. The induction hypothesis (\(T' \vdash _{\mathsf {CL}} C(t)'\) and \(T' \vdash _{\mathsf {CL}} C(t)' \rightarrow A(t)'\)) yields \(T' \vdash _{\mathsf {CL}} A(t)'\).    \(\square \)

Lemma 7

\(T \vdash _{\mathsf {SE}} A \Leftrightarrow T' \vdash _{\mathsf {CL}} A'\)

Proof

Left to right by induction on a derivation of A:

  1. 1.

    If \(A \in T\) or A is an axiom then \(A' \in T'\) and therefore \(T' \vdash _{\mathsf {CL}} A'\).

  2. 2.

    If A is obtained by MP from B and \(B \rightarrow A\) then the induction hypothesis (\(T' \vdash _{\mathsf {CL}} B'\) and \(T' \vdash _{\mathsf {CL}} B' \rightarrow A'\)) immediately yields \(T' \vdash _{\mathsf {CL}} A'\).

  3. 3.

    If A(t) is obtained by jv from A(x) then the induction hypothesis is \(T' \vdash _{\mathsf {CL}} A(x)'\). By the previous lemma we conclude \(T' \vdash _{\mathsf {CL}} A(t)'\).

Right to left by induction on a derivation of \(A'\):

  1. 1.

    If \(A(x_1,...,x_n)' \in T'\) then there exist a formula \(B(x_1,...,x_n)' \in N\) and justification terms \(s_1,...,s_n\) such that \(B(s_1,...,s_n)' = A(x_1,...,x_n)'\). Trivially we have \(T \vdash _{\mathsf {SE}} B(x_1,...,x_n)\) and get by jv that \(T \vdash _{\mathsf {SE}} B(s_1,...,s_n)\). Since f is injective, the only difference between \(A(x_1,...,x_n)\) and \(B(s_1,...,s_n)\) is that some terms may be replaced by equivalent ones (modulo the semiring). Therefore, we get \(T \vdash _{\mathsf {SE}} A(x_1,...,x_n)\) by using the semiring axioms of \(\mathsf {SE}\) and propositional reasoning.

  2. 2.

    If \(A'\) is a propositional tautology then so is A because f is injective, but some terms in A may be replaced by equivalent ones. We get \(T \vdash _{\mathsf {SE}} A\) again by using the semiring axioms and propositional reasoning.

  3. 3.

    If \(A'\) is obtained by MP from \(B \rightarrow A'\) and B then B can be written as \(C'\). The induction hypothesis (\(T \vdash _{\mathsf {SE}} C \rightarrow A\) and \(T \vdash _{\mathsf {SE}} C\)) implies \(T \vdash _{\mathsf {SE}} A\).

   \(\square \)

Lemma 7 gives us the ability to switch from \(\mathsf {SE}\) to \(\mathsf {CL}\) and vice versa. Therefore, we can use completeness of \(\mathsf {CL}\) to obtain completeness for \(\mathsf {SE}\).

Theorem 3 (Completeness)

Let T be an arbitrary theory. Then:

$$\begin{aligned} T \Vdash F \quad \text {implies}\quad T \vdash F. \end{aligned}$$

Proof

We will prove the contraposition, which means for \(T \nvdash F\) we will construct a semiring model M and find a valuation v, such that \(M \Vdash T\) and \(M,v \nVdash F\). Assume \(T \nvdash F\). By Lemma 7 we get \(T' \nvdash _\mathsf {CL}F'\). The completeness of \(\mathsf {CL}\) delivers \(*: \mathsf {Prop}\cup \mathsf {Prop}2 \rightarrow \{\mathbb {F},\mathbb {T}\}\), such that for the \(\mathsf {CL}\)-model \(M_*\) consisting of \(*\) we have \(M_* \Vdash T'\) and \(M_* \nVdash F'\). Now we can define the semiring model M:

  • \(M := (K_{\mathsf {Tm}}, *|_{\mathsf {Prop}}, I, J)\)

  • \(*|_{\mathsf {Prop}}\) is the restriction of \(*\) to \(\mathsf {Prop}\)

  • \(I: \mathsf {JConst}\rightarrow S_{\mathsf {Tm}}\), \(I(c) := [c]\)

  • \(J := \{([t], [A]) \mid M_* \Vdash f([t], [A])\}\)

In order to prove that M is a semiring model, we need to show that J is an evidence relation.

  1. 1.

    From \(M_* \Vdash T'\) we derive \(M_* \Vdash (s:(A \rightarrow B) \rightarrow (t:A \rightarrow s \cdot t:B))'\) \(\forall s,t \in \mathsf {Tm}\) and \(\forall A,B \in \mathsf {Fml}\) by using the definition of \(T'\) and (3). It follows

    $$\begin{aligned} M_* \Vdash f([s],[A \rightarrow B]) \rightarrow (f([t],[A]) \rightarrow f([s \cdot t],[B])). \end{aligned}$$

    By the truth definition in \(\mathsf {CL}\) we find

    $$\begin{aligned} \text {if } f([s],[A \rightarrow B])^* = \mathbb {T} \text { and } f([t],[A])^* = \mathbb {T} \text { then } f([s \cdot t],[B])^* = \mathbb {T}. \end{aligned}$$

    From the definition of J in M we get

    $$\begin{aligned} \text {if } J([s],[A] \rightarrow [B]) \text { and } J([t],[A]) \text { then } J([s] \cdot [t],[B]). \end{aligned}$$
  2. 2.

    From \(M_* \Vdash T'\) we derive \(M_* \Vdash (s:A \wedge t:A \rightarrow s+t:A)'\) \(\forall s,t \in \mathsf {Tm}\) and \(\forall A \in \mathsf {Fml}\) by using the definition of \(T'\) and (3). It follows

    $$\begin{aligned} M_* \Vdash f([s],[A]) \wedge f([t],[A]) \rightarrow f([s+t],[A]) \text { } \forall s,t \in \mathsf {Tm}\text { and } \forall A \in \mathsf {Fml}. \end{aligned}$$

    By the truth definition in \(\mathsf {CL}\) we find

    $$\begin{aligned} \text {if } f([s],[A])^* = \mathbb {T} \text { and } f([t],[A])^* = \mathbb {T} \text { then } f([s+t],[A])^* = \mathbb {T}. \end{aligned}$$

    From the definition of J in M we get

    $$\begin{aligned} \text {if } J([s],[A]) \text { and } J([t],[A]) \text { then } J([s]+[t],[A]). \end{aligned}$$

Knowing that M is a semiring model we prove

$$\begin{aligned} M_* \Vdash A(t_1,...,t_n)' \Leftrightarrow M,w \Vdash A(x_1,...,x_n) \end{aligned}$$
(4)

by induction on the structure of A, where \(w(x_i)=[t_i]\):

  • Case \(A=\perp \). We have \(M_* \nVdash \perp '\) and \(M,w \nVdash \perp \).

  • Case \(A=P\). We have \(M_* \Vdash P' \Leftrightarrow M_* \Vdash P \Leftrightarrow P^*=\mathbb {T} \Leftrightarrow M,w \Vdash P\).

  • Case \(A=B \rightarrow C\). We have \(M_* \Vdash (B \rightarrow C)(t_1,...,t_n)'\)

    \(\Leftrightarrow M_* \Vdash B(t_1,...,t_n)' \rightarrow C(t_1,...,t_n)' \)

    \(\Leftrightarrow M_* \nVdash B(t_1,...,t_n)' \text { or } M_* \Vdash C(t_1,...,t_n)' \)

    \(\Leftrightarrow M,w \nVdash B(x_1,...,x_n) \text { or } M,w \Vdash C(x_1,...,x_n)\)     \(\text {(by induction hypothesis)}\)

    \(\Leftrightarrow M,w \Vdash B(x_1,...,x_n) \rightarrow C(x_1,...,x_n)\)

    \(\Leftrightarrow M,w \Vdash (B \rightarrow C)(x_1,...,x_n)\).

  • Case \(A=s:B\). We have \(M_* \Vdash (s:B)(t_1,...,t_n)'\)

    \(\Leftrightarrow M_* \Vdash (s(t_1,...,t_n):B(t_1,...,t_n))'\)

    \(\Leftrightarrow M_* \Vdash f([s(t_1,...,t_n)], [B(t_1,...,t_n)]) \quad \text {(by definition of }'\text {)}\)

    \(\Leftrightarrow J([s(t_1,...,t_n)], [B(t_1,...,t_n)])\)     (by definition of J)

    \(\Leftrightarrow J(s(x_1,...,x_n)_I^w, [B(t_1,...,t_n)])\)     (by Lemma 4)

    \(\Leftrightarrow J(s(x_1,...,x_n)_I^w, B(x_1,...,x_n)_I^w)\)     (by Lemma 5)

    \(\Leftrightarrow M,w \Vdash s(x_1,...,x_n):B(x_1,...,x_n)\)

    \(\Leftrightarrow M,w \Vdash (s:B)(x_1,...,x_n)\)

Now we show \(M \Vdash T\), i.e. \(M,w \Vdash T\) for all valuations w. Hence let w be an arbitrary valuation (assume \(w(x_i)=[t_i]\)) and \(A(x_1,...,x_n) \in T\). It follows \(A(x_1,...,x_n)' \in T'\) and by (3) also \(A(t_1,...,t_n)' \in T'\). From \(M_* \Vdash T'\) we get \(M_* \Vdash A(t_1,...,t_n)'\). (4) implies \(M,w \Vdash A(x_1,...,x_n)\). Since w was arbitrary we conclude \(M \Vdash T\).

Now we consider the special case of (4) where \(w=v\) with \(v(x)=[x]\). We have

$$\begin{aligned} M_* \Vdash A(x_1,...,x_n)' \Leftrightarrow M,v \Vdash A(x_1,...,x_n) \end{aligned}$$

Remembering \(M_* \nVdash F'\), we derive \(M,v \nVdash F\), which finishes the proof.    \(\square \)

4 Realization

Realization is concerned with the relationship between justification logic and modal logic. In this section, we let \(\circ \) be the mapping from \(\mathsf {Fml}\) to formulas of the modal logic \(\mathsf {K}\) that replaces all occurrences of s :  in a formula of \(\mathsf {SE}\) with \(\Box \). We immediately get the following lemma.

Lemma 8

For any formula A we have

$$ \vdash _{\mathsf {SE}} A \quad \textit{implies}\quad \vdash _{\mathsf {K}} A^\circ . $$

To investigate mappings from modal logic to \(\mathsf {SE}\), we need the notion of an axiomatically appropriate theory.

Definition 10

A theory T is called axiomatically appropriate if

  1. 1.

    for each axiom A of \(\mathsf {SE}\), there is a constant c such that \(c:A \in T\) and

  2. 2.

    for each \(B \in T\), there is a constant c such that \(c:B \in T\).

Using axiomatically appropriate theories, we get an analogue of modal necessitation in \(\mathsf {SE}\).

Lemma 9 (Internalization)

Let T be an axiomatically appropriate theory. For any formula A, there exists a ground term t such that

$$ T \vdash A \quad \textit{implies}\quad T \vdash t:A. $$

For the following definition we need the notion of positive and negative occurrences of \(\Box \) within a given formula A. First we assign a polarity to each subformula occurrence within A as follows.

  1. 1.

    The only occurrence of A within A is given positive polarity.

  2. 2.

    If a polarity is already assigned to an occurrence \(B \rightarrow C\) within A, then the same polarity is assigned to C and the opposite polarity is assigned to B.

  3. 3.

    If a polarity is already assigned to an occurrence \(\Box B\) within A, then the same polarity is assigned to B.

The leading \(\Box \) in an occurrence of \(\Box B\) within A has the same polarity as the occurrence of \(\Box B\) within A.

Definition 11

A realization r is a mapping from modal formulas to \(\mathsf {Fml}\) such that for each modal formula F we have \((r(F))^\circ =F\). A realization is normal if all negative occurrences of \(\Box \) are mapped to distinct justification variables.

For the rest of this section, we require axiomatically appropriate theories T also to be schematic, which is a technical requirement saying roughly that T respects substitutions, for a discussion of this property see [30]. Schematicness is needed for the following two claims.

We are confident that Kuznets’ realization procedure [28] can be applied in the context of \(\mathsf {SE}\). Thus we have the following:

Conjecture 1

Let T be an axiomatically appropriate theory such that for some constant c,

$$ c: (A \rightarrow (A\vee B)) \in T \quad \text {and}\quad c: (B \rightarrow (A\vee B)) \in T. $$

Then there exists a realization r such that for all modal formulas F,

$$ \vdash _{\mathsf {K}} F \quad \text {implies}\quad T \vdash _{\mathsf {SE}} r(F). $$

However, the realization obtained by the previous theorem will not be normal. In traditional justification logic normal realizations can be achieved using the \(+\) operation, which there (unlike in \(\mathsf {SE}\)) is axiomatized by \(s:A \vee t:A \rightarrow s+t:A\).

Since we work with general theories (instead of simple constant specifications) and with variables that are interpreted universally, we can mimick the traditional \(+\) operation and perform the usual realization procedure given in [5, 30].

Conjecture 2

Let T be an axiomatically appropriate theory such that for some constant c

$$ x:A \rightarrow c\cdot x \cdot y: (A\vee B) \in T \quad \text {and}\quad y:B \rightarrow c\cdot x \cdot y: (A\vee B) \in T. $$

Then there exists a normal realization r such that for all modal formulas F,

$$ \vdash _{\mathsf {K}} F \quad \text {implies}\quad T \vdash _{\mathsf {SE}} r(F). $$

5 Applications

The semiring interpretation of evidence has a wide range of applications. Many of them require a particular choice of the semiring. The following are of particular interest to us (see also [26]):

  • \(V = ([0,1],\max ,\cdot ,0,1)\) is called the Viterbi semiring. We can think of the elements of V as confidence scores and use them to model trust.

  • \(T = (\mathbb {R}^\infty _{+},\min ,+,\infty ,0)\) is called the tropical semiring. This is connected to shortest path problems. In the context of epistemic logic, we can employ this semiring to model the costs of obtaining knowledge. Among other things, this might provide a fresh perspective on the logical omniscience problem, related to the approaches in [12,13,14].

  • \(P = (\mathcal {P}(S),\cup ,\cap ,\emptyset ,S)\) is called the powerset lattice (semiring). This is closely related to the recently introduced subset models for justification logic [31,32,33]. This semiring can be used to model probabilistic evidence and aggregation thereof, see, e.g., [9].

  • \(F = ([0,1],\max ,\max (0,a+b-1),0,1)\) is called the Łukasiewicz semiring. We can use it to model fuzzy evidences. Ghari [22] provides a first study of fuzzy justification logic that is based on this kind of operations for combining evidence.

Another stream of possible applications emerges from the fact that terms with variables represent actual functions. If the underlying semiring is \(\omega \)-continuous, then the induced polynomial functions are \(\omega \)-continuous and, therefore, monotone [27]. Hence, they have least and greatest fixed points. Thus it looks very promising to consider this kind of semirings to realize modal fixed point logics like common knowledge.

Common knowledge of a proposition A is a fixed point of \(\lambda X.(\mathsf {E}A \wedge \mathsf {E}X)\). There are justification logics with common knowledge available [6, 18] but their exact relationship to modal common knowledge is still open.

We believe that non-wellfounded and cyclic proof systems [1, 16, 17, 35] are the right proof-theoretic approach to settle this question. In those systems, proofs can be regarded as fixed points and hence justifications realizing those cyclic proofs will be fixed points in a semiring. For this purpose, making use of formal power series, which might be thought of as infinite polynomials, look very promising. First results in this direction have been obtained by Shamkanov [34] who presents a realization procedure for Gödel-Löb logic based on cyclic proofs.