A Substructural Approach to Explicit Modal Logic

Abstract

In this paper, we build on earlier work by Standefer (Logic J IGPL 27(4):543–569, 2019) in investigating extensions of substructural logics, particularly relevant logics, with the machinery of justification logics. We strengthen a negative result from the earlier work showing a limitation with the canonical model method of proving completeness. We then show how to enrich the language with an additional operator for implicit commitment to circumvent these problems. We then extend the logics with axioms for D, 4, and 5, which requires additional justification term operators, following the work of Pacuit (in proceedings of the fifth panhellenic logic symposium, 2005) and Rubtsova (in Grigoriev D, Harrison J (eds) Computer science—theory and applications, CSR 2006; J Logic Comput 16(5):671–684, 2006), and present the required modifications to the frame semantics. We present a simplification of the neighborhood frames from the earlier work and we close by investigating the distinctive contribution of the $+$ operator to the logic.

Justification logics are multi-modal logics for representing and reasoning about reasons and their combinations.¹ While there has been some development of justification logic in the context of intuitionistic logic, there has been little development of the area in the context of relevant logics.² Savić and Studer (2019) and (Standefer, 2019) present justification-logical extensions of relevant logics, albeit arriving at different logics. In this paper, we will build on the latter development, along the way commenting on the differences.

The combination of explicit justification modals with relevant logics is a natural combination. Both relevant and justification logics have the feature that necessary truths, as well as logical truths, need not all be equivalent. The explicit justification modals provide a method for fine-grained tracking of reasons that has a natural affinity with the fine-grained implication of relevant logics. One may have some bit of evidence x for $p\rightarrow q$ and a bit of perceptual evidence y for p, which one can combine to obtain evidence, $x\cdot y$, for q, but in so doing not fall into the (relevant-logically dubious) position of saying that other evidence z for q implies that $x\cdot y$ is evidence for q. Exploring this pairing is useful and important to provide further logical tools to use in the development of substructural epistemic logics, as well as to identify where and how standard constructions need to be modified to work in the substructural setting. With respect to the latter issue, the approach of this paper is to develop the frames so that many of the standard techniques in the area are applicable.

This work should be viewed as contribution to the burgeoning literature on substructural epistemic logics, more than as a contribution to the ongoing developments in justification logic. The reason is that this will not pursue some of the standard goals of the justification logic literature, such as Realization theorems and arithmetical completeness. Rather, this work develops epistemic enrichments of substructural logics, using the machinery of justification logics, in a way that fits with some of the philosophical outlooks associated with those logics, especially relevant logics. There have been many developments in substructural epistemic logics, particularly relevant epistemic logics, recently, some of which we will highlight. Bilková et al. (2010); Bílková et al. (2016) and Sedlár (2015, 2016) have developed different formulations of logics of knowledge. Punčochář and Sedlár (2017) have explored the logic of information pooling in a substructural setting. Punčochář (2019, 2020) has shown how to combine inquisitive logics and substructural logics.³ Wansing (2002) develops a response to Fitch’s paradox of knowability using a paraconsistent constructive relevant modal epistemic logic.

We will begin with a presentation of the basic ternary relational frames for substructural logics along with an axiomatization of the basic logic B to be used in this paper (Sect. 1). In Sect. 2, we will present the extensions of these frames, from (Standefer, 2019) , with machinery from models for justification logics and summarize a problem with using the canonical model method to prove Completeness for the provided axiom system. In Sect. 3, we strengthen a result from (Standefer, 2019) showing that for a wider range of logics extended with the standard justification logic axiom, (K) $\llbracket t\rrbracket (A\rightarrow B)\rightarrow (\llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B)$, the canonical frame does not satisfy one of the required frame conditions. Following this, we show how to extend the language with a new operator for implicit commitment and provide axioms that permit a proof of Completeness (Sect. 4). In Sect. 5, we show how to add additional justification term operators to provide stronger justification logical extensions, following the work of Pacuit (2005) and Rubtsova (2006b). In Sect. 6, we provide a simpler presentation of the neighborhood frames from Standefer (2019). Then, we develop the basic justification logic machinery without implicit commitment but with the $+$ operator, which otherwise does not appear in the paper, showing that the resulting axiom system is sound and complete for the frame semantics, provided that the evidence sets are theories (Sect. 7). Finally, in Sect. 8, we provide some concluding discussion.

1 Ternary Relational Frames

In this section, I will present the basics of the frame semantics for substructural logics and an axiomatization of the basic substructural logic B. For the basic relevant language $\mathbin {\mathscr {L}}^{-}$, we have a countably infinite set of atoms $\textsf {At}$ and complex formulas built as follows.

$$\begin{aligned} A:= p \;|\; \mathord {\sim }A\;|\; A\wedge B\;|\; A\vee B \;|\; A\rightarrow B \end{aligned}$$

We begin with the frame semantics.⁴

Definition 1

(Frame) A Routley-Meyer frame is a quadruple $\langle K,N,R,^*\rangle$ where $K\ne \emptyset$, $R\subseteq K\times K\times K$, and $^*$ is a function from K to K such that

• the relation $a\le b$ defined as $\exists x\in N(Rxab)$ is a partial order,

• if $a\in N$ and $a\le b$, then $b\in N$,

• ${{a}^{**}}=a$,

• if $a\le b$, then $b^*\le a^*$, and

• if $a\le b$ and Rbcd, then Racd.

We adopt the definition of frame where the set of normal, or regular, points $N$ may contain many points. This is in contrast to the definition of Savić and Studer (2019), who use reduced frames.⁵ The set $N$ is used for defining validity as well as defining the heredity relation, $\le$, which plays a significant role in the models.

Definition 2

(Model) A model is a pair of a frame F and a valuation $V: \textsf {At} \times K\mapsto \{ 0,1\}$ such that if $V(p,a)=1$ and $a\le b$, then $V(p,b)=1$. Where a model M is $\langle F,V\rangle$, the model is built on the frame F. Valuations are extended to the whole language as follows.

• $a\Vdash p$ iff $V(p,a)=1$

• $a\Vdash B\wedge C$ iff $a\Vdash B$ and $a\Vdash C$

• $a\Vdash B\vee C$ iff $a\Vdash B$ or $a\Vdash C$

• $a\Vdash \mathord {\sim }B$ iff $a^*\not \Vdash B$

• $a\Vdash B\rightarrow C$ iff for all b, c, if Rabc and $b\Vdash B$, then $c\Vdash C$

As is standard, the Heredity Lemma holds for these models.

Lemma 1

(Heredity) If $a\le b$ and $a\Vdash A$, then $b\Vdash A$.

This is proved via a straightforward induction on formula complexity. The Heredity Lemma continues to hold for the other models and the other languages introduced throughout this paper. A useful consequence of this lemma is the Verification Lemma.

Lemma 2

(Verification) Let M be a model. The formula $A\rightarrow B$ holds in M iff for all $a\in K$, if $a\Vdash A$, then $a\Vdash B$.

This lemma simplifies the soundness proofs. Although it will be used in those proofs, appeals to it will be left implicit.

Next, we define a useful bit of standard notation. In a given model M, the truth set $[A]_{M}=\{ a\in K: a\Vdash A\}$. The subscript on truth sets will be dropped when the model is clear from context. Now, we turn to the definitions of holding and validity.

Definition 3

(Validity) A formula A holds in a model M iff $N\subseteq [A]$.

A formula A is valid in a frame F iff A holds in all models built on F.

A formula A is valid in a class of frames ${\mathcal {F}}$, $\models _{{\mathcal {F}}}{A}$, iff A is valid in F for all $F\in {\mathcal {F}}$.

It is worth underlining here that holding, and so validity, depend on the evaluation of a formula with respect to the set $N$.⁶

The substructural, relevant logic B is axiomatized with the following axioms and rules. Note that (A8)–(A12) are rules of proof, rather than axioms, and the ‘$\Rightarrow$’ separates the premises of each rule from its conclusion.⁷

More carefully, ${\textsf {B} }$ is the smallest set of formulas containing the above axioms and closed under the above rules.

Say that $\vdash _{{\textsf {{\textsf {B} }} }}{{A}}$ if there is a proof of A from the axioms of B using the rules of B. Then we get the following.

Theorem 1

(Soundness and Completeness) Let ${\mathcal {F}}$ be the class of all Routley-Meyer frames. $\vdash _{{\textsf {{\textsf {B} }} }}{{A}}$ iff $\models _{{{\mathcal {F}}}}{A}$.

For the proof, see Routley et al. (1982, ch. 4) or Restall (2000, ch. 11). One can extend the logic with axioms by narrowing the class of frames to those that obey corresponding frame conditions, although I will not pursue that here. An exception is that in Sect. 3, I will discuss the logic R and I will present the additional axioms needed to obtain it from B.⁸

2 Evidence Frames

We want to add to the basic substructural logic B the machinery of justification logic. A natural way to do this is via the addition of a binary accessibility relation S and an evidence function ${\mathcal {E}}$, the natural combination of Fitting models and ternary relational frames.⁹ We extend the basic language $\mathbin {\mathscr {L}}^{-}$ to $\mathbin {\mathscr {L}}$ by adding a countably infinite set of justification variables, $x_{1},\ldots ,x_{n},\ldots$, as atomic terms and defining the set $\textsf {Terms}$ as follows.¹⁰

$$\begin{aligned} t:= x \;|\; (t\cdot s) \end{aligned}$$

The justification variables represent particular justifications for claims, such as a proof or a particular bit of visual evidence. The dot represents one form of justification combination, akin to the application operation $\circ$ on theories considered in the next section.¹¹ This is an extractive form of combination, clarified in the (K) axiom below and its related frame condition. An alternative form of combination, $+$, which acts as a straightforward pooling operation, will be considered in more detail in Sect. 7. The omission of $+$ from the initial sections is largely because the dot operator appears the most interesting from a logical point of view and receives more attention in the literature.¹²

The definition of formula is then expanded to permit formulas of the form $\llbracket t\rrbracket A$, where $t\in \textsf {Terms}$.¹³

$$\begin{aligned} A:= p \;|\; \mathord {\sim }A\;|\; A\wedge B\;|\; A\vee B \;|\; A\rightarrow B \;|\; \llbracket t\rrbracket A \end{aligned}$$

We can now give the frame semantics.

Definition 4

(RME-frames) A Routley-Meyer evidence frame, or RME-frame, is a tuple $\langle K, N, R,^*, S, {\mathcal {E}}\rangle$, where the first four components make up a Routley-Meyer frame, $S\subseteq K\times K$, ${\mathcal {E}}: \textsf {Terms} \times K\mapsto {\mathcal {P}}(\mathbin {\mathscr {L}})$ such that

• (1) if $a\le b$ and Sbc, then Sac,

• (2) if $a\le b$, then ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$,

