Getting some (non-classical) closure with justification logic

Abstract

Justification logics provide frameworks for studying the fine structure of evidence and justification. Traditionally, these logics do not impose any closure requirements on justification. In this paper, we argue that for some applications they should subject justification to closure under some variety of logical consequence. Specifically, we argue, building on ideas from Beall, that the non-classical logic $\mathsf {FDE}$ offers a particularly attractive notion of consequence for this purpose and define a justification logic where justification is closed under $\mathsf {FDE}$ consequence. We show the resulting logic to be sound and complete. Lastly, we discuss how the closure of justification under $\mathsf {FDE}$ contrasts closure under related non-classical logics and how our approach contrasts with some alternatives.

1 Introduction

How should a computer think? In seminal work, Nuel Belnap (1977a; b) suggested that the four-valued logic of first-degree entailment ($\mathsf {FDE}$) provides a good logic for drawing inferences from a database of information that may be incomplete  or inconsistent.¹ Belnap’s idea was that one can give an epistemic interpretation to the semantic values of $\mathsf {FDE}$, namely 1, 0, b, n, corresponding to what a database, or computer, has been told by different sources. To explain, suppose that information sources supply a computer with their verdicts about different formulas. When a source tells the computer a formula is true, ‘t’ is transcribed in the database entry for that formula. When it says a formula is false, ‘f’ is transcribed. Since the database may contain judgments from different sources, it is possible for an entry in the database to include conflicting judgments of both t and f. Nothing at all is written in entries for formulas not reported on. These four possibilities for the contents of the entry for a given formula—$\{t\}$, $\{f\}$, $\{t,f\}$, $\emptyset$—correspond to the four semantic values of $\mathsf {FDE}$. A formula receives 1 or 0, respectively, when its entry is $\{t\}$ or $\{f\}$. It receives the value b(oth) when its entry is $\{t,f\}$. And, it receives n(either) when its entry is $\emptyset$. With this understanding in place, the logic $\mathsf {FDE}$ provides a good notion of consequence for a computer to be able to extract consequences from a database containing inconsistent or incomplete information while retaining the ability to say that some things do not follow from it.²

Perhaps that’s how a computer should think about judgments stored in a single database that does not also include information about the sources of those judgments. But, a computer may have information stored across a few different databases, or in a single database with information about the sources of each stored judgment. This prompts the question of whether Belnap’s idea can extend to these cases. While there are a number of different ways to address this question, we will pursue one promising option using the tools of justification logic to provide a fine-grained way of tracking information derived from different databases or sources.³ This requires strengthening justification logic and modifying its models. As we will see, these modifications are further motivated on broader philosophical grounds.

The formal development of justification logic originates in the work of Sergie Artemov (1994, 1995) on the logic of proofs.⁴ Artemov’s idea was to enrich modal provability logic with a class of justification terms ($s,t,\ldots$) that serve to name individual arithmetical proofs in its modalities.⁵ Earlier modal logics of provability include modalities of the form ‘$\mathsf {Prv}(A)$’ and assigned the reading ‘A is provable’. Of course, to say that something is provable is to commit to the existential claim that there exists some proof of it. Thus, the justification terms in the logic of proofs supply the expressive power for us to cite witnesses for these implicit existentials so that the modality ‘$\llbracket {t}\rrbracket A$’ is read ‘t is a proof of A’. As will be evident shortly, these modalities are non-normal and create hyperintensional contexts whose particular treatment has important philosophical consequences. The general purpose epistemic models for the logic of proofs were developed later by Melvin Fitting (2005). Fitting’s models extend the standard Kripke models for modal logics with an evidence function adapted from the earlier models provided by Mkrtychev (1997). This function specifies, for each world and term, an evidence set comprised of the formulas justified by that term at that world. Although the evidence function is crucial to securing the non-normality and hyperintensionality of justification logic, it is subject to surprisingly sparse constraints. As we will discuss, this may be plausible for a logic of proofs but is inadequate for certain other applications.

The basic apparatus of justification logic provides an excellent framework to model finely individuated sources of evidence and justification, such as proofs. That application requires a strongly hyperintensional account of justification capable of distinguishing between, e.g., any two classical tautologies,⁶ At the other end of the spectrum, one might consider a weaker notion of justification according to which a claim is justified by some evidence if it follows classically from the evidence. This weak notion does not distinguish between any classical tautologies and, thus, evidence for one would justify every classical tautology. This washes out much of the important texture of justification. We will argue that there are interesting intermediate notions of justification between these two—one that is not as fine-grained as may be found in the basic justification logic models yet not as permissive as the weak notion just described. These intermediate notions can be modeled using the tools of justification logic by imposing some closure conditions on its evidence sets. Our focus in this paper will be on applications aiming to model certain varieties of epistemic justification. The most natural target in the vicinity is propositional justification as explored by epistemological internalists; however, as we will discuss in the next section, much of what we say is relevant to doxastic justification modulo certain idealisations on agents.

The largely unconstrained models for justification logic developed by Fitting fail to establish a number of intuitively plausible and widely accepted properties of justification. This is because in justification logic the fact that t justifies A entails nothing about what else is justified by t. While closure under classical consequence is clearly far too demanding, it is widely accepted that evidence is subject to some closure conditions.⁷ As such, realising the often cited ambition to use justification logic in a more general epistemic setting requires more tightly constrained models that impose certain (limited) closure conditions. However, some care is needed here, since many of the obvious candidates would rob justification logic of its most desirable features. We will aim to walk a fine line between enriching the treatment of evidence, while retaining the logic’s distinctive behaviour. To this end, we will argue that evidence sets should be closed under $\mathsf {FDE}$ in logics for epistemic justification. The result will be a logic of justification that relies on both classical and non-classical consequence to yield a compelling and well-motivated model of epistemic justification.⁸

The choice of $\mathsf {FDE}$ to use for closure of evidence is further motivated by the philosophy of logic of Jc Beall. Beall (2017; 2018) has compellingly argued that $\mathsf {FDE}$ is the universal closure relation on theories. Evidence, or justification, is, we think, naturally understood as a theory, rather than just an arbitrary collection of principles. We can view the evidence sets in Fitting models as providing the basic axioms of a theory, the consequences of which are elaborated by closure under $\mathsf {FDE}$ consequence. $\mathsf {FDE}$ consequence is fairly weak, and it only provides consequences that obtain in virtue of the logical form of the axioms, without involving their non-logical content. One can, of course, consider models that include consequences involving non-logical content, but Beall’s view provides good reason for using $\mathsf {FDE}$ as a logical starting point. In the final section of this paper, we will consider some stronger candidate logics and show that they do not share the nice features of $\mathsf {FDE}$.

We begin by introducing our target varieties of epistemic justification in Sect. 2. Then in Sect. 3, we briefly summarise the pertinent details of justification logics. We return in Sect. 4 to explain issues relating to the introduction of different closure requirements in justification logic and why some of the obvious candidates will not do. The formal details of our proposal will be provided in Sect. 5, where we introduce the new system of justification logic, $\mathsf {J}_{\mathsf {FDE}}$, which uses tools from the study of non-classical logic in its closure requirement. Additionally, we construct the Hilbert-style system $\mathsf {HJ}_{\mathsf {FDE}}{}$ for the logic $\mathsf {J}_{\mathsf {FDE}}{}$ and establish soundness and completeness. Finally, we conclude in Sect. 6 by exploring some of the noteworthy features of the proposed logic and some related logics.

2 Varieties of epistemic justification

Shortly after Artemov’s first work on the logic of proofs, Johan van Benthem (1991)⁹ suggested that epistemic logic would benefit from the introduction of an explicit representation of justification. There is a striking disconnect between the emphasis given to justification as a necessary condition for knowledge by mainstream epistemologists and the complete lack of discussion that justification has received from epistemic logicians. To wit, he suggested that epistemic logic “seems hampered by the absence of any systematic way of bringing out the justifications underlying our knowledge as first-class citizens” (van Benthem 1991, 9–10). The proposal he sketches was to conservatively extend epistemic logic with devices to cite the justifications that ground particular pieces of knowledge. In parallel to the motivation we saw in the previous section for the logic of proofs, van Bentham observed that since justification is a necessary component of knowledge, knowledge claims carry an implicit commitment to the existence of some justification. Thus, the standard reading of ‘S knows that p’ for the epistemic modality ‘Kp’ can be replaced by the conceptually equivalent gloss ‘S knows that p on the basis of some justification’. In this light, justification logic can be interpreted as an epistemic logic that explicitly cites witnesses for the existential commitments to justification that are implicit in ordinary knowledge claims where ‘$\llbracket {t}\rrbracket p$’ is read ‘S knows that p on the basis of t’.