• (3) if $\exists x(Rabx \wedge Sxc)$, then $\exists y,\exists z(Ryzc\wedge Say\wedge Sbz)$, and

• (4) if Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$, then $B\in {\mathcal {E}}(t\cdot s,c)$.

The definition of model is extended to RME-models by adding the following clause for the new connectives.

• $a\Vdash \llbracket t\rrbracket A$ iff for all b such that Sab, $b\Vdash A$, and $A\in {\mathcal {E}}(t,a)$

The Heredity Lemma extends to RME-models.

Lemma 3

Let M be a RME-model. If $a\le b$ and $a\Vdash A$, then $b\Vdash A$.

Proof

There is one new case for RME-models, namely the justification modal.

Suppose $a\le b$ and $a\Vdash \llbracket t\rrbracket B$. Suppose that $b\not \Vdash \llbracket t\rrbracket B$. Then either there is a c such that Sbc and $c\not \Vdash B$ or $B\not \in {\mathcal {E}}(t,b)$.

Suppose there is a c such that Sbc and $c\not \Vdash B$. From the frame conditions, then Sac, so $a\not \Vdash \llbracket t\rrbracket C$, contradicting the assumption.

Suppose that $B\not \in {\mathcal {E}}(t,b)$. Since $a\Vdash \llbracket t\rrbracket B$, we have $B\in {\mathcal {E}}(t,a)$. From the frame conditions, as $a\le b$, ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$, so $B\in {\mathcal {E}}(t,b)$, contradicting the assumption.

Therefore, $b\Vdash \llbracket t\rrbracket B$. $\square$

Let the logic B.K be B with the addition of the axiom (K) $\llbracket t\rrbracket (A\rightarrow B)\rightarrow (\llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B)$.

We can prove Soundness as in Standefer (2019). Let ${\mathcal {E}}$ be the class of all RME-frames.

Theorem 1

If $\vdash _{{\textsf {{\textsf {B.K} }} }}{{A}}$, then $\models _{{{\mathcal {E}}}}{A}$.

Proof

The proof is by a fairly routine inductive argument. $\square$

Completeness for relevant logics is often proved via a Henkin-style canonical model construction. (Standefer, 2019) shows that the canonical frame, to be defined, for a stronger logic, T.K, does not satisfy condition (3) of definition 4 above. In the next section, I will improve that result and show that the canonical frame for R.K, where R is the strongest relevant logic considered in that paper, does not satisfy that frame condition. In the section after that, I will show how to enrich the logic so as to avoid that result. Before proceeding to the next section, however, it will be worth stopping to comment on an interpretation of these models and to consider the differences between the two approaches to relevant logic with justifications.

The ternary relational models admit different philosophical interpretations. One interpretation that seems to fit neatly with the apparatus of justification logics is the interpretation taking the points to represent bodies of information.¹⁴ This information is the information available in a situation. The ternary relation holding between some situations indicates that there is a channel in the first transferring information from the second situation to the third, such as via a law or law-like regularity. Some of the information in a situation supports or bears on particular claims, as codified by ${\mathcal {E}}$, and the information is taken to represent how things are in some situations, the epistemic alternatives represented by S. The lack of conditions on S reflects the freedom of information in situations in the present setting.¹⁵

The RME-models of this section are a straightforward combination of the ternary relational models for substructural logics and the Fitting models for (classical) justification logics. In this setting, the verification condition for a justification formula matches that of the usual Fitting models, and it is repeated here for ease of reference.

• $a\Vdash \llbracket t\rrbracket A$ iff for all b such that Sab, $b\Vdash A$, and $A\in {\mathcal {E}}(t,a)$

The two approaches to adding justifications to relevant logics deal with this clause in different ways. (Savić and Studer 2019) take an approach that drops the first part of the clause, using only the evidence function portion. This, arguably, leaves out the modal element and makes it more similar to an awareness logic, but it does keep the logic more in line with standard justification logics.¹⁶ Indeed, in their models, Savić and Studer eschew a modal accessibility relation, opting instead for an operation, $\spadesuit$, assigning sets of formulas to terms at points, analogously to ${\mathcal {E}}$. Conditions on this operation ensure that it assigns acceptable sets of formulas to terms and that it interacts appropriately with the ternary relation and the heredity ordering.

Standefer (2019), on the other hand, drops the second part of the clause, opting instead for a proliferation of binary relations. These relations require frame conditions to ensure the validity of the (K) axiom. Dropping the evidence portion of the clause has consequences for the logic, such as the validity of the rule (Mono), $A\rightarrow B\Rightarrow \llbracket t\rrbracket A\rightarrow \llbracket t\rrbracket B$, which is not a feature of standard justification logics. Below, we will show how to extend the language in a way that permits one to keep the verification condition above while also obtaining Completeness results using the canonical model method. Before exploring the extensions, we will prove that the canonical model method does not work for the logic R.K, obtained by adding the axiom (K) to the relevant logic R, which result also shows that the method does not work for any logic contained in R.K, including B.K.

3 Canonical Frame

In this section, we will show that the canonical frame for the logic R.K is not in the class of RME-frames that obey the frame conditions for R.K. In particular, it lacks the frame condition for (K). This will be done by constructing two theories, ${\hat{a}}$ and ${\hat{b}}$ that are related, via R, to a theory that contains no formulas of the form $\llbracket t\rrbracket A$, which is used to force a violation of the frame condition for (K).

For this section, the logic of interest is R.K, which adds to B.K the following axioms.

• (R1) $(A\rightarrow \mathord {\sim }B)\rightarrow (B\rightarrow \mathord {\sim }A)$

• (R2) $(A\rightarrow B)\rightarrow ((B\rightarrow C)\rightarrow (A\rightarrow C))$

• (R3) $A\rightarrow ((A\rightarrow B)\rightarrow B)$

• (R4) $(A\rightarrow (A\rightarrow B))\rightarrow (A\rightarrow B)$

The definition of a theorem of R or of R.K is adapted in the usual way.

Next, we need some notions that are standard in the area. For the definitions used in this section, all logics L are assumed to extend B.

Definition 5

(Theories) A set X of formulas is a L-theory iff both (i) if $A\in X$ and $\vdash _{{\textsf {{\textsf {L} }} }}{{A\rightarrow B}}$, then $B\in X$, and (ii) if $A\in X$ and $B\in X$, then $A\wedge B\in X$.

A theory X is prime iff $A\vee B\in X$ implies $A\in X$ or $B\in X$.

A theory X is L-regular iff $\vdash _{{\textsf {{\textsf {L} }} }}{{A}}$ implies $A\in X$.

A pair of sets of formulas $\langle X,Y\rangle$ is L-inconsistent iff there are $A_1,\ldots ,A_n\in X$ and $B_1,\ldots ,B_m\in Y$ such that $\vdash _{{\textsf {{\textsf {L} }} }}{{(A_1\wedge \ldots \wedge A_n)\rightarrow (B_1\vee \ldots \vee B_m)}}$.

A pair of sets of formulas $\langle X,Y\rangle$ is L-consistent iff it is not L-inconsistent.

The concept of L-consistency replaces negation-consistency, since the logics under consideration in this paper are paraconsistent.¹⁷L-consistency is used to prove the Prime Extension Lemma.

Lemma 4

(Prime Extension) If a pair $\langle X,Y\rangle$ of sets of formulas is L-consistent, then there is a prime L-theory $Z\supseteq X$ such that $\langle Z,Y\rangle$ is L-consistent.

Proof

For the proof technique, see Routley et al. (1982, ch. 4) or Restall (2000, ch. 5). $\square$

The canonical frame for R.K is defined as follows.

• K is the set of prime R.K-theories.

• $N=\{ a\in K: a \text { is }{\textsf {R.K} }\text {-regular}\}$.

• Rabc iff for all A, B, if $A\rightarrow B\in a$ and $A\in b$, then $B\in c$.

• $a^*=\{ A\in \mathbin {\mathscr {L}}: \mathord {\sim }A\not \in a\}$.

• Sab iff $\{ A\in \mathbin {\mathscr {L}}: \exists t\in \textsf {Terms} , \llbracket t\rrbracket A\in a\}\subseteq b$.

• ${\mathcal {E}}(t,a)=\{ A\in \mathbin {\mathscr {L}}: \llbracket t\rrbracket A\in a\}$.

• $V(p,a)=1$ iff $p\in a$.

We will now argue that the defined canonical frame does not satisfy condition (3) of definition 4, that if $\exists x(Rabx \wedge Sxc)$, then $\exists y,\exists z(Ryzc\wedge Say\wedge Sbz)$. This will be done in stages.

To begin, for any logic L extending B, for L-theories x and y, let $x\circ y=\{ C\in \mathbin {\mathscr {L}}: \exists B\in \mathbin {\mathscr {L}}, B\rightarrow C\in x\wedge B\in y\}$.

Lemma 5

Let L be a logic extending B. If x and y are L-theories, then $x\circ y$ is an L-theory.

Proof

See (Fine, 1974) Lemma 2. $\square$

We do not need the full generality of this lemma for what follows in this section, since we are interested in the case where L is R.K.

Next let $a=\{ \llbracket x\rrbracket {((p\rightarrow q)\wedge r)}\}$ and let $b=\{ \llbracket y\rrbracket p\}$. Let ${\hat{a}}$ be the least theory containing a and let ${\hat{b}}$ be the least theory containing b. Note that ${\hat{a}}$ and ${\hat{b}}$ may not be prime.

Lemma 6

If $B\in {\hat{a}}$, then $\vdash _{{\textsf {{\textsf {R.K} }} }}{{\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow B}}$.

If $B\in {\hat{b}}$, then $\vdash _{{\textsf {{\textsf {R.K} }} }}{{(\llbracket y\rrbracket {p})\rightarrow B}}$.

Proof

These follow from the definition of theory. $\square$

Next, consider the algebra $M_{0}$ from Priest (2008, pp. 205–206), presented in Table 1. $M_{0}$, in a different notation, is used by Anderson and Belnap (1975, pp. 252–254) to show that R has the variable sharing property: if $\vdash _{{\textsf {{\textsf {R} }} }}{{A\rightarrow B}}$, then A and B share a propositional variable. Here, we will use it in a key step showing that the R.K canonical frame does not satisfy the frame condition for (K).¹⁸

Table 1 Hasse diagram and tables for $M_{0}$

A valuation v on this algebra is a function from $\textsf {At}$ to V such that conjunction and disjunction are meet and join, respectively, and the arrow and negation are interpreted according to the table. A formula is designated on a valuation just in case it takes one of the primed values. A formula is valid on this algebra iff it is designated on all valuations.

All axioms of R are valid and the rules of R preserve validity.¹⁹ Let a (K)-valuation be a valuation v such that $v(\llbracket t\rrbracket (A\rightarrow B))=0$, for all formulas A, B and all terms $t\in \textsf {Terms}$. If v is a (K)-valuation, then the (K) axiom is designated on v. The definition of (K)-valuation provides much latitude for values to assign to formulas of the form $\llbracket t\rrbracket B$, where B is not a conditional, as it essentially treats such formulas as distinct atoms. We will use these valuations to prove a lemma showing that certain formulas are excluded from ${\hat{a}}\circ {\hat{b}}$.

Lemma 7

Let v be a (K)-valuation such that $v(\llbracket x\rrbracket ((p\rightarrow q)\wedge r))=b$ and $v(\llbracket y\rrbracket p)=n$ and for all formulas of the form $\llbracket t\rrbracket B$, where B is neither $(p\rightarrow q)\wedge r$ nor p and B is not a conditional, $v(\llbracket t\rrbracket B)=0$. Let D be a disjunction of formulas of the form $\llbracket t_{i}\rrbracket B_{i}$, for some $i>0$. Then $v(\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow (\llbracket y\rrbracket p\rightarrow D))=0$.

Proof

Let v and D be as in the lemma. There are four cases for v(D), depending on the disjuncts of D.

Case: neither $\llbracket x\rrbracket ((p\rightarrow q)\wedge r)$ nor $\llbracket y\rrbracket p$ are disjuncts. Then $v(D)=0$. Then the evaluation reduces to $b\rightarrow (n\rightarrow 0)=b\rightarrow 0=0$.

Case: $\llbracket x\rrbracket ((p\rightarrow q)\wedge r)$ is a disjunct but not $\llbracket y\rrbracket p$. Then $v(D)=b$. Then the evaluation reduces to $b\rightarrow (n\rightarrow b)=b\rightarrow 0=0$.

Case: $\llbracket x\rrbracket ((p\rightarrow q)\wedge r)$ is not a disjunct but $\llbracket y\rrbracket p$ is. Then $v(D)=n$. Then the evaluation reduces to $b\rightarrow (n\rightarrow n)=b\rightarrow n'=0$.

Case: both $\llbracket x\rrbracket ((p\rightarrow q)\wedge r)$ and $\llbracket y\rrbracket p$ are disjuncts. Then $v(D)=1$. Then the evaluation reduces to $b\rightarrow (n\rightarrow 1)=b\rightarrow n'=0$.

In all cases, $v(\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow (\llbracket y\rrbracket p\rightarrow D))=0$, as desired. $\square$

Since the (K)-valuations are required to assign 0 to formulas of the form $\llbracket t\rrbracket (A\rightarrow B)$ but unconstrained on other formulas, there is no constraint on the value they can assign to formulas of the form $\llbracket t\rrbracket (A\wedge B)$, such as $\llbracket x\rrbracket ((p\rightarrow q)\wedge r)$ above. We use this feature to prove an important fact about ${\hat{a}}\circ {\hat{b}}$ in the next lemma, and this will allow us to show that the canonical model for R.K violates the frame condition for (K).

Lemma 8

No disjunction D of formulas of the form $\llbracket t_{i}\rrbracket B_{i}$, for some $i>0$, is in ${\hat{a}}\circ {\hat{b}}$.

Proof

Suppose otherwise, so there is a disjunction D of formulas of the form $\llbracket t_{i}\rrbracket B_{i}$, for some $i>0$, in ${\hat{a}}\circ {\hat{b}}$. Then there must be a C such that $C\rightarrow D\in {\hat{a}}$ and $C\in {\hat{b}}$. By lemma 6, $\vdash _{{\textsf {{\textsf {R.K} }} }}{{\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow (C\rightarrow D)}}$ and $\vdash _{{\textsf {{\textsf {R.K} }} }}{{\llbracket y\rrbracket p\rightarrow C}}$. It then follows that $\vdash _{{\textsf {{\textsf {R.K} }} }}{{\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow (\llbracket y\rrbracket p\rightarrow D)}}$.²⁰ By lemma 7, there is a (K)-valuation v such that $v(\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow (\llbracket y\rrbracket p\rightarrow D))=0$. Therefore, it is not the case that $\vdash _{{\textsf {{\textsf {R.K} }} }}{{\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\rightarrow (\llbracket y\rrbracket p\rightarrow D)}}$, which is a contradiction. Therefore, there is no such disjunction D in ${\hat{a}}\circ {\hat{b}}$. $\square$

Corollary 1

The pair $\langle {\hat{a}}\circ {\hat{b}}, \{ \llbracket t\rrbracket B\in \mathbin {\mathscr {L}}: t\in \textsf {Terms} , B\in \mathbin {\mathscr {L}}\}\rangle$ is R.K-consistent.

Using this corollary and the Prime Extension Lemma, we can extend ${\hat{a}}\circ {\hat{b}}$ to a prime theory d that contains no formulas of the form $\llbracket t\rrbracket B$. So, Sde for all $e\in K$. Let c be a prime theory such that $q\not \in c$. Then, Sdc.

Since ${\hat{a}}$ and ${\hat{b}}$ are theories and d is a prime theory, we can extend them to prime theories $a'$ and $b'$ respectively such that $Ra'b'd$. This establishes the antecedent of the frame condition, recorded below.

Lemma 9

The canonical frame for R.K is such that $\exists x(Ra'b'x\wedge Sxc)$.

To show that the consequent of the frame condition is false, first note that any prime theory g such that $Sa'g$ will be such that $p\rightarrow q\in g$. Similarly, any prime theory h such that $Sb'h$ will be such that $p\in h$. Next, note that there are such prime theories.

Lemma 10

For all prime theories g and h such that $Sa'g$ and $Sb'h$, it is not the case that Rghc.

Proof

Let g and h be prime theories such that $Sa'g$ and $Sb'h$. As $\llbracket x\rrbracket ((p\rightarrow q)\wedge r)\in a'$, $(p\rightarrow q)\wedge r\in g$, so $p\rightarrow q\in g$. Similarly, as $\llbracket y\rrbracket p\in b'$, we have $p\in h$. Since $p\rightarrow q\in g$ and $p\in h$, but $q\not \in c$, by definition it is not the case that Rghc. $\square$

That establishes the desired result.

Theorem 2

The canonical frame for R.K does not obey the frame condition that if $\exists x(Rabx \wedge Sxc)$, then $\exists y,\exists z(Ryzc\wedge Say\wedge Sbz)$.

Proof

An instance of the antecedent is established by lemma 9 and the falsity of the consequent is established by lemma 10. $\square$

The canonical frame for R.K does not satisfy one of the necessary frame conditions.²¹ The counterexample carries over to weaker logics, including B.K, although it does not obviously affect logics that contain the weakening axiom. This presents a serious hurdle to proving Completeness for R.K, or B.K, with respect to RME-frames.²² In the next section, I will show how to remedy this problem through an extension of the language and the logic.

4 Implicit Commitment

Justifications, in the context of justification logic, are often taken to represent explicitly considered justifications. (Giordani, 2013) has extended basic (classical) justification logics with implicit justification operators. It is this idea, distinguishing implicit commitment from explicit justification, that will provide a route to proving Completeness.²³

We enrich the justification language with a unary operator, $\Box$, so that $\Box A$ is to be read as “the agent has an implicit commitment to A”. There are a two primary differences between this work and Giordani’s.²⁴ First, we are working a substructural base logic, whereas Giordani uses classical logic. Second, Giordani uses implicit justification modalities $[j]^*$ for each justification term j, whereas the implicit commitment modality $\Box$ collects together all the justifications. Giordani’s implicit justifications occupy an intermediate level between the explicit justification modals and the implicit commitment modality. Giordani’s implicit justification modals are not closed under provable entailment, which would be disastrous in classical logic, so they differ also from the justification modals considered by Standefer (2019).

The addition of the implicit commitment operator has two primary upshots. First, philosophically, it gives us a way to shift perspective from particular bits of information available in relation to particular claims to instead admitting whatever information is available. This change of perspective permits one to combine evidence more flexibly, albeit at the cost of losing information about the source of that evidence and its manner of combination. In the model, this reflects the fact that ${\mathcal {E}}$ does not feature in the verification condition for $\Box$, as that jettisons the fine-grained information about what claims any bit of information bears on.²⁵ Second, the implicit commitment operator permits an alternative definition of the canonical frame that avoids the problems of the previous section. In particular, the definition of S is given in terms of $\Box$, rather than in terms of an existential quantification over $\textsf {Terms}$. This is sufficient, given the logic, to show that the canonical frame obeys the required conditions.

The language extended with $\Box$ will be $\mathbin {\mathscr {L}}^{\Box }$, defined as follows.

$$\begin{aligned} A:= p \;|\; \mathord {\sim }A\;|\; A\wedge B\;|\; A\vee B \;|\; A\rightarrow B \;|\; \llbracket t\rrbracket A \;|\; \Box A \end{aligned}$$

The verification condition for the new connective is

• $a\Vdash \Box A$ iff for all b, if Sab, then $b\Vdash A$.

For the remainder of this section, we will treat RME-frames and -models as frames and models for the justification language extended with the implicit commitment modality, and the definitions for validity are carried over as well. We must verify that the Heredity Lemma still holds.

Lemma 11

(Heredity) If $a\le b$ and $a\Vdash A$, then $b\Vdash B$.

Proof

The new case is when A is of the form $\Box B$. The argument for this case is similar to that of the first subcase presented in Sect. 2. $\square$

A logic for the extended language can be had by adding to the axioms and rules of B.K the axiom and rule

(C):

${\Box A\wedge \Box B\rightarrow \Box (A\wedge B)}$,

(JB):

$\llbracket t\rrbracket A\rightarrow \Box A$,

(K$\Box$ ):

$\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)$, and

(RM):

$A\rightarrow B\Rightarrow \Box A\rightarrow \Box B$.

Call the resulting logic B.KI. We can then show Soundness and Completeness for B.KI with respect to ${\mathcal {E}}$.

Theorem 3

(Soundness) If $\vdash _{{\textsf {{{\textsf {B.KI} }}} }}{{A}}$, then $\models _{{{\mathcal {E}}}}{A}$.

Proof

Most of the cases have already been covered, leaving (C), (JB), (K$\Box$ ), and (RM). The cases for (C) and (RM) are handled by the work of Fuhrmann (1988), so I will deal with the remaining cases.

For (JB), suppose $a\Vdash \llbracket t\rrbracket B$. Then for all b such that Sab, it is the case that $b\Vdash B$, and $B\in {\mathcal {E}}(t,a)$. So, for all b such that Sab, $b\Vdash B$, which implies $a\Vdash \Box B$, as desired.

For (K$\Box$ ), suppose $a\Vdash \Box (B\rightarrow C)$. We want to show that $a\Vdash \Box B\rightarrow \Box C$. Suppose that Rabc and $\Box B$ but $c\not \Vdash \Box C$. Then there is a d such that Scd and $d\not \Vdash C$. From the frame conditions, it follows that $\exists y,\exists z(Say\wedge Sbz\wedge Ryzc)$. Let g and h be witnesses for the existentials, so that Sag, Sbh, and Rghc. It follows that $g\Vdash B\rightarrow C$ and $h\Vdash B$, which implies $c\Vdash C$, which contradicts the assumption. $\square$