A different route—indeed, the one that we will pursue—is to first define a separate logic of epistemic justification that could later be used in the construction of a richer epistemic logic.¹⁰ To this end, we will give our modalities the reading ‘For S, t is justification for p’. To clarify the precise meaning of this gloss, we will need to take a brief detour to rehearse the distinction between two familiar varieties of epistemic justification.

In the dispute between internalists and externalists about knowledge, much is made of the distinction between doxastic justification and propositional justification.¹¹ The distinction itself, however, is not a partisan one and, as such, we freely make use of the distinction without taking sides in the debate. To understand the difference between these two types of justification, observe that the claim that one has a justified belief that p could be understood in two ways. On the one hand, it could mean that their belief that p is held on the basis of some sufficient justification for p. Here, we say that their belief is doxastically justified. On the other hand, it could mean simply that there exists some sufficient justification for p. Under this understanding, we say that their belief is propositionally justified. The crucial differences are that doxastic justification—unlike propositional justification—depends on the structure of the agent’s attitudinal state. Firstly, belief in a proposition is required for an agent to have doxastic justification for that proposition; and, second, that belief must be based on the salient justification.¹²

With this distinction in hand, we may now clarify the reading we assigned to the modalities in a logic of epistemic justification. We will return in Sect. 4 to discuss the merits of these two interpretations and defend our claim that they require certain closure requirements. Recall that we proposed that ‘$\llbracket {t}\rrbracket p$’ should be read ‘For S, t is justification for p’. When understood an attribution of doxastic justification, this implies that S accepts that t is justification for p. The important point here is that the agent must stand in some special attitudinal relationship to the justificatory relationship that holds between t and p as mentioned above. By contrast, there is no such requirement in place for a logic of propositional justification. This is because our target is the internal structural properties of justifications rather than anything dependent on how the agent regards them. Reference to the agent is still included in the intuitive parse, since there are good reasons to think that justification is not an objective, agent-independent matter and instead depends on contextual features ( e.g. on the agent’s total evidence). Nonetheless, the point here is that the determination of whether t is propositional justification for p relies only on the conceptual nature of justification rather than whether they have the propositional attitude toward that justification necessary for doxastic justification.

3 Justification logics

To make things more concrete, we begin by presenting the language $\mathcal {L}$ of propositional justification logic along with the Fitting models used to interpret its logic. The signature of $\mathcal {L}$ includes a set of justification terms, $\mathsf {Term}$, constructed by closing a countable set of variables, $\{x_1,x_2,\ldots \}$, and constants, $\{c_1,c_2,\ldots \}$, under a binary dot operation $(\cdot )$. In service of simplicity, our language only contains the operations on terms necessary for present purposes and lacks several of the operations commonly included.¹³ In Backus-Naur form, we define the set $\mathsf{Term}$ using the rule

$$\begin{aligned} t {::}= x \;|\; c \;|\; t\cdot t' \end{aligned}$$

where x is any variable and c is any constant. Letting $\mathsf{At}$ be a countable set of atomic formulas, we define the set of formulas of $\mathcal {L}$ in the usual way by the rule

$$ \begin{aligned} A {::}= p \;|\; \mathord {\sim }A \;|\; A\, \& \, A' \;|\; A\vee A' \;|\; A\mathbin {\supset }A' \;|\; \llbracket t \rrbracket A \end{aligned}$$

where $p\in \mathsf{At}$ and $t\in \mathsf{Term}$. The logical connectives receive their ordinary readings and the modality is given the reading ‘For S, t is justification for A’ as previously discussed.

The Fitting models used to interpret formulas of $\mathcal {L}$ are quadruple, $\mathcal {M}=\langle W, R, \mathcal {E}, V \rangle$, where W is some (non-empty) set of worlds, $R\subseteq W\times W$ is an accessibility relation, $\mathcal {E}:W\times {\mathsf {Term}}\mapsto \wp \mathcal {L}$ is the evidence function mentioned above, while $V:W\mapsto \wp \mathsf{At}$ is a valuation function for the atomic formulas. The crucial element of Fitting models is its evidence function, which assigns an evidence set, $\mathcal {E}(w,t)$, to each pair consisting of a world w and justification term t. Intuitively, $\mathcal {E}(w,t)$ contains the propositions for which t is justification at w. Evidence functions are only subject to the single condition provided below.¹⁴

${\mathsf {Application}}$:

If $A\mathbin {\supset }B\in \mathcal {E}(w,t)$ and $A\in \mathcal {E}(w,s)$, then $B\in \mathcal {E}(w,t\cdot s)$

This condition requires that whenever both a material conditional and its antecedent are in the evidence sets assigned to t and s at some world, respectively, its consequent is in the evidence set of $t\cdot s$ at that same world.

The truth conditions for the classical connectives are as usual, while the semantic clause for the modal formulas is given below.

$$\begin{aligned} \mathcal {M}, w\mathbin {\Vdash }\llbracket t \rrbracket A \;\text { iff }\; \forall u(\text {If } wRu \text { then } \mathcal {M},u\mathbin {\Vdash }A) \text { and } A\in \mathcal {E}(w,t) \end{aligned}$$

As we can see, this adds the condition that A is in the evidence set assigned to t at the world of evaluation to the familiar requirement that A is true in all accessible worlds. Readers versed in awareness logic, as introduced by Fagin and Halpern (1985, 1988), may find this semantic clause familiar. Awareness logic was developed to provide an epistemic logic for explicit belief capable of avoiding the classic problem of logical omniscience from Hintikka (1975). That is, to avoid requiring that belief is closed under logical consequence, the semantic clause for the epistemic modalities depends on the assignments of an awareness function that works in much the same way as the evidence function. The non-normality of awareness logic’s epistemic operators needed to avoid logical omniscience follows from the further syntactic restriction provided by its awareness function. Indeed, one widely advertised virtue of justification logic is its similar capacity to restrict logical omniscience.

4 Getting some closure

In the previous section, we introduced the ${\mathsf {Application}}$ condition imposed on the evidence function. This condition is needed to guarantee the validity of justification logic’s characteristic axiom:

$$\begin{aligned} \llbracket t \rrbracket (A\mathbin {\supset }B)\mathbin {\supset }(\llbracket s \rrbracket A\mathbin {\supset }\llbracket {t\cdot s} \rrbracket B). \end{aligned}$$

This variant of the familiar $\mathsf {K}{}$ axiom from normal modal logics imposes a certain (albeit restricted) type of closure on justifications: the fact that a material conditional and its antecedent each have some justification, say t and s respectively, implies that its consequent has some justification, namely $t\cdot s$. So, justification is transmitted in a limited fashion through material implication via the dot product of justifications of premises. Nonetheless, when considered individually, evidence sets remain entirely unconstrained—the fact that A is a member of $\mathcal {E}(w,t)$ implies nothing else about what $\mathcal {E}(w,t)$ contains.

To see this, observe that it is possible that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$, but neither $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\, \& \, p)$ nor $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\vee q)$. Still further, it could be the case that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$ without there being any constant s such that either $\mathcal {M},w\mathbin {\Vdash }\llbracket s \rrbracket (p\, \& \, p)$ or $\mathcal {M},w\mathbin {\Vdash }\llbracket s \rrbracket (p\vee q)$. Although these latter possibilities may be ruled out by requiring that all truth-functional tautologies have some justification, that approach will fall short of ensuring that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$ implies $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\, \& \, p)$.¹⁵ It will only guarantee, for example, that $\mathcal {M},w\mathbin {\Vdash }\llbracket {s\cdot t} \rrbracket (p\, \& \, p)$ for some s that is a justification of the truth-functional tautology $p\mathbin {\supset }(p\, \& \, p)$ and, similarly, that $\mathcal {M},w\mathbin {\Vdash }\llbracket {s'\cdot t} \rrbracket (p\vee q)$ for some $s'$ that is a justification for the truth-functional tautology $p\mathbin {\supset }(p\vee q)$. Alternatively, we could adopt the most liberal assignment of evidence sets to justification constant so that every justification term justifies every truth-functional tautology.¹⁶ This would suffice to guarantee that $\llbracket t \rrbracket p$ implies both $\llbracket {t\cdot t} \rrbracket (p\, \& \, p)$ and $\llbracket {t\cdot t} \rrbracket (p\vee q)$. It may then seem plausible that we require that t be understood as equivalent to $t\cdot t$, which would give us the desired result that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$ implies $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\, \& \, p)$. However, the cost of this maneuver would be too great for our purposes. Requiring that every truth-functional tautology is justified by every justification constant strips the logic of its ability to distinguish between and keep track of different justifications.