To show Completeness, we reuse the definition of the canonical model from earlier, changing the relevant logic to B.KI in the definitions and modifying the definition of the canonical binary accessibility relation as follows to take advantage of the expanded language, where $a^{-\Box }=\{ B\in \mathbin {\mathscr {L}}^{\Box }: \Box B\in a\}$.

• Sab iff $a^{-\Box }\subseteq b$.

We prove a lemma about the sets $a^{-\Box }$.

Lemma 12

For any B.KI-theory a, $a^{-\Box }$ is a B.KI-theory.

Proof

See (Fuhrmann, 1988). $\square$

We have to verify that the canonical frame satisfies the frame conditions for RME-frames.

Lemma 13

The canonical frame satisfies the following frame conditions.

• (1) if $a\le b$ and Sbc, then Sac,

• (2) if $a\le b$, then ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$,

Proof

For these, we note that the definition of the canonical R relation has the consequence that $a\le b$ iff $a\subseteq b$.

For (1), suppose $a\le b$ and Sbc. Since $a\le b$, $a\subseteq b$, so $a^{-\Box }\subseteq b^{-\Box }$. It follows that Sac, as desired.

For (2), suppose $a\le b$ and $B\in {\mathcal {E}}(t,a)$. Then $\llbracket t\rrbracket B\in a$. Since $a\le b$, $a\subseteq b$, so $\llbracket t\rrbracket B\in b$, and so $B\in {\mathcal {E}}(t,b)$. $\square$

Next, I will prove that the canonical frame satisfies the condition that was so elusive in Sect. 3.

Lemma 14

The canonical frame satisfies the condition that if $\exists x(Rabx \wedge Sxc)$, then $\exists y,\exists z(Ryzc\wedge Say\wedge Sbz)$.

Proof

Suppose that $\exists x(Rabx \wedge Sxc)$. Let d be a prime B.KI-theory such that Rabd and Sdc. We will show that $a^{-\Box }\circ b^{-\Box }\subseteq c$. Suppose that $A\rightarrow B\in a^{-\Box }$ and $A\in b^{-\Box }$. Then, $\Box (A\rightarrow B)\in a$ and $\Box A\in b$. From (K$\Box$ ), it follows that $\Box A\rightarrow \Box B\in a$. As Rabd, it follows that $\Box B\in d$, so $B\in c$. Therefore, $a^{-\Box }\circ b^{-\Box }\subseteq c$.

By lemma 12, $a^{-\Box }$ and $b^{-\Box }$ are B.KI-theories. Using the Prime Extension Lemma, these can be extended to prime theories, g and h, respectively, such that Sag, Sbh, and Rghd. This suffices for the consequent of the condition. $\square$

That leaves one final condition.

Lemma 15

The canonical frame satisfies the condition that if Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$, then $B\in {\mathcal {E}}(t\cdot s,c)$.

Proof

Suppose that Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$. From the definition of ${\mathcal {E}}$, $\llbracket t\rrbracket (A\rightarrow B)\in a$ and $\llbracket s\rrbracket A\in b$. From (K), $\llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket {B}\in a$. As Rabc, $\llbracket t\cdot s\rrbracket B\in c$, so $B\in {\mathcal {E}}(t\cdot s,c)$, as desired. $\square$

The canonical frame satisfies all the conditions to be an RME-frame, which leaves the Truth Lemma.

Lemma 16

(Truth) For all formulas A, $A\in a$ iff $a\Vdash A$

Proof

This is proved by induction on formula complexity. The inductive hypothesis says that that for formulas C of complexity less than n, $C\in a$ iff $a\Vdash C$, for all $a\in K$. Most of the cases are standard, so I will present the cases for the justification and implicit modals.

Let A be of the form $\llbracket t\rrbracket B$. Suppose that $\llbracket t\rrbracket B\in a$. Suppose that Sab. From axiom (JB), $\Box B\in a$, so $B\in b$. By the inductive hypothesis, $b\Vdash B$. By definition, $B\in {\mathcal {E}}(t,a)$, so we have that $a\Vdash \llbracket t\rrbracket B$.

Suppose that $\llbracket t\rrbracket {B}\not \in a$. Then $B\not \in {\mathcal {E}}(t,a)$, so $a\not \Vdash \llbracket t\rrbracket B$.

Let A be of the form $\Box B$. Suppose that $\Box B\in a$. Suppose that Sab. Then $B\in b$, so by the inductive hypothesis, $b\Vdash B$, which suffices for $a\Vdash \Box B$.

Suppose that $\Box B\not \in a$. Then $B\not \in a^{-\Box }$. We can then use the Prime Extension Lemma to obtain a prime theory $b\supseteq a^{-\Box }$ such that Sab and $B\not \in b$. By the inductive hypothesis, $b\not \Vdash B$, so $a\not \Vdash \Box B$. $\square$

These are all the pieces we need for Completeness.

Theorem 4

(Completeness) If $\models _{{{\mathcal {E}}}}{A}$, then $\vdash _{{\textsf {{{\textsf {B.KI} }}} }}{{A}}$.

Proof

Suppose $\not \vdash _{\textsf {B.KI} }{A}$. Then there is a prime, B.KI-regular, B.KI-theory a in the canonical model such that $A\not \in a$. By lemma 16, $a\not \Vdash A$, which implies $\not \models _{{{\mathcal {E}}}}{A}$. $\square$

We have, then, proven Completeness for B.KI with respect to ${\mathcal {E}}$. This was done by using the implicit commitment modal to define the canonical binary accessibility relation. Thus, we have shown how to obtain Completeness results using the standard verification condition for justification modals from Fitting models in modal extensions of models for relevant logics. The arguments of this section extend to completeness for L.KI, for many logics L between B and R. Arguments in later sections will be similarly general, working when the base logic is extended to one of many logics between B and R.

It is most natural to view the connective $\Box$ as an implicit commitment modality, extending the justifications. The construction just given provides a formal way to turn this relationship on its head. If one has a relevant modal logic with (C), (K$\Box$ ), and (RM), then one can extend this logic with justification modals by adding the (K) and (JB). While not every such logic will have an attractive interpretation, some may, such as a relevant deontic logic satisfying the deontic analogue of (K$\Box$ ).²⁶

It would be a nice result if the addition of the axioms involving $\Box$ were a conservative extension of the underlying logic B.K, which is to say that if $\vdash _{{\textsf {{\textsf {B.KI} }} }}{{A}}$ and A does not contain $\Box$, then $\vdash _{{\textsf {{\textsf {B.K} }} }}{{A}}$. We have not, however, been able to prove this, so the problem will be left open here. Let us turn, instead, to further enrichments of the language.

5 Additional Justification Terms

Since the RME-frames have only one accessibility relation, there appears to be no hurdle to enriching the justification language with additional terms, as opposed to the RMJ-frames of Standefer (2019), which would require the addition of more accessibility relations and potentially conditions coordinating them. For this section, we will enrich Terms with the additional operators ‘!’ and ‘?’, so that if $t\in \textsf {Terms}$, then $!t\in \textsf {Terms}$ and $?t\in \textsf {Terms}$, following the work of Pacuit (2005) and Rubtsova (2006a, 2006b).²⁷ The set Terms is defined as follows.

$$\begin{aligned} t:= x \;|\; (t\cdot s)\;|\; !t \;|\; ?t \end{aligned}$$

A brief gloss on these new operations is in order. The ‘!’ operation is the positive justification checker and it is supposed to verify or check that a given justification is adequate. For example, $\llbracket !x\rrbracket \llbracket x\rrbracket p$ is a verification that the justification x of p is correct. An example, provided by Artemov and Fitting (2021), is a referee report certifying the correctness of a proof. The ‘?’ operation is the negative justification checker and it is supposed to verify that a given justification is inadequate. The language with these new terms will be $\mathbin {\mathscr {L}}^{\Box !?}$. The formal definition of the language does not change from before, although the $\llbracket t\rrbracket A$ clause permits a wider range of options for the term t.

Additional axioms are needed to obtain the desired contribution of the new terms. For the ‘!’ operator, we need the axioms

(4):

$\llbracket t\rrbracket A\rightarrow \llbracket !t\rrbracket \llbracket t\rrbracket A$, and

(4$\Box$ ):

$\Box A\rightarrow \Box \Box A$.²⁸

For the ‘?’ operator, we need the axioms

(5):

$\mathord {\sim }\llbracket t\rrbracket A\rightarrow \llbracket ?t\rrbracket \mathord {\sim }\llbracket t\rrbracket A$, and

(5$\Box$ ):

$\mathord {\sim }\Box A\rightarrow \Box \mathord {\sim }\Box A$.

For a logic with (D), the axiom to be added is (D) $\Box \mathord {\sim }A\rightarrow \mathord {\sim }\Box A$, rather than Pacuit’s axiom $\llbracket t\rrbracket \bot \rightarrow \bot$, as $\bot$ is not in the language.²⁹ There is no need to add the axiom $\llbracket t\rrbracket \mathord {\sim }A\rightarrow \mathord {\sim }\llbracket t\rrbracket A$ in addition to (D), since the latter implies the former.³⁰ For a logic with (T), we can get away with just $\Box A\rightarrow A$, as $\llbracket t\rrbracket \rightarrow A$ follows from the first axiom and (JB). The logic B.KI4 will be B.KI with the addition of both (4) and (4$\Box$ ), B.K5 the addition with both (5) and (5$\Box$ ), B.KIT with (T), and B.KID with the (D) axiom. The axioms can be combined for further logics, provided that the indicated pairs of axioms are always included. Such a logic will be named B.KIX, replacing ‘X’ with the appropriate axiom names.

The frame conditions for the !-axioms, the (D)-axioms, and the (T)-axiom are relatively straightforward. The additions for the ?-axioms will require a bit more work, so I will leave them for last.

For the !-axioms, we add the conditions

(F4A):

if Sab then ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$,

(F4B):

if $A\in {\mathcal {E}}(t,a)$, then $\llbracket t\rrbracket A\in {\mathcal {E}}(!t,a)$, and

(F4C):

if Sab and Sbc, then Sac.

The class of RME4-frames will be the RME-frames satisfying these conditions.

Lemma 17

Axioms (4) and (4$\Box$ ) are valid in the class of RME4-frames.

Proof

For the first, suppose $a\Vdash \llbracket t\rrbracket A$ but $a\not \Vdash \llbracket !t\rrbracket \llbracket t\rrbracket A$. By assumption, $A\in {\mathcal {E}}(t,a)$, so by the frame condition (F4B), $\llbracket t\rrbracket {A}\in {\mathcal {E}}(!t,a)$. So there must be a b such that Sab and $b\not \Vdash \llbracket t\rrbracket A$. Since ${A}\in {\mathcal {E}}(t,a)$, by condition (F4A), $A\in {\mathcal {E}}(t,b)$. So there must be a c such that Sbc and $c\not \Vdash A$. Then by (F4C), Sac, so $a\not \Vdash \llbracket t\rrbracket A$, which is a contradiction.