When taken as models for arithmetic provability, as in Artemov’s logic of proofs, this failure of closure is appropriate. Under a standard definition, an axiomatic Hilbert proof is a sequence of formulas, each of which is either an axiom or follows from earlier items in the sequence by one of the rules. To check whether such a sequence is a proof of A, it suffices to confirm that A is the final formula in the sequence. Thus, there is a bright line between a proof of A and a proof of $A\, \& \, A$. The existence of the former may entail the existence of the latter, but that falls short (if only by one step) of the former being the latter. One could loosen the definition of proof slightly, permitting a sequence to count as a proof of any formula appearing anywhere in the sequence, rather than in terminal position. Even with this more permissive definition, although a proof of A may sometimes be a proof of $A\, \& \, A$, a proof of A would not in general be a proof of $A\, \& \, A$. Again, it would be inappropriate to close evidence sets under logical consequence.¹⁷

Let us now turn to consider how things fare under the epistemic interpretations introduced in the previous section. The formal apparatus does not change with a change to the philosophical interpretation. As before, evidence sets are only subject to the closure principle on their evidence function provided by ${\mathsf {Application}}$. This may be plausible for some of these applications. For instance, this seems apt if our target is doxastic justification for non-ideal agents. Recall that doxastic justification requires that the agent stands in the necessary attitudinal relation to the justification so that (possibly among other things) it must be that the agent accepts t as justification for A. Under this interpretation, the satisfaction of the modal formulas is subject to facts about the agent’s mental states. Realistic agents often fall short of holding the explicit attitudes required of idealised unboundedly rational agents due to computational bounds or a simple failure to draw out all (or even very many) consequences of claims that they accept.¹⁸ Such agents are appropriately captured by models with minimally constrained evidence sets.¹⁹ There are then some epistemic interpretations of justification logic where it is appropriate to admit nearly arbitrary evidence sets: when our target is doxastic justification for non-ideal agents. But, there are others for which this simply will not do.

For instance, suppose that we are building a logic of propositional justification. As previously discussed, propositional justification (unlike doxastic justification) is obtained independently of whether the agent is aware of it. So, even if we are dealing with non-ideal agents, the agent’s failure to explicitly accept an available justification for a proposition poses no threat to its standing. Alternatively, we may be interested in a logic of doxastic justification for heavily idealised agents for whom doxastic and propositional justification coincide. As we will now argue, adopting either of these interpretations requires imposing some closure requirements on evidence sets.

Suppose that t is justification for p at world w—model-theoretically, $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$. Since nothing further than justifying p is required to justify $p\, \& \, p$, it should then be the case that t is justification for the conjunction, $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\, \& \, p)$. However, as we have seen, this inference is invalid in the traditional models. Similarly, it is plausible that if t is justification for p, then it also justifies any logically weaker entailment of p,²⁰ That is, for example, $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$ should imply that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\vee q)$, but, as before, this inference remains invalid.²¹ Similar examples can be multiplied. These considerations suggest that evidence sets should be subject to some closure conditions, but do not settle which would be appropriate.

What happens if we were to close evidence sets under classical logical consequence? This would have the unfortunate effect of turning the modalities into normal modal operators obeying the rule of necessitation and satisfying the usual $\mathsf {K}{}$ axiom of modal logics, i.e. it would validate $\llbracket t \rrbracket (A\mathbin {\supset }B)\mathbin {\supset }(\llbracket t \rrbracket A\mathbin {\supset }\llbracket t \rrbracket B)$. Necessitation licenses the modalisation of any theorem, while the $\mathsf {K}{}$ axiom distributes a necessity modality over the material conditional. The cost here is the same as the one we saw earlier for requiring both that every justification term justifies every truth-functional tautology and that every justification term t is equivalent to $t\cdot t$. Specifically, we would be saddled with the untoward consequence that both of the following two conditions are satisfied: (i) every evidence sets would contain every theorem, and (ii) $A\in \mathcal {E}(w,t)$ and $A\supset B\in \mathcal {E}(w,t)$ would imply $B\in \mathcal {E}(w,t)$. By satisfying these conditions, justification logic would lose its distinctive ability to avoid imposing logical omniscience. For some interpretations of the modality, logical omniscience is too heavy-handed an idealization. For example, when they have epistemic content, it requires that agents know every tautology and every logical consequence of their knowledge.²² As Artemov and Kuznets (2009) observe, it is implausible to require that agents know every complex tautology and that knowledge of the rules of chess should imply knowledge of whether there exists a winning strategy for White.²³ This also seems to be too strong a requirement for some interpretations of the justification modalities. This is obviously the case for interpretations sensitive to the possibly bounded rationality of agents, such as those discussed above.

A second related downside of closing evidence sets under classical logical consequence is found in the loss of hyperintensionality. Indeed, the hyperintensionality of justification operators is one of its more attractive features. Closing evidence sets under classical consequence flattens much of the structure of justifications and washes out much of the hyperintensionality. In particular, it prevents different justification terms from distinguishing distinct tautologies or distinct contradictions. It is here that the tension lies. Our challenge then is to establish appropriate conditions under which a specific justification for a formula transmits to related formulas without spreading it to all classical consequences. Justification logic should, it seems, naturally accommodate these sorts of considerations. But, doing so requires isolating some appropriate class of models short of the class of all Fitting models. We think that bringing in some insights from Beall’s philosophy of logic is the way to respond to this challenge. Beall argues that ${\mathsf {FDE}}$ is the universal logic of theory closure, and, as such, it provides a compelling option for generating consequences of one’s evidence. In the next section, we will utilize tools from non-classical logics to make good on our claims.

5 Getting some non-classical closure

To provide a precise specification of our proposal, we will need to introduce some additional logical apparatus. We begin with some definitions: first, for a given logic L, let $\models _L$ be the relation of L-logical consequence. Next, say that a set of formulas X is an L-theory just in case (i) if $A\in X$ and $B\in X$, then $A\, \& \, B\in X$, and (ii) if $A\models _L B$ and $A\in X$, then $B\in X$. So, an L-theory is any set of formulas that is closed under adjunction and L-logical consequence.

We will focus on the case where our chosen L is the logic ${\mathsf {FDE}}$.²⁴ Valuations for ${\mathsf {FDE}}$ are simple four-valued extensions of classical valuations. Because we have dropped the assumption that each formula must have exactly one of the two standard truth values—1 or 0—the semantic clauses of formulas in ${\mathsf {FDE}}$ require separate conditions for each. For the conjunction, we have the following two conditions:

$$ \begin{aligned} A\, \& \, B\text { has value }t&\text { iff }A\text { has value }t\text { and }B\text { has value }t\\ A\, \& \, B\text { has value }f&\text { iff }A\text { has value }f\text { or }B\text { has value }f \end{aligned}$$

Similarly, the following two conditions suffice to define disjunction:

$$\begin{aligned} A\vee B\text { has value }t&\text { iff }A\text { has value }t\text { or }B\text { has value }t\\ A\vee B\text { has value }f&\text { iff }A\text { has value }f\text { and }B\text { has value }f \end{aligned}$$

These conditions generate the truth-tables for the connectives in ${\mathsf {FDE}}$ provided below.

In ${\mathsf {FDE}}$, B is a logical consequence of a set of formulas X, $X\models _{\mathsf {FDE}} B$, iff for all valuations v, if $v(A)\in \{1,b\}$, for each $A\in X$, then $v(B)\in \{1,b\}$. One notable feature of ${\mathsf {FDE}}$ is that despite not having any tautologies, its consequence relation remains rich and in many ways similar to classical consequence. For instance, we retain the inferences licensed by the usual de Morgan laws, distribution laws, and double negation introduction and elimination, as well as disjunction and conjunction normal form properties.

With these basic definitions in place, we proceed to our proposal. As we have seen, the minimal constraints imposed on evidence functions in Fitting models lead to the problematic consequence that nearly arbitrary sets may stand as evidence sets. Our proposed remedy for this shortcoming is to adopt the following further condition that evidence sets are ${\mathsf {FDE}}$-theories.

${\mathsf {FDE-Closure}}$:

If $X\subseteq \mathcal {E}(w,t)$ and $X\models _{\mathsf {FDE}} B$, then $B\in \mathcal {E}(w,t)$.

Let $\mathcal {F}$ be the class of all Fitting models satisfying the constraint above (as well as the ${\mathsf {Application}}$ constraint introduced earlier). The definition of validity for the justification logic is kept the same, namely truth in all worlds in all models in $\mathcal {F}$. The justification logic over $\mathcal {F}$ will be the class of all validities, which we will call $\mathsf {J}_{\mathsf {FDE}}$. There are further conditions that one may consider placing on the models. For example, one could require that evidence sets be prime ${\mathsf {FDE}}$-theories, where a theory X is prime just in case $A\vee B\in X$ only if either $A\in X$ or $B\in X$.