The second is valid by the usual transitivity argument, using condition (F4C). $\square$

For the (D)-axioms, we add the condition

$$\begin{aligned} {\textsf {(FD)} }\qquad \forall a\exists b(Sab^*\wedge Sa^*b). \end{aligned}$$

The class of RMED-frames will be those that satisfy the condition (FD).

Lemma 18

The (D)-axiom $\Box \mathord {\sim }A\rightarrow \mathord {\sim }\Box A$ is valid in the class of RMED-frames.

Proof

Suppose that $a\Vdash \Box \mathord {\sim }A$. Suppose that $a\not \Vdash \mathord {\sim }\Box A$. Then $a^*\Vdash \Box A$. From the verification condition for $\Box$, it follows that for all c such that $Sa^*c$, $c\Vdash A$. Let b be such that $Sab^*$ and $Sa^*b$, as given by (FD). Then $b^*\Vdash \mathord {\sim }A$ and $b\Vdash A$. The former implies $b\not \Vdash A$, which is a contradiction. $\square$

For the (T)-axiom, we add the condition that for all a,

$$\begin{aligned} {\textsf {(FT)} }\qquad Saa. \end{aligned}$$

The class of RMET-frames will be the class of frames satisfying (FT).

Lemma 19

The (T)-axiom $\Box A\rightarrow A$ is valid in the class of RMET-frames.

Proof

The proof is as usual. $\square$

That suffices for Soundness for logics with the !-axioms and the (D) and (T) axioms.

The Completeness arguments will use the same definitions from the previous section. We need to show that the canonical frame for a given logic satisfies the frame conditions.

Lemma 20

Suppose B.KIX contains the axioms (4) and (4$\Box$ ). Then the canonical frame for the logic obeys the conditions ${\textsf {(F4A)} }$, ${\textsf {(F4B)} }$, and ${\textsf {(F4C)} }$.

Proof

The proof for ${\textsf {(F4C)} }$ is the usual one, so I will omit it.

For ${\textsf {(F4A)} }$, suppose Sab and let $B\in {\mathcal {E}}(t,a)$. It follows that $\llbracket t\rrbracket B\in a$, which implies $\llbracket !t\rrbracket \llbracket t\rrbracket B$ from (4). From (JB), we have $\Box \llbracket t\rrbracket B\in a$. Then Sab implies $\llbracket t\rrbracket B\in b$, which in turn implies $B\in {\mathcal {E}}(t,b)$, as desired.

For ${\textsf {(F4B)} }$, suppose $A\in {\mathcal {E}}(t,a)$. From (4), $\llbracket !t\rrbracket \llbracket t\rrbracket A\in a$, so $\llbracket t\rrbracket A\in {\mathcal {E}}(!t,a)$. $\square$

Lemma 21

Suppose B.KIX contains the axiom (D). Then the canonical frame for the logic obeys the conditions ${\textsf {(FD)} }$.

Suppose B.KIX contains the axiom (T). Then the canonical frame for the logic obeys the conditions ${\textsf {(FT)} }$.

Proof

The proof for both claims was provided by Fuhrmann (1990). $\square$

When combined with the canonical model construction from the previous section, the preceding lemmas suffice for the Completeness of BKI4, BKID, and BKIT with respect to the appropriate class of frames. Let us now turn to the issue of the ?-axioms.

The complication arising for the ?-axioms is that they appear to require a condition on models, rather than just conditions on frames. This can be seen in the work of Pacuit (2017) and Rubtsova (2006a, 2006b), both of which use a combination of frame and model conditions. Four conditions are required. The frame conditions are

(F5A):

if $A\not \in {\mathcal {E}}(t,a^*)$ then $\mathord {\sim }\llbracket t\rrbracket A\in {\mathcal {E}}(?t,a)$, and

(F5B):

if Sab and $A\in {\mathcal {E}}(t,b^*)$ then $A\in {\mathcal {E}}(t,a^*)$, and

(F5C):

if $Sa^*c$ and Sab, then $Sb^*c$.

An RME5-frame is an RME-frame obeying these three conditions. The definition of a model on an RME5-frame needs an additional condition:

(M5):

if $A\in {\mathcal {E}}(t,a^*)$ and $Sa^*b$, then $b\Vdash A$

The definitions of holding in a model and validity will then use models on RME5-frames with the additional condition (M5). A model on an RME5-frame satisfying the condition (M5) will be a 5-model.

I will now show that the ?-axioms are valid on RME5-frames.

Lemma 22

The axioms (5) $\mathord {\sim }\llbracket t\rrbracket A\rightarrow \llbracket ?t\rrbracket \mathord {\sim }\llbracket t\rrbracket A$ and (5$\Box$ ) $\mathord {\sim }\Box A\rightarrow \Box \mathord {\sim }\Box A$ are valid on the class of RME5-frames.

Proof

Let M be an arbitrary 5-model. Suppose $a\Vdash \mathord {\sim }\llbracket t\rrbracket A$ and $a\not \Vdash \llbracket ?t\rrbracket \mathord {\sim }\llbracket t\rrbracket A$. There are two cases, either $\mathord {\sim }\llbracket t\rrbracket A\not \in {\mathcal {E}}(?t,a)$ or for some b such that Sab, $b\not \Vdash \mathord {\sim }\llbracket t\rrbracket A$. Suppose $\mathord {\sim }\llbracket t\rrbracket A\not \in {\mathcal {E}}(?t,a)$. From the inital assumption, $a^*\not \Vdash \llbracket t\rrbracket A$. There are then two subcases, $A\not \in {\mathcal {E}}(t,a^*)$ or there is a c such that $Sa^*c$ and $c\not \Vdash A$. Suppose that $A\not \in {\mathcal {E}}(t,a^*)$. By (F5A), $\mathord {\sim }\llbracket t\rrbracket A\in {\mathcal {E}}(?t,a)$, which contradicts the assumption of the case. Therefore, $A\in {\mathcal {E}}(t,a^*)$. For the second subcase, assume that there is a c such that $Sa^*c$ and $c\not \Vdash A$. From (M5), we have $c\Vdash A$, which contradicts the assumption of the subcase. Therefore, we conclude that the assumption of the case is false.

For the second case, suppose that for some b such that Sab, $b\not \Vdash \mathord {\sim }\llbracket t\rrbracket A$. Then, $b^*\Vdash \llbracket t\rrbracket A$. This implies $A\in {\mathcal {E}}(t,b^*)$. From (F5B), we have $A\in {\mathcal {E}}(t,a^*)$. From the initial assumption that $a\Vdash \mathord {\sim }\llbracket t\rrbracket A$, it follows that $a^*\not \Vdash \llbracket t\rrbracket A$. There are two subcases. The first is that $A\not \in {\mathcal {E}}(t,a^*)$. This is ruled out by the fact that $A\in {\mathcal {E}}(t,a^*)$, just established. The second subcase is that there is a c such that $Sa^*c$ and $c\not \Vdash A$. Then, by (F5C), $Sb^*c$. This implies $b^*\not \Vdash \llbracket t\rrbracket A$, contradicting the assumption of the case.

Both cases led to contradictions, so we conclude that $a\Vdash \llbracket ?t\rrbracket \mathord {\sim }\llbracket t\rrbracket A$, which suffices for the validity of (5).

The validity of (5$\Box$ ) is established by an argument similar to that of the second subcase of the second case. $\square$

For the Completeness proof, we must show that the canonical frame obeys condition (F5A), (F5B), and (F5C), and that the canonical model obeys (M5).

Lemma 23

The canonical frame for a logic B.KIX containing (5) and (5$\Box$ ) obeys (F5A).

Proof

Suppose that $A\not \in {\mathcal {E}}(t,a^*)$. Then $\llbracket t\rrbracket A\not \in a^*$, so $\mathord {\sim }\llbracket t\rrbracket A\in a$. From (5), it follows that $\llbracket ?t\rrbracket \mathord {\sim }\llbracket t\rrbracket A\in a$, so $\mathord {\sim }\llbracket t\rrbracket A\in {\mathcal {E}}(?t,a)$, as desired. $\square$

Lemma 24

The canonical frame for a logic B.KIX containing (5) and (5$\Box$ ) obeys (F5B).

Proof

Suppose that Sab, $A\in {\mathcal {E}}(t,b^*)$, but $A\not \in {\mathcal {E}}(t,a^*)$. Then $\llbracket t\rrbracket A\not \in a^*$, so $\mathord {\sim }\llbracket t\rrbracket A\in a$. From (5), it follows that $\llbracket ?t\rrbracket \mathord {\sim }\llbracket t\rrbracket A\in a$. From (JB), $\Box \mathord {\sim }\llbracket t\rrbracket A\in a$. As Sab, $\mathord {\sim }\llbracket t\rrbracket A\in b$, which implies $\llbracket t\rrbracket A\not \in b^*$. This implies $A\not \in {\mathcal {E}}(t,b^*)$, contradicting the assumption. $\square$

Lemma 25

The canonical frame for a logic B.KIX containing (5) and (5$\Box$ ) obeys (F5C).

Proof

Suppose $Sa^*c$ and Sab. Suppose $\Box B\in b^*$. Then $\mathord {\sim }\Box B\not \in b$. So, $\Box \mathord {\sim }\Box B\not \in a$, which, from (5$\Box$ ), implies $\mathord {\sim }\Box B\not \in a$. From this, we get $\Box B\in a^*$, which implies $B\in c$, which suffices for $Sb^*c$. $\square$

Putting these together yields the following.

Lemma 26

The canonical frame for a logic B.KIX containing (5) and (5$\Box$ ) is an RME5-frame.

The Truth Lemma can be established, as before, so we have an RME-model. To show that the canonical model is a 5-model, it remains to show that it satisfies (M5).

Lemma 27

The canonical model for a logic B.KIX containing (5) and (5$\Box$ ) obeys (M5).

Proof

Suppose that $A\in {\mathcal {E}}(t,a^*)$ and $Sa^*b$. The former implies $\llbracket t\rrbracket A\in a^*$. From (JB), we get $\Box A\in a^*$. Since $Sa^*b$, $A\in b$, which, by lemma 16, gives us $b\Vdash A$, as desired. $\square$

The preceding lemmas suffice for Completeness for B.KI5.

Theorem 5

If $\models _{{\textsf {B.KI5} }}{A}$, then $\vdash _{{\textsf {B.KI5} }}{{A}}$.

6 Simplified Neighborhoods

The techniques of the previous sections can be adapted to cover the neighborhood frames, RMN-frames, presented by Standefer (2019) as well.³¹ For the remainder of the paper, the term-forming operators ‘!’ and ‘?’ will be excluded from the language for simplicity, reverting to $\mathbin {\mathscr {L}}^{\Box }$. Rather than using RMN-frames, we will use a modified form, which we will call Nb-frames.

Definition 6

An Nb-frame is a sextuple $\langle K, N, R,^*, {\mathcal {E}}, {{\mathcal {N}}}, \textsf {Nb} \rangle$, where the first four components comprise an RM-frame, ${{\mathcal {N}}}: K\mapsto {\mathcal {P}}({\mathcal {P}}(K))$, $\textsf {Nb} \subseteq {\mathcal {P}}(K)$, obeying the following conditions.

• if $a\le b$, then ${{{\mathcal {N}}}(a)}\subseteq {{{\mathcal {N}}}(b)}$;

• if $a\le b$, then ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$;

• if Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$, then $B\in {\mathcal {E}}(t\cdot s,c)$;

• $\textsf {Nb} \ne \emptyset$;

• $\displaystyle \bigcup _{{a\in K}}{{{\mathcal {N}}}(a)}\subseteq \textsf {Nb}$; and

• if Rabc, then ${\hat{R}}{{{\mathcal {N}}}(a)}{{{\mathcal {N}}}(b)}{{{\mathcal {N}}}(c)}$, where for $X,Y, Z\in {\mathcal {P}}({\mathcal {P}}(K)), {\hat{R}}XYZ$ is defined as

  $$\begin{aligned} \forall U,V\in \textsf {Nb} ( \{ x\in K: \forall u,v\in K(Rxuv \wedge u\in U\Rightarrow v\in V)\}\in X\wedge U\in Y\Rightarrow V\in Z). \end{aligned}$$

Since we have a set Nb of sets of points, these frames are what (Pacuit, 2017) calls “general neighborhood” frames. These frames replace the closure conditions on the set of neighborhoods, PROP, of the RMN-frames with a simpler condition on the potential set of neighborhoods, Nb, of the Nb-frames. Although the definitions of the neighborhoods in the canonical frame in the RMN-frames and the Nb-frames are similar, the relaxed condition on the set of neighborhoods in the Nb-frames makes them easier to construct. Additionally, the Nb-frames follow the RME-frames of Sect. 4 in using an evidence function and a single modal accessibility widget, a single N function, rather than the multiple $N_{t}$ functions of the RMN-frames.

In the Nb-models, the neighborhood function N replaces the accessibility relation S of the RME-models in identifying what information is about. In the Nb-models, information in a situation concerns propositions, as codified by N, and the evidence function ${\mathcal {E}}$ says that particular pieces of justification bear on specific propositions. The use of neighborhoods then represents a shift from taking the information in a situation representing how things are in other situations to representing that particular propositions hold.

The verification condition for the modals in this setting are the following.

• $a\Vdash \llbracket t\rrbracket A$ iff $[A]\in {{{\mathcal {N}}}(a)}$ and $A\in {\mathcal {E}}(t,a)$.

• $a\Vdash \Box A$ iff $[A]\in {{{\mathcal {N}}}(a)}$.

The definitions of holding in a model and validity in a frame and class of frames are adapted in a straightforward way.

I will record a feature of the definition of ${\hat{R}}$ that is used in proving Soundness.

Lemma 28

In a Nb-model M,

$$\begin{aligned} \{ x\in K: \forall u,v\in K(Rxuv \wedge u\in [A]\Rightarrow v\in [B])\}=[A\rightarrow B]. \end{aligned}$$

The logic B.IEK is obtained by adding to the axioms and rules of B the following axioms and rule.

(K):

$\llbracket t\rrbracket (A\rightarrow B)\rightarrow (\llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B)$

(K$\Box$ ):

$\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)$

(JB):

$\llbracket t\rrbracket A\rightarrow \Box A$

(RE):

$A\leftrightarrow B\Rightarrow \Box A\leftrightarrow \Box B$

The Heredity Lemma holds for these new frames.

Lemma 29

(Heredity) If $a\le b$ and $a\Vdash A$, then $b\Vdash A$.

Proof

There are two new cases, for the modals. Suppose $a\le b$.

The first case is that A is of the form $\llbracket t\rrbracket B$. Suppose $a\Vdash \llbracket t\rrbracket B$. So, $[B]\in {{{\mathcal {N}}}(a)}$, from which it follows by the first condition on Nb-frames that $[B]\in {{{\mathcal {N}}}(b)}$. The assumption also implies $B\in {\mathcal {E}}(t,a)$. From the second condition on Nb-frames, $B\in {\mathcal {E}}(t,b)$, which suffices for $b\Vdash \llbracket t\rrbracket B$.

The second case is that A is of the form $\Box B$. Suppose $a\Vdash \Box B$. This implies $[B]\in {{{\mathcal {N}}}(a)}$. From the first condition on Nb-frames, $[B]\in {{{\mathcal {N}}}(b)}$, which implies $b\Vdash \Box B$, as desired. $\square$

Next, I will move to proving Soundness.

Lemma 30

(Soundness) If $\vdash _{{\textsf {{\textsf {B.IEK} }} }}{{A}}$, then $\models _{{\textsf {{\textsf {B.IEK} }} }}{A}$.

Proof

The new cases over the proof for Soundness for B are the axioms (K), (K$\Box$ ), (JB), and the rule (RE).

For the (K) axiom, suppose $a\Vdash \llbracket t\rrbracket (A\rightarrow B)$. To show that $a\Vdash \llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B$, suppose Rabc, $b\Vdash \llbracket s\rrbracket A$, and $c\not \Vdash \llbracket t\cdot s\rrbracket B$. There are then two cases: either $B\not \in {\mathcal {E}}(t\cdot s,c)$ or $[B]\not \in {{{\mathcal {N}}}(c)}$.

Suppose $B\not \in {\mathcal {E}}(t\cdot s,c)$. From the assumption, we have $A\rightarrow B\in {\mathcal {E}}(t,a)$, $A\in {\mathcal {E}}(s,b)$, and Rabc. With the third Nb-frame condition, these suffice for $B\in {\mathcal {E}}(t\cdot s,c)$, contradicting the assumption.

Suppose that $[B]\not \in {{{\mathcal {N}}}(c)}$. From Rabc, it follows that ${\hat{R}}{{{\mathcal {N}}}(a)}{{{\mathcal {N}}}(b)}{{{\mathcal {N}}}(c)}$. Instantiating the universal quantifiers gives

$$\begin{aligned} \{ x\in K: \forall u,v\in K(Rxuv \wedge u\in [A]\Rightarrow v\in [B])\}\in {{{\mathcal {N}}}(a)}\wedge [A]\in {{{\mathcal {N}}}(b)}\Rightarrow [B]\in {{{\mathcal {N}}}(c)}. \end{aligned}$$

By lemma 28, this is equivalent to

$$\begin{aligned}{}[A\rightarrow B]\in {{{\mathcal {N}}}(a)}\wedge [A]\in {{{\mathcal {N}}}(b)}\Rightarrow [B]\in {{{\mathcal {N}}}(c)}. \end{aligned}$$

From the assumptions, we have both $[A\rightarrow B]\in {{{\mathcal {N}}}(a)}$ and $[A]\in {{{\mathcal {N}}}(b)}$, so we have $[B]\in {{{\mathcal {N}}}(c)}$, contradicting the assumption.

Therefore, we conclude $c\Vdash \llbracket t\cdot s\rrbracket B$, which suffices for $a\Vdash \llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B$, as desired.

The argument for the validity of (K$\Box$ ) is similar to the second case of the argument for (K), so it is omitted.

For (JB), suppose $a\Vdash \llbracket t\rrbracket A$. This implies $[A]\in {{{\mathcal {N}}}(a)}$, which gives $a\Vdash \Box A$, as desired.

For the rule (RE), suppose $\models _{{\textsf {B.IEK} }}{A\leftrightarrow B}$. Suppose $a\Vdash \Box A$. This implies $[A]\in {{{\mathcal {N}}}(a)}$. From the initial assumption, $[A]=[B]$, so $[B]\in {{{\mathcal {N}}}(a)}$, which implies $a\Vdash \Box B$. The converse conditional is similar. $\square$

For Completeness, the definitions for the B.KI canonical model from Sect. 4 are carried over, substituting ‘B.EIK’ for ‘B.KI’ throughout, with the addition of the following additional definitions.

• $||A||=\{ a\in K: A\in a\}$

• $\textsf {Nb} =\{ ||A||: A\in \mathbin {\mathscr {L}}^{\Box }\}$

• ${{{\mathcal {N}}}(a)}=\{ ||A||\in \textsf {Nb} : \Box A\in a\}$

First, we note a lemma, which is important because of its corollaries.

Lemma 31

In a canonical frame for B.EIK, if $||A||\subseteq ||B||$, then $\vdash _{{\textsf {B.EIK} }}{{A\rightarrow B}}$.

Proof

Suppose $\not \vdash _{{\textsf {B.EIK} }}{{A\rightarrow B}}$. The pair $\langle \{ A\},\{ B\}\rangle$ is then B.EIK-consistent, so $\{ A\}$ can be extended to a prime theory a such that $B\not \in a$. Therefore, it is not the case that $||A||\subseteq ||B||$. $\square$

Corollary 2

If $||A||=||B||$, then $\vdash _{{\textsf {B.EIK} }}{{A\leftrightarrow B}}$.

If $||A||=||B||$, then $\vdash _{{\textsf {B.EIK} }}{{\Box A\leftrightarrow \Box B}}$.

Next, we note an important lemma for showing that the defined canonical frame obeys the Nb-frame conditions, as well as one of the cases for the Truth Lemma.

Lemma 32

If $A\rightarrow B\not \in a$, then there are b and c in K such that Rabc, $A\in b$, and $B\not \in c$.

Proof

The proof is as in Restall (2000, ch. 11). $\square$

Lemma  32 lets us prove the following.

Lemma 33

In the defined canonical frame, $||A\rightarrow B||=\{ x\in K: \forall u,v\in K(Rxuv \wedge u\in ||A||\Rightarrow v\in ||B||)\}$.

Proof

Suppose $a\in ||A\rightarrow B||$. Suppose Rabc and $b\in ||A||$. From the assumptions, $A\rightarrow B\in a$ and $A\in b$. Given that Rabc, $B\in c$, establishing one direction of the lemma.

Suppose that $a\not \in ||A\rightarrow B||$. Then $A\rightarrow B\not \in a$. From lemma 32, there are prime theories b and c such that Rabc, $A\in b$ and $B\not \in b$. So this implies $a\not \in \{ x\in K: \forall u,v\in K(Rxyz \wedge u\in ||A||\Rightarrow v\in ||B||)\}$, establishing the other direction of the lemma. $\square$

Next, we show the neighborhood functions are well-defined.