${\mathsf {Primeness}}$:

$A\vee B\in \mathcal {E}(w,t)$ only if either $A\in \mathcal {E}(w,t)$ or $B\in \mathcal {E}(w,t)$.

While this condition is sometimes useful for obtaining certain meta-theoretic results, it is not plausible as a general condition for our purposes. After all, it seems reasonable that evidence for a disjunction need not be evidence for either disjunct. That the lamp does not turn on when the button is pushed is evidence that either the bulb is out or that the lamp is not plugged in, without providing more specific evidence regarding one or the other disjunct. It is worth noting that, even if adopted, the condition does not have the undesirable consequence that justification distributes over disjunction. That is to say, $\llbracket t \rrbracket (p\vee q)\mathbin {\supset }(\llbracket t \rrbracket p\vee \llbracket t \rrbracket q)$ is invalid even if we consider only models which satisfy ${\mathsf {Primeness}}$. To see this, let $\theta _p=\{A: p\models _{\mathsf {FDE}}A\}$, namely the $\subseteq$-least prime $\mathsf {FDE}$-theory containing p. By $\mathsf {FDE}$-closure, $p\vee q\in \theta _p$. Take a model $\mathcal {M}$ with $W=\{x,y,z\}$, with $\mathcal {E}(x,t)=\theta _p$, xRy and xRz, with $V(x,p)=V(x,q)=0$, $V(y,p)=V(z,q)=0$, and $V(z,p)=V(y,q)=1$. Further specification of the evidence function is not needed for the example. As desired, this gives us $\mathcal {M}, x\mathbin {\Vdash }\llbracket t \rrbracket (p\vee q)$ but $\mathcal {M}, x\mathrel {\not \Vdash }\llbracket t \rrbracket p\vee \llbracket t \rrbracket q$. For this counterexample, it is important to note that the evidence function is not doing any important work, which is handled entirely by the modal aspect of the justification terms. Depending on the application, ${\mathsf {Primeness}}$ may be adopted, or not, so we will not let it delay us further.

Instead, we turn to some of the more technical aspects of our proposal and construct the Hilbert-style system $\mathsf {HJ}_{\mathsf {FDE}}{}$ that we show is sound and complete for $\mathsf {J}_{\mathsf {FDE}}$. Readers who are less interested in these more technical points may proceed without loss in continuity to the next section for discussion of our proposal. The axiom system $\mathsf {HJ}_{\mathsf {FDE}}{}$ has the following axioms and rules, where $A{\succ }_{\mathsf {FDE}}B$ means that sequent is derivable in the proof system for $\mathsf {FDE}$ subsequently characterised.

(A1):

All classical tautologies

(A2):

$\llbracket t \rrbracket (A\mathbin {\supset }B)\mathbin {\supset }(\llbracket s \rrbracket A\mathbin {\supset }\llbracket {t\cdot s} \rrbracket B)$

(A3):

From A and $A\mathbin {\supset }B$ to infer B

(A4):

From $A {\succ }_{\mathsf {FDE}} B$ to infer $\llbracket t \rrbracket A\mathbin {\supset }\llbracket t \rrbracket B$

(A5):

$\llbracket t \rrbracket A\, \& \,\llbracket t \rrbracket B\mathbin {\supset }\llbracket t \rrbracket (A\, \& \, B)$

We now define the sequent-based proof system for ${\mathsf {FDE}}$. This system includes the axiom sequents (B1)–(B6) and rules (C1)–(C5) provided below.

(B1):

$A {\succ }_{\mathsf {FDE}} A$

(B2):

$A\, \& \, B {\succ }_{\mathsf {FDE}} A$,   $A\, \& \, B{\succ }_{\mathsf {FDE}} B$

(B3):

$A {\succ }_{\mathsf {FDE}} A\vee B$,   $B {\succ }_{\mathsf {FDE}} A\vee B$

(B4):

$A\, \& \,(B\vee C) {\succ }_{\mathsf {FDE}} (A\, \& \, B)\vee C$

(B5):

${\mathord {\sim }A} {\succ }_{\mathsf {FDE}} {A\mathbin {\supset }B}$,   ${B} {\succ }_{\mathsf {FDE}} {A\mathbin {\supset }B}$

(B6):

${\mathord {\sim }\mathord {\sim }A} {\succ }_{\mathsf {FDE}} {A}$,   ${A} {\succ }_{\mathsf {FDE}} {\mathord {\sim }\mathord {\sim }A}$

(C1):

From $A {\succ }_{\mathsf {FDE}} B$ and ${B} {\succ }_{\mathsf {FDE}} {C}$ to infer ${A} {\succ }_{\mathsf {FDE}} {C}$

(C2):

From $A {\succ }_{\mathsf {FDE}} B$ and ${A} {\succ }_{\mathsf {FDE}} {C}$ to infer ${A} {\succ }_{\mathsf {FDE}} {B\, \& \, C}$

(C3):

From ${A} {\succ }_{\mathsf {FDE}} {C}$ and ${B} {\succ }_{\mathsf {FDE}} {C}$ to infer ${A\vee B } {\succ }_{\mathsf {FDE}} {C}$

(C4):

From ${\mathord {\sim }A} {\succ }_{\mathsf {FDE}} {C}$ and ${B}{\succ }_{\mathsf {FDE}}{C}$ to infer ${A\mathbin {\supset }B} {\succ }_{\mathsf {FDE}} {C}$

(C5):

From $A {\succ }_{\mathsf {FDE}} B$ to infer ${\mathord {\sim }B } {\succ }_{\mathsf {FDE}} {\mathord {\sim }A}$

Observe that this system is equivalent to one that replaced both (A4) and the proof system for ${\mathsf {FDE}}$ with additional axioms capturing ${\mathsf {FDE}}$-consequence inside the scope of the modality. However, this option is less attractive to us as it would provide less clarity about what is going on and, thus, we choose to leave it aside. In the remainder of this section, we sketch the proofs of soundness and completeness for $\mathsf {HJ}_{\mathsf {FDE}}{}$ with respect to the class of Fitting models whose evidence sets are ${\mathsf {FDE}}$-theories.

We start with some definitions. Let a generalized atom be any formula that is a member of At or whose main connective is a modal. We modify the definition of $\models _{\mathsf {FDE}}$ from earlier to incorporate generalized atoms. A valuation v is a function from the set of generalized atoms to the set $\{1,0, b, n\}$ that obeys the truth-tables from earlier. B is a logical consequence of a set X of formulas, $X\models _{FDE} B$, iff for all valuations v, if $v(A)\in \{1,b\}$, for all $A\in X$, then $v(B)\in \{1,b\}$. We will only need the case in which X is a singleton, which we will write as $A\models _{\mathsf {FDE}}B$.

Now, we note the following fact connecting the proof system for ${\mathsf {FDE}}$ and its consequence relation, treating formulas whose main connective is a modal as an atom.

Fact 1

$A {\succ }_{\mathsf {FDE}} B$ iff $A\models _{\mathsf {FDE}}B$. See Anderson and Belnap (1975, 204–205) for a proof. Another fact that we will appeal to below is the following.

Fact 2

If $A\models _{FDE}B$, then A classically entails B.

As before, we say that a set X of formulas is an $\mathsf {FDE}$-theory just in case (i) if $A\in X$ and $B\in X$, then $A\, \& \, B\in X$, and (ii) if $A\in X$ and $A\models _{\mathsf {FDE}}B$, then $B\in X$. Let $\mathcal {T}$ is the set of all $\mathsf {FDE}$-theories over the language $\mathcal {L}$. Say that a model $\mathcal {M}$ is in the class $\mathcal {F}$ of Fitting models iff for any $t\in {\mathsf {Term}}$ and any $w\in W_{\mathcal {M}}$ we have $\mathcal {E}(w,t)\in \mathcal {T}$ (where $\mathcal {E}\in \mathcal {M}$). That is to say, the class $\mathcal {F}$ of Fitting models contains all and only the models in which all evidence sets are drawn from $\mathcal {T}$.

Next, we define the relevant notions of theoremhood and validity. We say that A is a theorem of $\mathsf {HJ}_{\mathsf {FDE}}{}$ and write $\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\!A$ iff A is provable under the axioms and rules of $\mathsf {HJ}_{\mathsf {FDE}}{}$ above. We say that A is valid in $\mathsf {HJ}_{\mathsf {FDE}}{}$ and write $\models _{\mathsf {J}_{\mathsf {FDE}}}\!A$ iff for all models $\mathcal {M}\in \mathcal {F}$ and every $w\in W_{\mathcal {M}}$, we have that $\mathcal {M}, w\mathbin {\Vdash }A$. Now, we show that our proof system for logic $\mathsf {J}_{\mathsf {FDE}}$ is sound with respect to $\mathcal {F}$.