Lemma 34

If $||A||=||B||$ and $||A||\in {{{\mathcal {N}}}(a)}$, then $||B||\in {{{\mathcal {N}}}(a)}$

Proof

Suppose $||A||=||B||$ and $||A||\in {{{\mathcal {N}}}(a)}$. The latter and the definition of ${{\mathcal {N}}}$ suffice for $\Box A\in {a}$. From the former assumption and corollary 2, $\vdash _{{\textsf {B.EIK} }}{{\Box A\leftrightarrow \Box B}}$. As a is a B.EIK-theory, $\Box B\in a$, so $||B||\in {{{\mathcal {N}}}(a)}$. $\square$

It remains to verify that all the frame conditions are satisfied.

Lemma 35

In the defined canonical frame, if $a\le b$, then ${{{\mathcal {N}}}(a)}\subseteq {{{\mathcal {N}}}(b)}$.

Proof

Suppose $a\le b$ and $X\in {{{\mathcal {N}}}(a)}$. The latter implies that for some B, we have $X=||B||$, so $\Box B\in a$. The former implies $a\subseteq b$, which gives $\Box B\in b$, so $||B||\in {{{\mathcal {N}}}(b)}$. $\square$

Lemma 36

In the defined canonical frame, if $a\le b$, then ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$.

Proof

Suppose $a\le b$ and $A\in {\mathcal {E}}(t,a)$. These assumptions imply $\llbracket t\rrbracket A\in a$ and $a\subseteq b$, which give $\llbracket t\rrbracket A\in b$, and so $A\in {\mathcal {E}}(t,b)$. $\square$

Lemma 37

In the defined canonical frame, if Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$, then $B\in {\mathcal {E}}(t\cdot s,c)$.

Proof

Suppose Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$. The assumptions imply $\llbracket t\rrbracket (A\rightarrow B)\in a$ and $\llbracket s\rrbracket A\in b$. From (K) and the fact that a is a B.EIK theory, $\llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B\in a$. The assumption that Rabc then implies $\llbracket t\cdot s\rrbracket B\in c$, whence $B\in {\mathcal {E}}(t\cdot s,c)$. $\square$

Lemma 38

In the defined canonical frame, $\textsf {Nb} \ne \emptyset$.

Proof

By definition, $||p||\in \textsf {Nb}$. $\square$

Lemma 39

In the defined canonical frame, $\displaystyle \bigcup _{{a\in K}}{{{\mathcal {N}}}(a)}\subseteq \textsf {Nb}$.

Proof

Immediate from the definitions. $\square$

Lemma 40

In the defined canonical frame, if Rabc, then ${\hat{R}}{{{\mathcal {N}}}(a)}{{{\mathcal {N}}}(b)}{{{\mathcal {N}}}(c)}$.

Proof

Suppose Rabc. Suppose also that for some $U,V\in \textsf {Nb}$, we have the following: $\{ x\in K: \forall u,v\in K(Rxuv \wedge u\in U\Rightarrow v\in V)\}\in {{{\mathcal {N}}}(a)}$, and $U\in {{{\mathcal {N}}}(b)}$, but $V\not \in {{{\mathcal {N}}}(c)}$. From the definition of Nb, for some B and C, it holds that $U=||B||$ and $V=||C||$. The assumption is, then $\{ x\in K: \forall u,v\in K(Rxyz \wedge u\in ||B||\Rightarrow v\in ||C||)\}\in {{{\mathcal {N}}}(a)}$, $||B||\in {{{\mathcal {N}}}(b)}$, but $||C||\not \in {{{\mathcal {N}}}(c)}$. From lemma 33, $||B\rightarrow C||\in {{{\mathcal {N}}}(a)}$, so $\Box (B\rightarrow C)\in a$. From (K$\Box$ ), we have that $\Box B\rightarrow \Box C\in a$. From $||B||\in {{{\mathcal {N}}}(b)}$, it follows that $\Box B\in b$. Given that Rabc, it follows that $\Box C\in c$, so $||C||\in {{{\mathcal {N}}}(c)}$, contradicting the assumption. $\square$

The defined canonical frame satisfies the conditions for being an Nb-frame. The next piece is to verify the Truth Lemma.

Lemma 41

(Truth Lemma) In the defined canonical frame, $||A||=[A]$.

Proof

Most of the cases are standard, so I will present the new cases. The inductive hypothesis is that for all formulas C of complexity less than n, $||C||=[C]$.

Let A be of the form $\llbracket t\rrbracket B$. Suppose $\llbracket t\rrbracket B\in a$. Then $B\in {\mathcal {E}}(t,a)$. From (JB), $\Box B\in a$, so $||B||\in {{{\mathcal {N}}}(a)}$. From the inductive hypothesis, $||B||=[B]$, so $a\Vdash \llbracket t\rrbracket B$.

Suppose $\llbracket t\rrbracket B\not \in a$. Then $B\not \in {\mathcal {E}}(t,a)$. Therefore, $a\not \Vdash \llbracket t\rrbracket B$.

Let A be of the form $\Box B$. Suppose $\Box B\in a$. Then $||B||\in {{{\mathcal {N}}}(a)}$. By the inductive hypothesis, $||B||=[B]$, so $[B]\in {{{\mathcal {N}}}(a)}$. Therefore, $a\Vdash \Box B$.

Suppose $\Box B\not \in a$. Then $||B||\not \in {{{\mathcal {N}}}(a)}$. By the inductive hypothesis, $||B||=[B]$, so $[B]\not \in a$, whence $a\not \Vdash \Box B$. $\square$

We can then consider Completeness proved.

Theorem 6

(Completeness) If $\models _{{\textsf {B.EIK} }}{A}$, then $\vdash _{{\textsf {B.EIK} }}{{A}}$.

The Nb-frames are adequate for the logic B.EIK. In the next section, I will settle a question raised by Standefer (2019).

7 Evidence and Theories

In this section, the $\Box$ modal will drop out. The set of terms will be enriched with the binary operator ‘+’, so that the set Terms contains variables, $t\cdot s$, and $t+s$, for all terms $t,s\in \textsf {Terms}$, defined as follows.

$$\begin{aligned} t := x \;|\; (t\cdot s) \;|\; (t+s) \end{aligned}$$

The language will be $\mathbin {\mathscr {L}}^{+}$, defined as follows.

$$\begin{aligned} A:= p \;|\; \mathord {\sim }A\;|\; A\wedge B\;|\; A\vee B \;|\; A\rightarrow B \;|\; \llbracket t\rrbracket A \end{aligned}$$

This is $\mathbin {\mathscr {L}}$, with the addition of +-terms in the justification modal clause.

I will define a modification of the RME-frames, the point of which is to address a question raised by Standefer (2019). The question is whether one can obtain a Completeness result with respect to RME-frames in which the evidence sets are theories of an appropriate logic. I will supply an affirmative answer, and in doing so, I will highlight the important contribution of the $+$ operator, which has not played a role elsewhere in this paper. While this question is motivated primarily by technical concerns, the answer illuminates some of the workings of substructural modal logics and importance of theories, which are connected to the contribution of the $+$ operator.

To begin, let the logic B.RCK+ be the logic obtained from adding to the axioms and rules of B the following.

(K):

$\llbracket t\rrbracket (A\rightarrow B)\rightarrow (\llbracket s\rrbracket A\rightarrow \llbracket t\cdot s\rrbracket B)$

(+):

$\llbracket t\rrbracket A\rightarrow \llbracket t+s\rrbracket A$, $\llbracket t\rrbracket A\rightarrow \llbracket s+t\rrbracket A$

(C):

$\llbracket t\rrbracket A\wedge \llbracket t\rrbracket B\rightarrow \llbracket t\rrbracket (A\wedge B)$

(RM):

$A\rightarrow B\Rightarrow \llbracket t\rrbracket A\rightarrow \llbracket t\rrbracket B$

These axioms and rules turn each justification modal a kind of implicit commitment modal. The logic, without $+$, is what is considered by Standefer (2019). Next, I will turn to the frames.

Definition 7

Let a RMEth-frame be an RME-frame, $\langle K, N, R,^*, S, {\mathcal {E}}\rangle$, in which ${\mathcal {E}}(t,a)$ is a B.RCK+ theory, for each $t\in \textsf {Terms}$ and which obeys the condition

• ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t+s,a)$ and ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(s+t,a)$.

The definitions of model, holding, and validity are as for RME-frames, substituting ‘RMEth’ for ‘RME’. The verification conditions for the justification modals are the same as in RME-models.

I will now prove Soundness for the logic with respect to validity for RMEth-frames.

Theorem 7

If $\vdash _{{\textsf {B.RCK+} }}{{A}}$, then $\models _{{\textsf {B.RCK+} }}{A}$.

Proof

The proof is by induction on the length of a B.RCK+-proof. We assume that for all B.RCK+-proof $\pi$ of length less than $n\ge 1$, if C is the conclusion of $\pi$, then $\models _{{\textsf {B.RCK+} }}{A}$. The axiom and rule cases for the base logic are standard. The new cases are (+), (C), and (RM).

For (+), suppose $a\Vdash \llbracket t\rrbracket B$, so for all b such that Sab, $b\Vdash B$ and $B\in {\mathcal {E}}(t,a)$. From the RMEth frame condition, ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t+s,a)$. Therefore, $a\Vdash \llbracket t+s\rrbracket B$. The argument for the other (+) axiom is similar.

For (C), suppose $a\Vdash \llbracket t\rrbracket B\wedge \llbracket t\rrbracket C$. It follows that $B\in {\mathcal {E}}(t,a)$ and $C\in {\mathcal {E}}(t,a)$. Since ${\mathcal {E}}(t,a)$ is a B.RCK+-theory, $B\wedge C\in {\mathcal {E}}(t,a)$. From the assumption, for all b such that Sab, $b\Vdash B$ and $b\Vdash C$, so $b\Vdash B\wedge C$, which suffices for $a\Vdash \llbracket t\rrbracket (B\wedge C)$.

For (RM), we have $\vdash _{{\textsf {B.RCK+} }}{{B\rightarrow C}}$, so $\models _{{\textsf {B.RCK+} }}{B\rightarrow C}$ by the inductive hypothesis. Suppose that $a\Vdash \llbracket t\rrbracket B$, so for all b such that Sab, $b\Vdash B$ and also $B\in {\mathcal {E}}(t,a)$. As ${\mathcal {E}}(t,a)$ is a B.RCK+-theory and $\vdash _{{\textsf {B.RCK+} }}{{B\rightarrow C}}$, $C\in {\mathcal {E}}(t,a)$. Since $\models _{{\textsf {B.RCK+} }}{B\rightarrow C}$ and $b\Vdash B$, $b\Vdash C$, which suffices for $a\Vdash \Box C$. $\square$

For Completeness, I adapt the definitions from Sect. 3, in particular,