Theorem 1

(Soundness). If $\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\!A$, then $\models _{\mathsf {J}_{\mathsf {FDE}}}\!A$.

Proof

The proof is by induction on the length of the proof of A. Since all Fitting models use classical worlds, the axioms in (A1) are valid. As these are Fitting models obeying the ${\mathsf {Application}}$ condition, (A2) is valid. The classicality of the models also suffices to show that (A3) preserves validity.

For (A4), suppose that $A {\succ }_{\mathsf {FDE}} B$ but $\not \models _{{\mathsf {J}_{\mathsf {FDE}}}}\!\llbracket t \rrbracket A\mathbin {\supset }\llbracket t \rrbracket B$. Then there is a model $\mathcal {M}$ and a world w such that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket A$ and $\mathcal {M}, w\mathrel {\not \Vdash }\llbracket t \rrbracket B$. There are two cases: either there is a world u such that wRu and $\mathcal {M},u\mathrel {\not \Vdash }B$ or $B\not \in \mathcal {E}(w,t)$. We begin with the former case. By assumption, wRu and $\mathcal {M},u\mathrel {\not \Vdash }B$. It follows that $\mathcal {M},u\mathrel {\not \Vdash }A$. Since $A {\succ }_{\mathsf {FDE}} B$, it follows that $A\models _{\mathsf {J}_{\mathsf {FDE}}}\!B$, whence by Fact 2$\mathcal {M}, u\mathbin {\Vdash }B$, which is a contradiction. We proceed to the latter case, where $B\not \in \mathcal {E}(w,t)$. Since $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket A$, $A\in \mathcal {E}(w,t)$. As $A {\succ }_{\mathsf {FDE}} B$, and $\mathcal {E}(w,t)$ is an $\mathsf {FDE}$-theory, $B\in \mathcal {E}(w,t)$, which is a contradiction.

For (A5), suppose there is some model, $\mathcal {M}$, and world, w, such that $\mathcal {M},w\mathrel {\not \Vdash }\llbracket t \rrbracket A\, \& \,\llbracket t \rrbracket B\mathbin {\supset }\llbracket t \rrbracket (A\, \& \, B)$. So, $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket A\, \& \,\llbracket t \rrbracket B$, but $\mathcal {M},w\mathrel {\not \Vdash }\llbracket t \rrbracket (A\, \& \, B)$. There are then two cases: there is a u such that wRu and $\mathcal {M},u\mathrel {\not \Vdash }A\, \& \, B$ or $A\, \& \, B\not \in \mathcal {E}(w,t)$. The former case leads straightforwardly to a contradiction, so consider the latter. Suppose $A\, \& \, B\not \in \mathcal {E}(w,t)$. It follows from the assumption that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket A\, \& \,\llbracket t \rrbracket B$ that $A\in \mathcal {E}(w,t)$ and $B\in \mathcal {E}(w,t)$. As $\mathcal {E}(w,t)$ is an $\mathsf {FDE}$-theory, $A\, \& \, B\in \mathcal {E}(w,t)$, contradicting the assumption.$\square$

Having established the soundness of the proof system, we turn to completeness, which largely follows the proof provided by Fitting (2005).

Theorem 2

(Completeness) If $\models _{\mathsf {J}_{\mathsf {FDE}}}\!A$, then $\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\! A$.

For the proof, we will show the contrapositive, using a fairly standard canonical model construction.²⁵ This will require some additional definitions. If X is a set of formulas, then $X\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\! A$ iff $\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\!(B_1\, \& \,\cdots \, \& \, B_n)\mathbin {\supset }A$, for some $B_1,\ldots ,B_n\in Y$. Let a $\mathsf {J}_{\mathsf {FDE}}$-theory X be a set of formulas containing the theorems of $\mathsf {HJ}_{\mathsf {FDE}}{}$ and closed under classical consequence. A set X of formulas is consistent iff for no formula A, $X\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\!A\, \& \,\mathord {\sim }A$; and, X is maximally consistent iff X is consistent and there is no consistent set of formulas Y such that $X\subset Y$. By the usual Lindenbaum-style construction, any consistent set of formulas can be extended to a maximally consistent, prime $\mathsf {J}_{\mathsf {FDE}}$-theory.

We may now proceed with the construction of our the canonical model, $\mathcal {M}^c=\langle W^c,R^c,\mathcal {E}^c,v^c\rangle$, where

• $W^c$ is the set of maximally consistent, prime $\mathsf {J}_{\mathsf {FDE}}$-theories,

• $wR^cu$ iff $\{A:\exists t\in {\mathsf {T}erm}(\llbracket t \rrbracket A\in w)\}\subseteq u$,

• $\mathcal {E}^{c}(w,t)=\{A: \llbracket t \rrbracket A\in w\}$, and

• $v^c(w)=\{p:p\in w\}$.

We must verify that $\mathcal {M}^c\in \mathcal {F}$. That $R^c$ is properly defined is routine.

Lemma 1

For all $t\in {\mathsf {T}erm}$, for all $w\in W^c$, $\mathcal {E}^{c}(w,t)\in \mathcal {T}$.

Proof

Suppose $t\in {\mathsf {T}erm}$ and $w\in W^c$. There are two conditions to check. Suppose that $A\in \mathcal {E}^{c}(w,t)$ and $A\models _{\mathsf {FDE}}\!B$. It then follows that $\llbracket t \rrbracket A\in w$ and $\vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\!\llbracket t \rrbracket A\mathbin {\supset }\llbracket t \rrbracket B$. As w is a $\mathsf {J}_{\mathsf {FDE}}$-theory, $\llbracket t \rrbracket A\mathbin {\supset }\llbracket t \rrbracket B\in w$, and so $\llbracket t \rrbracket B\in w$. From the definition of $\mathcal {E}^c$, $B\in \mathcal {E}^{c}(w,t)$.

Suppose that $A\in \mathcal {E}^{c}(w,t)$ and $B\in \mathcal {E}^{c}(w,t)$. By definition, it follows that $\llbracket t \rrbracket A\in w$ and $\llbracket t \rrbracket B\in w$. From axiom (A5) and the definition of $\mathsf {J}_{\mathsf {FDE}}$-theory, we then have $\llbracket t \rrbracket (A\, \& \, B)\in w$, and so $A\, \& \, B\in \mathcal {E}^{c}(w,t)$, as desired.$\square$

Lemma 2

The canonical model $\mathcal {M}^c$ satisfies ${\mathsf {Application}}$.

Proof

Suppose $A\mathbin {\supset }B\in \mathcal {E}^{c}(w,t)$ and $A\in \mathcal {E}^{c}(w,t)$. It follows that $\llbracket t \rrbracket (A\mathbin {\supset }B)\in w$ and $\llbracket s \rrbracket A\in w$. From axiom (A2) together with the definition of $\mathsf {J}_{\mathsf {FDE}}$-theory, $\llbracket {t\cdot s} \rrbracket B\in w$, so $B\in \mathcal {E}^{c}(w,t\cdot s)$, as desired.

Next, we establish the crucial truth lemma.

Lemma 3

$A\in w$ iff $\mathcal {M}^c,w\mathbin {\Vdash }A$.

Proof

The proof is by induction on the complexity of the formula A. The base case of an atom is immediate by the definition of $v^c$. The conjunction case is handled by the inductive hypothesis. The disjunction case is handled by the primeness of the theories and the inductive hypothesis. The negation case is handled by the maximal consistency of the theories and the inductive hypothesis. The material conditional is handled similarly to the preceding two cases. This just leaves the modal case.

Let A be of the form $\llbracket t \rrbracket B$. Suppose that $\llbracket t \rrbracket B\in w$. By definition, $B\in \mathcal {E}^{c}(w,t)$ so $B\in \{C:\exists t\in {\mathsf {T}erm}, \llbracket t \rrbracket C\in w\}$. Suppose $wR^cu$, so $\{C:\exists t\in {\mathsf {T}erm}, \llbracket t \rrbracket C\in w\}\subseteq u$, whence $B\in u$. By the inductive hypothesis, $\mathcal {M}^c,u\mathbin {\Vdash }B$. This suffices for $\mathcal {M}^c,w\mathbin {\Vdash }\llbracket t \rrbracket B$. For the converse, suppose $\mathcal {M}^c,w\mathbin {\Vdash }\llbracket t \rrbracket B$ and assume for reductio that $\llbracket t \rrbracket B\not \in w$. By definition, this gives us $B\not \in \mathcal {E}(w,t)$. However, this implies $\mathcal {M}^c,w\mathrel {\not \Vdash }\llbracket t \rrbracket B$ contradicting our assumption. Therefore, $\llbracket t \rrbracket B\in w$.$\square$

Proof

We may now complete the sketch of the proof of theorem 2 establishing completeness. Suppose $\not \vdash _{\mathsf {HJ}_{\mathsf {FDE}}}\!A$. Then we can extend the set $\{\mathord {\sim }A\}$ to a maximally consistent, prime $\mathsf {J}_{\mathsf {FDE}}$-theory w. In the canonical model, $\mathcal {M}^c, w\mathbin {\Vdash }\mathord {\sim }A$, so $\mathcal {M}^c,w\mathrel {\not \Vdash }A$, demonstrating $\not \models _{\mathsf {J}_{\mathsf {FDE}}}\!A$, as desired.$\square$

Having established the soundness and completeness of the proof system $\mathsf {HJ}_{\mathsf {FDE}}{}$ for the logic $\mathsf {J}_{\mathsf {FDE}}$, we turn now to philosophical discussion. Specifically, we will provide further argumentation for our proposal and contrast it with some alternatives.

6 Discussion

To provide further motivation for the logic $\mathsf {J}_{\mathsf {FDE}}$, we begin by examining some of its consequences. First, recall from Sect. 4 that the sparse constraints on evidence sets in the traditional models for justification logic allowed for t to be justification for p without also being justification for either $p\, \& \, p$ or $p\vee q$. This is remedied in $\mathsf {J}_{\mathsf {FDE}}$, where $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$ implies both $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\, \& \, p)$ and $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket (p\vee q)$. In fact, this extends to cover all $\mathsf {FDE}$-entailments: if $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket A$ and $A\models _{FDE}B$, then $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket B$. So, we find that evidence is transmitted across $\mathsf {FDE}$-consequence. This brings us to our second observation that, despite this newfound closure, we have not stripped the logic of its characteristic hyperintensionality. This is because it need not be the case in $\mathsf {J}_{\mathsf {FDE}}{}$ that any piece of evidence justify all classical tautologies. That is, it is possible that $\mathcal {M},w\mathbin {\Vdash }\llbracket t \rrbracket p$ but $\mathcal {M},w\mathrel {\not \Vdash }\llbracket t \rrbracket (q\vee \mathord {\sim }q)$. These features resolve the tension for the unconstrained models that we highlighted earlier.

To get a better feel for how the logic works, we examine some of the (in)validities of $\mathsf {J}_{\mathsf {FDE}}{}$. We start by noting the validities listed below.

• 1. $\models _{\mathsf {J}_{\mathsf {FDE}}}\!\llbracket t \rrbracket (A\, \& \, B)\equiv (\llbracket t \rrbracket A \, \& \,\llbracket t \rrbracket B)$

• 2. $\models _{\mathsf {J}_{\mathsf {FDE}}}\!\llbracket t \rrbracket A\mathbin {\supset }\llbracket t \rrbracket (A\vee B)$

• 3. $\models _{\mathsf {J}_{\mathsf {FDE}}}\!\llbracket t \rrbracket \mathord {\sim }(A\vee B)\equiv \llbracket t \rrbracket (\mathord {\sim }A\, \& \,\mathord {\sim }B)$

These are immediate consequences of the fact that the modalized formulas in the consequents are $\mathsf {FDE}$-entailments of those found in the antecedents. But, even though evidence sets are now theories, we retain the invalidities below.

• 4. $\not \models _{\mathsf {J}_{\mathsf {FDE}}}\!\llbracket t \rrbracket (p\vee \mathord {\sim }p)$

• 5. $\not \models _{\mathsf {J}_{\mathsf {FDE}}}\!\llbracket t \rrbracket (p\, \& \,\mathord {\sim }p)\mathbin {\supset }\llbracket t \rrbracket q$

A closer inspection of these observations helps to reveal some of the benefits of our approach.

By considering the invalidity in 4, we can see that even though we have closed evidence sets under a type of logical consequence, this does not entirely strip our logic of its ability to avoid the problem of logical omniscience. Since $\mathsf {FDE}$ does not include any tautologies, closing evidence sets under $\mathsf {FDE}$-consequence will not entail that any sentences are required to be included in every evidence set. So, we retain many of the intuitively plausible aspects of closure principles on evidence without paying the cost of imposing full-blown logical omniscience.

Next, the invalidity in 5 makes it clear that the closure condition on evidence sets does not trivialise inconsistent evidence sets. This observation also highlights the non-normality of the modalities. The smallest normal modal logic $\mathsf {K}{}$ validates $\Box (p\, \& \,\mathord {\sim }p)\mathbin {\supset }\Box q$. However, the analogue given in 5 remains invalid, since there exists a model and a world w, not R-related to any worlds, such that $p\, \& \,\mathord {\sim }p\in \mathcal {E}(w,t)$ yet $q\not \in \mathcal {E}(w,t)$. To further explain, say that a theory is inconsistent iff it contains some formula, A, and its negation, $\mathord {\sim }A$. Say that a theory is trivial iff it contains every formula. There is only one inconsistent classical theory, the trivial theory. By contrast, there are many non-trivial inconsistent $\mathsf {FDE}$-theories. This makes $\mathsf {FDE}$ well-suited to modeling databases of potentially inconsistent information. As suggested at the outset of this paper, the logic $\mathsf {J}_{\mathsf {FDE}}{}$ can be understood to provide a logic for reasoning about inconsistent or incomplete databases.

Using the machinery of justification logic, we can reason about the consequences of combining different databases, which extends Belnap’s idea presented in the introduction, using classical logic as the underlying logic. This allows one to maintain classical intuitions about the truth and falsity of formulas while capturing many of the intuitions behind Belnap’s idea.²⁶ Given this, $\mathsf {J}_{\mathsf {FDE}}{}$ can be understood as a logic of justification for Belnapian databases.

As mentioned, Beall has argued that $\mathsf {FDE}$ is the logic of universal theory closure. We are using $\mathsf {FDE}$ consequence to close the evidence sets while we are not using $\mathsf {FDE}$ as the underlying logic. We think, nonetheless, that the combination adopted fits with Beall’s philosophy of logic. The use of $\mathsf {FDE}$ as the logic for evidential closure adds consequences to evidence sets but still respects some motivating intuitions of justification logics. One can strengthen the closure operator for some or all justification terms, to model situations where a particular sort of evidence has additional non-logical content.

The use of classical logic as the basic logic for reasoning about evidence strengthens the universal logic, $\mathsf {FDE}$. There are two, related reasons for this. The first is that, as Beall notes, strengthening the base logic with consequences beyond $\mathsf {FDE}$ may be justified depending on the particular theory at issue, in this case a theory of evidence or of Belnapian databases. Second, we are adopting a default classicality for reasoning about evidence.²⁷ The approach developed here takes it that reasoning about evidence will be consistent with no gaps about evidence, but if situations are encountered that violate this assumption, then one can fall back to using $\mathsf {FDE}$ as the base logic, while preserving many virtues of the current approach.

Earlier we said that one of the intuitions we wanted to capture was that justification transmits to ‘related’ formulas. Here, related formulas are those that are $\mathsf {FDE}$-consequences. The $\mathsf {FDE}$-consequences of p are a proper subset of the classical consequences of p. For example, $q\vee \mathord {\sim }q$ is not a $\mathsf {FDE}$-consequence of p. The justificatory connections are then tighter than classical logical consequence.

The claim that justificatory connections are then tighter than classical logical consequence naturally suggests involvement of topics or subject matters. While topics and subject matters do not have a formal role in our models, there are some formal connections which can be seen in the truth maker semantics of Fine (2016). Berto et al. (2022) show how to incorporate topics into models explicitly, so that each formula is assigned a topic, and topic inclusion plays an important role in the truth conditions of various operators, such as knowledge relative to information, $K_{A}B$. The topic inclusion clause for relative knowledge has the consequence that one may not know some tautologies, say $q\vee \lnot q$, relative to some given information, say p, because the topic of the tautologies is not contained in that of the information.²⁸ In the setting of justification logic, assigning topics to formulas and to justification terms could provide a way to maintain a strong closure condition while not requiring all tautologies to be justified by all justification terms, namely adding a topic inclusion condition to the semantic clause for the justifications.

On a suitable understanding, evidence may fail to be total just as it can be inconsistent. A bit of, say, perceptual justification for the claim that grass is green, need not itself constitute a bit of justification for the claim that either Launceston is north of Geelong or it is not. More generally, a piece of evidence or bit of justification need not take an evidential stand on all matters. It may remain silent about a good many claims, including but not limited to logical truths. This allows the justification logic $\mathsf {J}_{\mathsf {FDE}}{}$ to preserve some of the hyperintensionality mentioned earlier. Perceptual justification for the claim that either grass is green or it is not, need not justify the claim that either Cairns is north of Geelong or it is not.