• Sab iff $\{ A\in \mathbin {\mathscr {L}}^{+}: \exists t\in \textsf {Terms} , \llbracket t\rrbracket A\in a\}\subseteq b$.

For a theory a, define $a^{-}=\{ A\in \mathbin {\mathscr {L}}^{+}: \exists t\in \textsf {Terms} , \llbracket t\rrbracket A\in a\}$, so the canonical binary accessibility relation holds iff $a^{-}\subseteq b$. The sets $a^{-}$ are theories, in particular B.RCK+-theories, as will be shown in the next lemma. This is in contrast with the situation with the theories b from Sect. 3, for which $b^{-}$ may fail to be a theory.

Lemma 42

Let a be a B.RCK+-theory. Then $a^{-}$ is a B.RCK+-theory.

Proof

Let a be a B.RCK+-theory. There are two things to show about $a^{-}$. For the first, suppose $\vdash _{{\textsf {B.RCK+} }}{{A\rightarrow B}}$ and $A\in a^{-}$. Then for some $t\in \textsf {Terms}$, $\llbracket t\rrbracket A\in a$. Since $\vdash _{{\textsf {B.RCK+} }}{{A\rightarrow B}}$, by (RM), $\vdash _{{\textsf {B.RCK+} }}{{\llbracket t\rrbracket A\rightarrow \llbracket t\rrbracket B}}$. Since a is a B.RCK+-theory, $\llbracket t\rrbracket B\in a$, so $B\in a^{-}$.

The second thing to show is that $a^{-}$ is closed under adjunction. Suppose $A\in a^{-}$ and $B\in a^{-}$. Then for some $t\in \textsf {Terms}$, $\llbracket t\rrbracket A\in a$ and for some $s\in \textsf {Terms}$, $\llbracket s\rrbracket B\in a$. From (+), we then have $\llbracket t+s\rrbracket A\in a$ and $\llbracket t+s\rrbracket B\in a$. Since a is a B.RCK+-theory, $\llbracket t+s\rrbracket A\wedge \llbracket t+s\rrbracket B\in a$, so from (C), $\llbracket t+s\rrbracket (A\wedge B)\in a$. Therefore, $A\wedge B\in a^{-}$, as desired. $\square$

Using this lemma, we can show that the canonical frame obeys the frame condition that was the focus of Sect. 3.

Lemma 43

The canonical frame for B.RCK+ obeys frame condition (3) of definition 4: if $\exists x(Rabx \wedge Sxc)$, then $\exists y,\exists z(Ryzc\wedge Say\wedge Sbz)$.

Proof

Suppose $\exists x(Rabx \wedge Sxc)$. Let d be such a prime B.RCK+-theory, so Rabd and Sdc. Both $a^{-}$ and $b^{-}$ are B.RCK+-theories, by lemma 42. We want to show that $a^{-}\circ b^{-}\subseteq c$. Suppose $B\rightarrow C\in a^{-}$ and $B\in b^{-}$. By definition, for some $t\in \textsf {Terms}$, $\llbracket t\rrbracket B\in a$ and for some $s\in \textsf {Terms}$, $\llbracket s\rrbracket B\in b$. From (K), $\llbracket s\rrbracket B\rightarrow \llbracket t\cdot s\rrbracket C\in a$. As Rabd, $\llbracket t\cdot s\rrbracket C\in d$, so $C\in c$, as desired. We can then use the Prime Extension Lemma to obtain prime B.RCK+-theories g and h such that $a^{-}\subseteq g$, $b^{-}\subseteq h$, and Rghc. By construction, Sag and Sbh, so $\exists y,\exists z(Ryzc\wedge Say\wedge Sbz)$, as desired. $\square$

It remains to verify that the canonical frame obeys the other RME-frame conditions in addition to the RMEth-frame conditions, with which I will start.

Lemma 44

The canonical B.RCK+-frame obeys the conditions ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t+s,a)$ and ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(s+t,a)$.

Proof

Suppose $A\in {\mathcal {E}}(t,a)$. Then $\llbracket t\rrbracket A\in a$, so from (+), $\llbracket t+s\rrbracket A\in a$, so $A\in {\mathcal {E}}(t+s,a)$. The other condition is similar. $\square$

Lemma 45

The canonical B.RCK+-frame satisfies the condition that ${\mathcal {E}}(t,a)$ is a B.RCK+-theory, for each $t\in \textsf {Terms}$.

Proof

The argument is similar to that of the proof of lemma 42. Suppose $\vdash _{{\textsf {B.RCK+} }}{{B\rightarrow C}}$ and $B\in {\mathcal {E}}(t,a)$. Then $\llbracket t\rrbracket B\in a$. From (RM), $\vdash _{{\textsf {B.RCK+} }}{{\llbracket t\rrbracket B\rightarrow \llbracket t\rrbracket C}}$, so $\llbracket t\rrbracket C\in a$. Thus $C\in {\mathcal {E}}(t,a)$, as desired.

Next, suppose $B\in {\mathcal {E}}(t,a)$ and $C{\mathcal {E}}(t,a)$. Then $\llbracket t\rrbracket B\in a$ and $\llbracket t\rrbracket C\in a$. Since a is closed under adjunction, $\llbracket t\rrbracket B\wedge \llbracket t\rrbracket C\in a$. By (C), $\llbracket t\rrbracket (B\wedge C)\in a$, so $B || C\in {\mathcal {E}}(t,a)$. Therefore, ${\mathcal {E}}(t,a)$ is a B.RCK+-theory. $\square$

Lemma 46

The canonical B.RCK+-frame satisfies the conditions

• if $a\le b$ and Sbc, then Sac, and

• if $a\le b$, then ${\mathcal {E}}(t,a)\subseteq {\mathcal {E}}(t,b)$.

Proof

For the first, suppose $a\le b$ and Sbc. Suppose that not Sac, so there is some formula $\llbracket t\rrbracket A\in a$ such that $A\not \in c$. From the definitions, $a\le b$ implies $a\subseteq b$, so $\llbracket t\rrbracket A\in b$. Therefore, $A\in c$, contradicting the assumption.

The second follows from the fact that $a\le b$ implies $a\subseteq b$. $\square$

Lemma 47

The canonical B.RCK+-frame satisfies the condition that if Rabc, $A\rightarrow B\in {\mathcal {E}}(t,a)$, and $A\in {\mathcal {E}}(s,b)$, then $B\in {\mathcal {E}}(t\cdot s,c)$.

Proof

The argument is the same as the argument for lemma 15 in Sect. 4. $\square$

That the canonical frame is an RM-frame is established in the usual ways, so the canonical frame is an RMEth-frame. The next piece of the argument is to prove the Truth Lemma.

Lemma 48

In the canonical B.RCK+-model, $A\in a$ iff $a\Vdash A$.

Proof

The new case is when A is of the form $\llbracket t\rrbracket B$. The other cases are established as usual.

Suppose $\llbracket t\rrbracket B\in a$. So, $B\in {\mathcal {E}}(t,a)$. Suppose Sab, so $a^{-}\subseteq b$, so $B\in b$. By the inductive hypothesis, $b\Vdash B$, which suffices for $a\Vdash \llbracket t\rrbracket B$.

Suppose $\llbracket t\rrbracket B\not \in a$. Then $B\not \in {\mathcal {E}}(t,a)$, so $a\not \Vdash \llbracket t\rrbracket B$. $\square$

I will then consider Completeness proved.

Lemma 49

If $\models _{{\textsf {B.RCK+} }}{A}$, then $\vdash _{{\textsf {B.RCK+} }}{{A}}$.

It is not hard to see that the logics considered by Standefer (2019), with the addition of the $+$ operator to the language along with the addition of the $+$-axioms to the logics, are complete with respect to RMEth-frames, adjusting the definitions as appropriate for base logics apart from B.³²

It is worth dwelling on the role of $+$ in the Completeness proof. With (+), (C), and (RM), the canonical frame obeys one of the conditions corresponding to the (K) axiom. The $+$ operator appears necessary, since it provides a way to unify the potentially distinct terms obtained from the suppositions in showing the set $a^{-}$ is closed under adjunction. The axiom (C) appears necessary for the argument to go through. The rule (RM) is used to show that the set $a^{-}$ is closed under provable implications. In the canonical model for B.KI, these jobs are handled by the implicit commitment modal, which obeys analogues of each of (+), (C), and (RM).

Careful attention to the proofs above indicates that requiring every set ${\mathcal {E}}(t,a)$ to be a B.RCK+-theory is more than is required. The only terms t for which we need ${\mathcal {E}}(t,a)$ to be a theory are those of the form $s+s'$. If (C) and (RM) are restricted to terms of that form, then the Soundness and Completeness arguments will still go through for the restricted frames. These frames are not particularly natural, but it is worth mentioning them, since they give a sense of the extent to which the logic can be pared back while still providing resources enough for the canonical model proof.

8 Conclusions

At the outset of this paper, we noted that there were two approaches to combining the machinery of justification logic with that of relevant logics, the approach of Standefer (2019) and the approach of Savić and Studer (2019). Both depart from the classical verification conditions for the explicit justification modals, and, as we have shown in this paper, in the basic language justification language, the canonical frame will not satisfy the required frame conditions without such a departure. We showed that the addition of an implicit commitment operator permits one to keep the more familiar verification condition for the explicit justification modals while securing Completeness. This shows how to recover aspects of the more standard approach to justification modals, in particular the rejection of (RM) for them, enabling them to keep their hyperintensional features. Given the explicit justification modals, the addition of an implicit commitment operator is fairly natural, with a bridging axiom connecting the two. While the use of the implicit commitment operator is a departure from the standard justification logical machinery, it does enable the explicit modals to behave in a more justifiation-logically orthodox fashion, albeit not yet enabling the sorts of results obtained by Savić and Studer.

Further, some of the standard extensions of the explicit justification language, with the positive and negative checker operations, can be assimilated to the present framework without issue. This provides rich languages for representing epistemic scenarios, along the lines of Artemov (2008). As demonstrated by Savić and Studer (2019), in the context of substructural logics, there are further term-forming operators one might want to consider, such as their ${\tilde{\wedge }}$ operation, used to produce a conjunctive justification for $A\wedge B$, given justifications for each conjunct. For logics weaker than R, additional term-forming operators could be added to accommodate the use of the additional rules of those logics.³³ These would be useful for representing further structure of evidence.

In the context of relevant logics, it is natural to consider the theories obtained from some claims concerning evidence, to trace out their consequences. The B.K-theory of, say, $\llbracket x\rrbracket (p\rightarrow q)$ and $\llbracket y\rrbracket p$ will differ greatly from its R.K-theory, with, for example, the former but not the latter lacking $\llbracket x\cdot y\rrbracket q$. This suggests that one may want to consider an additional conjunctive form of the (K) axiom, particularly in the context of weaker substructural logics.³⁴ Further exploration of this idea will be left for future work.