One might think that the $\mathsf {K}{}$ axiom of justification logic has a tight connection with detachment, or modus ponens for material implication, which is invalid in $\mathsf {FDE}$. The connection, it turns out, is not that tight. Say that a set of formulas X is detached iff it is the case that if $A\in X$ and $A\mathbin {\supset }B\in X$ then $B\in X$. Evidence sets in Fitting models are not required to be detached, and there are many $\mathsf {FDE}$-theories that are not detached, although some are. This has consequences for the dot operation. One of these consequences is that, generally, the dot is not idempotent, $\mathcal {E}(w,t)\ne \mathcal {E}(w,t\cdot t)$, and, relatedly, $\llbracket {t\cdot t} \rrbracket A\mathbin {\supset }\llbracket t \rrbracket A$ is invalid. In addition, the dot is generally neither associative nor commutative.

Closure under $\mathsf {FDE}$-consequence affects the interpretation of the dot operation as a consequence of the logical behavior of the material conditional. Since $A\models _{FDE}\!B\mathbin {\supset }A$, it follows that $\mathcal {E}(w,t)\subseteq \mathcal {E}(w,t\cdot s)$ whenever $\mathcal {E}(w,s)$ is non-empty. To see this, suppose $A\in \mathcal {E}(w,t)$ and let $\mathcal {E}(w,s)$ be non-empty. From this it follows that $B\mathbin {\supset }A\in \mathcal {E}(w,t)$, where $B\in \mathcal {E}(w,s)$, and so by definition, $A\in \mathcal {E}(w,t\cdot s)$. This has consequences for inconsistent evidence sets, which we will define as evidence sets $\mathcal {E}(w,t)$ such that for some B, $B\wedge \mathord {\sim }B\in \mathcal {E}(w,t)$. Since $A\, \& \, \mathord {\sim }A\models _{FDE}\!(A\, \& \, \mathord {\sim }A)\mathbin {\supset }B$, for all A and B, if $\mathcal {E}(w,t)$ is inconsistent, then $\mathcal {E}(w,t\cdot t)$ will be trivial. Yet, it is still the case that there are inconsistent evidence sets $\mathcal {E}(w,s)$ such that $\mathcal {E}(w,t\cdot s)$ is non-trivial. It appears that there is much to explore in the fine structure of evidence composition, as given by the dot operation, in the present approach.

Let us say that a justification term t is inconsistent at a world w iff the evidence set assigned to t at w is inconsistent. As we saw above, there are some limits on composition of inconsistent justifications. We can sharpen those limits some. We begin by noting that for all formulas A and B,

$$ A\models _{\mathsf {FDE}} \mathord {\sim }A\mathbin {\supset }(B\wedge \mathord {\sim }B). $$

As a consequence, $\llbracket t \rrbracket A\mathbin {\supset }(\llbracket s \rrbracket \mathord {\sim }A\mathbin {\supset }\llbracket {t\cdot s} \rrbracket B)$ is valid. Even in a logic as inconsistency-tolerant as $\mathsf {FDE}$, the combination of the dot operation and the logical behavior of the material conditional present problems for non-trivial combination of justifications for contradictory claims. Say that two evidence sets are contradictory iff for some formula B, one set contains B and the other contains $\mathord {\sim }B$. Composing contradictory evidence sets leads to triviality of justification. Composing an inconsistent evidence set with itself leads to triviality as two copies of an inconsistent evidence set are contradictory.

There are two reactions that one might have these limitations. The first is to place the blame on the material conditional, and think that the logic should use a more restricted conditional, a route we will not explore here as it would take us to far afield.²⁹ The other reaction is to place the blame on the dot operation, prompting the question of whether there are any other operations on justification that may be more suited to $\mathsf {FDE}$. We will briefly explore this idea.

In Sect. 3, we mentioned that there is another operation on justification terms that is often used, the binary sum operation. We can add that operation as a new way to form terms. On the model-theoretic side, we place the condition

$\mathsf {Sum}$:

$\mathcal {E}(w,t)\cup \mathcal {E}(w,s)\subseteq \mathcal {E}(w,t+s)$

on the models. On the axiomatic side, we adopt the axioms $\llbracket t \rrbracket A\mathbin {\supset }\llbracket t+s \rrbracket A$ and $\llbracket t \rrbracket A\mathbin {\supset }\llbracket s+t \rrbracket A$. As an intuitive gloss, the sum operation pools the evidence and generates $\mathsf {FDE}$ consequences of the result. Not all $\mathsf {FDE}$-theories are detached, so one can sum inconsistent justifications without triviality. In contrast, the dot operation forms a new theory using some detachment, which is evidently trivializing in the face of some modest inconsistency.

There are two non-classical logics related to $\mathsf {FDE}$ whose consequence relations one may be tempted to use instead of $\mathsf {FDE}$ for closing evidence sets. These logics are $\mathsf {K3}{}$ and $\mathsf {LP}{}$.³⁰ These logics can be obtained from $\mathsf {FDE}$ by considering only the valuations that do not assign b or do not assign n, respectively, and otherwise using the same truth-tables. The definition of consequence remains the same, considering only these classes of valuations rather than all $\mathsf {FDE}$ valuations. Rather than interpret the justification terms by $\mathsf {FDE}$-theories, one would interpret them by $\mathsf {K3}{}$- or $\mathsf {LP}{}$-theories. From the definition of $\mathsf {K3}{}$- and $\mathsf {LP}{}$-consequence, one can see immediately that if $X\models _{\mathsf {FDE}} B$, then $X\models _{\mathsf {K3}} B$ and $X\models _{LP} B$.

Like $\mathsf {FDE}$, $\mathsf {K3}{}$ does not have any theorems and also avoids imposing logical omniscience. But, unlike $\mathsf {FDE}$, $\mathsf {K3}{}$-consequence satisfies $(A\, \& \,\mathord {\sim }A)\models _{\mathsf {K3}}B$, for all B. This means that $\mathsf {K3}$-theories are non-starters for dealing with inconsistent evidence. An upside of $\mathsf {K3}{}$ is that since modus ponens is valid, i.e. $A\wedge (A\mathbin {\supset }B)\models _{\mathsf {K3}}B$, all $\mathsf {K3}$-theories are detached, so the formula $\llbracket t \rrbracket (A\, \& \,(A\mathbin {\supset }B))\mathbin {\supset }\llbracket t \rrbracket B$ will be valid. The downside is that, due to there being only one inconsistent theory, the trivial one, $\llbracket t \rrbracket (A\, \& \,\mathord {\sim }A)\mathbin {\supset }\llbracket t \rrbracket B$ is valid. These properties might not be problematic if one is interested in applications where justifications and evidence are factive, in which case the T axiom, $\llbracket t \rrbracket A\mathbin {\supset }A$, should be in the logic.

As we saw above, the dot operation rules out non-trivial combination of some justifications, e.g. $\llbracket t \rrbracket A$ and $\llbracket s \rrbracket \mathord {\sim }A$. The result of combining them with the sum operation need not be trivial when interpreting the justification terms with $\mathsf {FDE}$-theories. This is not the case when using $\mathsf {K3}$-theories: If $A\in \mathcal {E}(w,t)$ and $\mathord {\sim }A\in \mathcal {E}(w,s)$, then $A\wedge \mathord {\sim }A\in \mathcal {E}(w,t+s)$, so $\mathcal {E}(w,t+s)$ must be the trivial theory. Relatedly, if $A\in \mathcal {E}(w,t)$ and $A\mathbin {\supset }B\in \mathcal {E}(w,s)$, then $B\in \mathcal {E}(w,t+s)$. In the context of $\mathsf {K3}{}$-theories the sum and dot operations are quite similar.

Using $\mathsf {LP}{}$-theories is, perhaps surprisingly, less attractive than using $\mathsf {K3}$-theories. All (non-empty) $\mathsf {LP}{}$-theories contain all classical tautologies.³¹ Consequently, the use of (non-empty) $\mathsf {LP}{}$-theories as evidence sets will result in all terms justifying all classical tautologies and $\llbracket t \rrbracket (A\vee \mathord {\sim }A)$ will be valid, as will $\llbracket t \rrbracket B\mathbin {\supset }\llbracket t \rrbracket (A\vee \mathord {\sim }A)$. We view this as a serious drawback since distinguishing classical tautologies is one of the key features of justification logic that makes it suited to formalize notions of justification.

There are some differences with the logic obtained from interpreting justification terms via $\mathsf {K3}$-theories, as one might expect. There are non-trivial, inconsistent $\mathsf {LP}{}$-theories, so $\llbracket t \rrbracket (A\, \& \,\mathord {\sim }A)\mathbin {\supset }\llbracket t \rrbracket B$ will be invalid. Note that the approach using $\mathsf {LP}{}$-theories as evidence sets inherits the limitations on using the dot operation to combine inconsistent and contradicting justifications that we saw with the approach using $\mathsf {FDE}$-theories.

Another point of difference between approaches using $\mathsf {K3}$- and $\mathsf {LP}{}$-theories as evidence sets comes out when looking at the dot and sum operations. There are $\mathsf {LP}{}$-theories that are not detached, so there will be more distance between the dot combination of two justifications and their sum, similar to what we saw with the approach using $\mathsf {FDE}$-theories as evidence sets.

Based on the preceding considerations, it seems that $\mathsf {LP}{}$-theories are not well suited to be used as interpretations of justification terms. They do collapse distinctions that justifications might draw among classical tautologies. $\mathsf {K3}$-theories, on the other hand, maintain those distinctions, although they are not well suited to considering inconsistent justifications. $\mathsf {FDE}$-theories are suited to inconsistent justifications, although, as we saw, there are limits to this enforced by dot operation.

The discussion above highlights an important feature in the comparison of $\mathsf {FDE}, \mathsf {K3}$, and $\mathsf {LP}. \mathsf {K3}{}$ and $\mathsf {LP}{}$ are asymmetric, in the sense that gaps and gluts are treated differently in the two logics. Considerations of symmetry can lead one to treat them in logically the same way, as noted by Beall (2017), whence one can arrive at $\mathsf {FDE}$. In the current context, there is a difference between the $\mathsf {K3}{}$ and $\mathsf {LP}{}$, illustrated by the following two observations. Intuitively, we don’t want every piece of evidence to justify every classical tautology, a desire that can be satisfied by $\mathsf {K3}{}$ but not $\mathsf {LP}. \mathsf {K3}{}$ will treat all inconsistent evidence alike, namely trivially, which $\mathsf {LP}{}$ does not do. In the present context, maintaining the intuition about evidence is more important. In the context of closure of evidence sets, there is some asymmetry between $\mathsf {K3}{}$ and $\mathsf {LP}{}$. Despite this difference, $\mathsf {FDE}$ still maintains the advantages of both logics.

Another non-classical logic, weak Kleene logic WK3, provides an alternative way of modeling topics that fits naturally with the ideas we have been exploring. Beall 2016 argues that WK3 provides a logic of preservation of both truth and topic.³² WK3 is a three-valued logic where if a subformula takes the intermediate value, then the whole formula takes the intermediate value, and like $\mathsf {K3}{}$, only the value 1 is designated. While WK3 shares some features with $\mathsf {K3}{}$, such as contradictions entailing everything, in WK3, p does not entail $p\vee q$. This means that closing (consistent) evidence sets under WK3 consequence need not result in every atom appearing in the evidence set, even as a disjunct.³³

To recap, our proposal highlights a philosophically motivated subclass of the more general class of Fitting models. Some known ideas from philosophical logic can be used to relieve tensions between the unconstrained Fitting models and epistemic applications of justification logic. Since the Fitting models are so flexible, one could focus on models that build additional closure conditions into the evidence sets. Natural closure conditions will push one to adopt theories for evidence sets; however, as mentioned above, the use of classical theories, i.e. theories closed under classical consequence, removes much of the interest of the justification terms. Thus, we have suggested using $\mathsf {FDE}$-theories.

One might object that what we have said motivates some closure conditions but perhaps falls short of the closure needed by $\mathsf {FDE}$-theories. For example, one might adopt the following conditions but no others.³⁴

• $A\, \& \, B\in \mathcal {E}(w,t)$ iff $A\in \mathcal {E}(w,t)$ and $B\in \mathcal {E}(w,t)$.

• $A\in \mathcal {E}(w,t)$ only if $A\vee B\in \mathcal {E}(w,t)$ and $B\vee A\in \mathcal {E}(w,t)$.

Many of the conditions one might adopt, including the above, are bundled into $\mathsf {FDE}$-theories. There may be applications for which these closure conditions, but not the full closure under $\mathsf {FDE}$-consequence, are motivated and desirable. Indeed, one may still see fit to only require closure under an even weaker type of consequence if concerned about the closure under adjunction and issues related to the Preface Paradox.³⁵ However, these issues remain separate from the present point and addressing them would take us too far afield for the current work.

One closure condition that is notably not built into $\mathsf {FDE}$-theories is closure under classical logical equivalence. Call a set of sentences X an equivalential theory iff X is closed under adjunction and Eq-logical consequence, where $A\models _{Eq}\!B$ iff $A\equiv B$ is a classical tautology. There are non-trivial, inconsistent equivalential theories, and equivalential theories will be closed under many, though not all, of the same entailments as $\mathsf {FDE}$-theories. Equivalential theories have a downside not shared by $\mathsf {FDE}$, which we think makes it unattractive. If an equivalential theory contains a tautology, it contains all tautologies, and, relatedly, if it contains the negation of any tautology, it contains the negation of each tautology. This washes out much of the hyperintensionality of justification logic, which we think should be preserved.

Before concluding, we will briefly discuss a somewhat related approach to epistemic logic with an explicit representation of evidence pursued by Sedlár (2015). Sedlár presents a bimodal epistemic logic whose modal operators are interpreted, in effect, via theories in different substructural logics. Sedlár uses two operators, $\Box$ for implicit belief by an agent and $\mathcal {A}$ for support by the evidence available to an agent. Sedlár’s approach, like ours, employs non-classical theories in the interpretation of modalities over a classical base. Because of this, on Sedlár’s approach there are failures of substitution of logical equivalents in the scope of modals, just as there are on our approach. Sedlár uses the modalities $\Box$ and $\mathcal {A}$ that are less fine-grained than the range of justification modalities, and so the $\mathsf {K}{}$ axioms used by Sedlár impose fewer constraints. Additionally, Sedlár’s approach validates $\mathcal {A}(B\vee C)\mathbin {\supset }(\mathcal {A}B\vee \mathcal {A}C)$, whereas the corresponding formula for our approach, $\llbracket t \rrbracket (B\vee C)\mathbin {\supset }(\llbracket t \rrbracket B\vee \llbracket t \rrbracket C)$, is invalid, as noted above.

Nonetheless, some caution is needed in comparing Sedlár’s approach with ours as there are important differences at the foundational level. Sedlár is using models for substructural logics with more connectives, so his models are more complex than ours. In contrast, we are using Fitting models, which only interpret the usual classical vocabulary and justification modalities. Sedlár is also motivated to avoid logical omniscience, an issue which we do not see as a problem for our approach, as agents do not enter into our approach. Sedlár responds to the problem of logical omniscience by pointing out that even if A and B are classically equivalent, $\mathcal {A}A$ is not, in general, equivalent to $\mathcal {A}B$.³⁶ A similar point holds in our framework, replacing $\mathcal {A}$ with a justification modal.

The approach of van Benthem et al. (2014) uses a single evidence modality, [E], interpreted via a function $E: W\mapsto \wp W$. The semantic clause for the evidence modality is that $w\mathbin {\Vdash }[E]A$ iff there is $X\in E(W)$ such that for all $x\in X$, $x\mathbin {\Vdash }A$. An evidence set on this approach is a set of sets of worlds, which cannot contain the empty set, glossed by saying “evidence per se is never contradictory.”³⁷ Given the semantic clause for the evidence modality, an empty evidence set, contradictory evidence, would justify everything. This differs from the present approach, which accepts the possibility of non-trivial contradictory evidence. A point of agreement between the two approaches is that the justification and evidence modalities obey a rule of monotonicity, although our approach uses $\mathsf {FDE}$ consequence rather than classical. As such, while the approach of van Benthem et al. (2014) has the result that evidence for anything is evidence for every classical tautology, our approach remains closer to basic justification logic in claiming that some evidence can justify one classical tautology without justifying all of them.

To conclude, justification logics offer flexible frameworks for investigating the logical fine structure of evidence. The philosophical interpretation of these logics, however, suggest that it would be appropriate for some purposes for evidence sets to be closed under some sort of consequence relation. This closure should not be closure under classical consequence, and instead, following some ideas of Beall, we suggest the use of $\mathsf {FDE}$-consequence, which has some distinct advantages over the closely related logics $\mathsf {K3}{}$ and $\mathsf {LP}{}$. The resulting logic and models provide another view of Belnap’s early motivation for $\mathsf {FDE}$, as a logic of databases, as well as illustrating an application of Beall’s more recent motivation for $\mathsf {FDE}$, as the universal closure relation on theories.