Stratified Evidence Logics

1 Introduction

Evidence logics were first proposed by van Benthem and Pacuit [van Benthem and Pacuit, 2011a; van Benthem and Pacuit, 2011b] and then further developed by van Benthem et al. [van Benthem et al., 2012; van Benthem et al., 2014] and Baltag et al. [Baltag et al., 2016a; Baltag and Occhipinti Liberman, 2017]. More recently, they were extended to the multi-agent setting by [Liu and Lorini, 2017]. They aim to model belief formation in settings where an agent has access to different pieces of evidence. Evidence is modelled as a family of sets of possible states of the world, which the agent must then combine in various ways in order to form her beliefs. This is similar to the conception of evidence held by Shafer's theory of uncertainty [Shafer, 1976] as well as by theories of information fusion [Benferhat et al., 1993; Benferhat et al., 1995; Dubois et al., 2016] that conceive belief as the result of aggregating incomplete or uncertain information coming from various sources of evidence. It is also connected with justification logic by [Artemov, 2008; Fitting, 2005] in which evidence is expressed as a term, and possible manipulations of evidence are conceived as operations over terms.

Evidence logics can be applied both to situations where an agent receives information from possibly fallible sources such as news outlets, as well as to situations where an agent performs experiments to obtain data of varying precision about the state of the world, as in e.g. physics. Their semantics exploit neighbourhood models that have also been used to model explicit, as opposed to implicit, belief [Balbiani et al., 2016; Balbiani et al., 2018; Vel´azquez-Quesada, 2013].

The logics considered so far provide a qualitative account of belief formation: either an agent has evidence for a certain fact, or she does not. Our aim is to introduce a quantitative element to these frameworks resulting in a new family of logics called stratified evidence logics. This may be used to measure the number of distinct sources needed to pool enough evidence to justify a certain belief, or else be interpreted as a measure of effort, say in performing precise measurements. As we want to allow for the possibility of considering arbitrary but finite amount of data (or, perhaps, countably many pieces of information), we will model this effort using cardinal numbers: [1]ϕ means that the belief ϕ can be justified using up to one piece of evidence, [2]ϕ that ϕ can be justified using up to two pieces of evidence, and [ω]ϕ that ϕ can be justified using some finite (but arbitrarily large) amount of pieces of evidence. The idea of adding a quantitative parameter to epistemic modalities goes back to [van der Hoek and Meyer, 1991] in which graded epistemic logics are studied. More recently, it was further developed by [Naumov and Tao, 2015] who introduce modal operators capturing the "cost" for an agent of justifying a certain conclusion.

We believe that stratified evidence logics provide a powerful and useful alternative to existing logics of evidence suitable for applications in artificial intelligence (AI), where an artificial agent such as a chatbot or a conversational agent is expected to gather information, to filter it and to transfer the selected information to the human user. Such agents may be endowed with the capability of forming beliefs on the basis of the collected evidences. By way of example, consider a chatbot connected to the Internet who has to provide information to the human user about the quality of a certain movie. The chatbot has access to different recommendation systems about movies (e.g., Netflix, Rotten Tomatoes, IMDb). Stratified evidence logics allow us to identify the number of recommendations that are sufficient for the chatbot to form an opinion about the quality of the movie and to be able to inform the human about this.

As we will show, existing frameworks naturally embed into our own (with some exceptions). Moreover we show that stratified evidence logic has a natural axiomatization and is decidable.

2 Preliminaries

We will need a few basic facts from cardinal arithmetic, which we briefly review. The cardinality of a set X is denoted |X|, and recall that cardinal addition is defined so that |X| + |Y | = |X ∪ Y | whenever X, Y are disjoint; + will always denote cardinal addition. Cardinal addition is associative and commutative, and coincides with standard addition on natural numbers; on the other hand, if either α or β is infinite, then α + β = max{α, β}. We use ω to denote the cardinality of N (i.e., of the set of natural numbers), and ω1 to denote the first uncountable cardinal. We also use ∞ as a formal symbol which is decreed to be greater than any cardinal (and hence not itself an actual cardinal).

Given a set A and a cardinal λ, we use the notation (Aλ ) for the set of subsets of A with cardinality λ (for example, (A0 ) = {∅}, (A1 ) is the set containing all singletons {a} with a ∈ A, (Aω ) is the set of countably infinite subsets of A). A cardinal degree set is a set Ω whose elements are all cardinals and such that 0 ∈ Ω. We assume that Ω is countable and comes equipped with a computable notation system such that the relation α+β ≤ γ is decidable. 1 Typically we take Ω = N or Ω = N ∪ {ω}.

3 Syntax and Axiomatics

Our formal language will be parametrized by a cardinal degree set, Ω. Fix a countably infinite set P of propositional variables. We define a language LΩ by the following grammar:

where p ∈ P and α ∈ Ω. Other Boolean connectives are defined by the usual abbreviations, 〈α〉ϕ is defined by ¬[α]¬ϕ, and we follow the standard rules for elimination of parentheses. We read [α]ϕ as "ϕ can be justified using α pieces of evidence" and 〈α〉ϕ as "ϕ cannot be refuted using α pieces of evidence".

We define the stratified evidence logic SELΩ by the following axioms and rules, where the nomenclature follows the modal logic literature.

(Taut) : All classical propositional tautologies

(T) : [α]ϕ→ϕ

(4) : [α]ϕ→ [α][α]ϕ

1 For example, one can enumerate cardinals using a standard ordinal notation system [Miller, 1976].

As we will see, these axioms and rules are sound and complete for the class of evidence models, defined in the following section. First let us exhibit a useful family of derivable formulas.

Lemma 3.1. If α + β ≤ γ ∈ Ω, then [α]ϕ ∧ [β]ψ → [γ]([α]ϕ ∧ [β]ψ) is derivable. More generally, if α1 + . . . + αn ≤ α ∈ Ω, then

is derivable.

Proof. By 4 we have that ⊢ [α]ϕ ∧ [β]ψ → [α][α]ϕ ∧ [β][β]ψ, while by Dist+ we have that ⊢ [α][α]ϕ ∧ [β][β]ψ → [γ]([α]ϕ∧ [β]ψ). The second claim follows from similar reasoning by induction on n.

4 Evidence Semantics

Our models are based on evidence models as in e.g. [van Benthem et al., 2012]. However, since our language allows us to represent quantitative, as well as qualitative, information about evidence, it is convenient to encode such information into our models. Thus we arrive at the notion of stratified evidence frames.

Definition 4.1. Fix a cardinal degree set Ω. A stratified evidence pre-frame is a tuple F = (W, E), where W is a nonempty set of worlds and E ⊆ Ω × (2W \ {∅}). We call E an evidence hierarchy. For α ∈ Ω and H ⊆ E, we write

We say that F is a stratified evidence frame if E0 = {W} and, whenever (α1, X1), . . . , (αn, Xn) ∈ E, γ ≥ α1 + . . . + αn and X := X1 ∩ . . . ∩ Xn ̸= ∅, we have (γ, X) ∈ E.

We say that F is a strict stratified evidence frame if it is a stratified evidence frame and for all X ⊆ W and cardinals α, X ∈ Eα if and only if X ̸= ∅ and there are β < α+1 and X ∈ (E1 β ) such that X = ⋂ X. In this case, we will identify F with (W, E1).

As usual, (strict) stratified evidence models are frames with a valuation V : P → 2W .

The inequality β < α + 1 is a succinct way of writing β ≤ α if α is finite, β < α otherwise. The reason for this choice is that, in a strict evidence frame, for n < ω we want X ∈ En to mean 'there are n basic evidence sets whose intersection is X.' We also want X ∈ Eω to mean 'there are finitely many evidence sets whose intersection is X': as we will see, this coincides with the interpretation of ✷ of Baltag et al. (note that ω + 1 = ω by the definition of cardinal addition). If we want to consider countable intersections, we write [ω1]ϕ. We remark that, by set-theoretic convention, ⋂ ∅ = W, which is the reason that we stipulate E0 = {W}. Note that our definitions then imply that W ∈ Eα for all α ∈ Ω.

Definition 4.2. Let Ω be a cardinal degree set and M = (W, E, V ) a stratified evidence model. The truth set of ϕ is defined as follows:

• JpK = V (p);
• Jϕ∧ψK = JϕK ∩ JψK;
• J¬ϕK =W \ JϕK;
• w ∈ J[α]ϕK iff there is X ∈ Eα such that w ∈ X ⊆ JϕK.

We may also write M,w |= ϕ if w ∈ JϕK. The logical notions of satisfiability and validity are defined as usual.

Theorem 4.3. Given a degree set Ω, the logic SELΩ is sound for the class of stratified evidence models.

Proof. LetM= (W, E, V ) be an arbitrary stratified evidence model; the proof proceeds by checking that axioms are valid on M and rules preserve validity. We consider only a few examples.

For Mon, suppose that α < β and w ∈ J[α]ϕK. Then, there is X ∈ Eα such that w ∈ X ⊆ JϕK, so that α =: α1 ≤ β (seen as a one-element sum) and thus X ∈ Eβ (seen as a one-element intersection). Thus X ∈ Eβ is such that w ∈ X ⊆ JϕK, hence w ∈ J[β]ϕK. The argument for Dist+ is essentially the same, except that now we have X ∈ Eα such that w ∈ X ⊆ JϕK and Y ∈ Eβ such that w ∈ Y ⊆ JψK, so that if α + β ≤ γ then X ∩ Y ∈ Eγ and w ∈ X ∩ Y ⊆ Jϕ∧ψK. Axiom T holds because w ∈ J[α]ϕK means that there is X ∈ Eα with w ∈ X ⊆ JϕK, which yields w ∈ JϕK. For 4 we note that if w ∈ J[α]ϕK then there is X ∈ Eα such that w ∈ X ⊆ JϕK. Choose v ∈ X; then v ∈ X ⊆ JϕK, which means that v ∈ J[α]ϕK. Since v was arbitrary, X ⊆ J[α]ϕK, thus witnessing that w ∈ J[α][α]ϕK. Other axioms are fairly standard.

5 Motivating Examples

5.1 Hamiltonian Cycles

Suppose we are given a graph G = (X, E) with |X| = n, and we want to know if G contains a Hamiltonian cycle. Since this problem is NP-complete, there is no known method that is substantially better than guessing a sequence of nodes and checking whether it is indeed a Hamiltonian cycle.

To model this, let W be the set of all graphs with vertices X. Let V be a valuation such that V (h) is the set of all graphs of W that contain a Hamiltonian cycle, and Perm(X) be the set of permutations of X. To each permutation v = (v1, . . . , vn) ∈ Perm(X), let us assign two evidence sets: Hv, the set of G ∈ W such that v is a Hamiltonian cycle of G, and Nv, the set of G ∈ W such that v is not a Hamiltonian cycle of G. We let E1 be the family of sets of the forms Hv or Nv with v ∈ Perm(V ). Finally, we define the strict evidence model M = (W, E1, V ).

We claim that M |= h → [1]h. Indeed, if G ∈ JhK then G has a Hamiltonian cycle given by some permutation v. We then note that G ∈ Hv ⊆ JhK, which witnesses that G ∈ J[1]pK. On the other hand, M ̸|= ¬h → [1]¬h, as if v is any permutation of X, we have that there is G ∈ Nv which has a Hamiltonian cycle (just choose G′ to have a Hamiltonian cycle different from v) and thus Nv ̸⊆ J¬hK. However, we do have that M |= ¬h → [ω]¬h, since J¬hK = ⋂v∈Perm(X) Nv .

5.2 The Halting Problem

Now let us consider the halting problem, where we are given a Turing machine T (where we assume that the input is hardwired into T) and we want to know whether T halts. As before, the best that one can do in general is to simulate T and wait for it to halt.

Let W be the set of all Turing machines, and for each natural number n let En = {Hn, Nn}, where Hn is the set of machines that halt in at most n steps and Nn its complement. Let V (h) be the set of all Turing machines that halt, and define a non-strict evidence model M = (W, E, V ). Then, M |= h → [ω]h, since if T ∈ JhK it follows that T halts after n steps for some n and thus T ∈ Hn ⊆ JhK. On the other hand, every Nn contains a Turing machine that halts (just choose M to halt after n + 1 steps), so that M, T ̸|= ¬h → [ω]¬h. On the other hand, ⋂n<ω Nn = J¬hK, which is a countably infinite intersection and thus witnesses that M |= ¬h → [ω1]¬h.

6 Comparison to Existing Frameworks

Our framework is meant to be an extension of existing evidence logics, so it will be convenient to review such logics. For convenience we consider the following language, Lev of evidence logic:

The intention is for Lev to include the languages of both [Baltag et al., 2016a] and [van Benthem et al., 2012]. If we indicate sublanguages of Lev by displaying the allowed modalities as subindexes, van Benthem et al. consider Lev EB∀ and Baltag et al. consider Lev ✷0✷∀ (in both cases, additional definable operators are also considered, as well as some proper extensions). Models are defined over evidence frames, which are pairs (W, E) where E ⊆ 2W ; such frames can be seen as a special case of stratified evidence frames where Ω = {0, 1}, and viewing E1 as the set of neighbourhoods.

Semantics are given as in Definition 4.2, with the new clauses

• w ∈ JEϕK iff there is X ∈ E such that X ⊆ JϕK;
• w ∈ J✷ϕK iff there is finite X ⊆ E such that w ∈ ⋂ X ⊆ JϕK;
• w ∈ J✷0ϕK iff there is X ∈ E such that w ∈ X ⊆ JϕK;
• w ∈ J∀ϕK iff JϕK =W.

We do not claim that Bϕ is definable in our language in general, but as pointed out in [Baltag et al., 2016a], E is definable in Lev ✷0✷∀ by Eϕ ↔ ∃✷ϕ and B is also definable over the class of finite structures by Bϕ ↔ ∀✸✷ϕ. Thus we will focus on comparing LΩ and Lev ✷0✷∀ .

The semantics for Bϕ are somewhat more elaborate. Say that S ⊆ E is consistent if any finite intersection of elements of S is non-empty, and maximal consistent if no proper extension of S is consistent. Then, w ∈ JBϕK if and only if for every maximal consistent family S we have that ⋂ S ⊆ JϕK.

Theorem 6.1. Over the class of strict stratified evidence models, L{0,1,ω} is expressively equivalent to Lev ✷0✷∀ .

Proof. By induction we show that for every ϕ ∈ Lev ✷0✷∀ there is ϕ′ ∈ L{0,1,ω} equivalent to ϕ. Let M = (W, E, V ) be a strict evidence model. If ϕ = ∀ψ, by induction hypothesis there is ψ′ ∈ L{0,1,ω} equivalent to ψ. Then [0]ψ′ holds if and only if Jψ′ K = W, i.e. if and only if ∀ψ holds, and we may thus set ϕ′ = [0]ψ′ . Similarly, [1]ψ′ holds if and only if ✷0ψ does (as the semantics are identical), and inspection on the semantics of [ω]ψ′ shows that it is equivalent to ✷ψ, as both require that x ∈ ⋂ X ⊆ JψK IH= Jψ′ K for some finite X ⊆ E1. Note that the translation ϕ ↦→ ϕ′ is invertible, so the two languages are expressively equivalent.

On the other hand, Lev ✷0✷∀ cannot express [2]ϕ, although we leave a proof of this fact for future work. Thus our framework naturally embeds the framework of Baltag et al., and in the case of finite structures also that of van Benthem et al.

There are other frameworks which consider quantitative notions of knowledge or belief, although these typically model trust rather than effort [Baltag et al., 2016b; Falappa et al., 2013]. Topological semantics for epistemic logic [Baltag et al., 2017; Moss and Parikh, 1992] also takes the notion of "effort" to form a new belief into consideration, although the approach is qualitative rather than quantitative.

7 Completeness for Stratified Evidence Models

The main result of this paper is that SELΩ is complete for the class of strict stratified evidence models. As an intermediate step, we first show that it is complete for the class of all stratified evidence models. This intermediate result is interesting since SELΩ has the finite model property for this class, even when Ω contains uncountable cardinals. Thus we immediately obtain the decidability of SELΩ.

Theorem 7.1. Given a cardinal degree set Ω, the logic SELΩ is sound and strongly complete for the class of stratified evidence models and sound and (weakly) complete for the class of finite, stratified evidence models.

We prove this by a standard canonical model construction. Let Ω be a cardinal degree set. First let us define the set of worlds of our models. Say that a set Σ of formulas is admissible if it closed under subformulas, single negations and [0]⊤ ∈ Σ.

Definition 7.2. Let Ω be a cardinal degree set, Σ ⊆ LΩ be admissible, and let MC be the set of all maximal SELΩconsistent subsets of Σ. For w ∈ MC, let MCw be the set of all v ∈ MC such that, for all ϕ, [0]ϕ ∈ v if and only if [0]ϕ ∈ w.

In order to interpret [0] correctly, we need all of the worlds in a model to satisfy the same formulas of the form [0]ϕ. Thus we will not work with all of MC, but rather with subsets of the form MCw, and these will be the possible worlds in a model.

Next we define the evidence sets in our canonical model.

Definition 7.3. Fix a degree set Ω, an admissible set Σ ⊆ LΩ and w ∈ MC. For α ∈ Ω and ϕ ∈ Σ, define

Then, let Eα be the set of all non-empty sets of the form

such that α1 + . . . + αn ≤ α and ϕj ∈ Σ for each j ≤ n. With this we define the structure Mw = (MCw, E, V ) where u ∈ V (p) if and only if p ∈ u.

Lemma 7.4. Given w ∈ MC, the structureMw is a stratified evidence model.

Proof. First we check that E0 = {MCw}; that MCw ∈ E0 follows from the fact that [0]⊤ ∈ v for all v ∈ MCw, hence X⊤ 0 = MCw. On the other hand, if X ∈ E0, it follows that X = Xϕ1 0 ∩ . . . ∩Xϕn 0 for some formulas ϕ1, . . . , ϕn. For each i ≤ n, either [0]ϕi ∈ w and hence [0]ϕi ∈ v for all v ∈ MCw, or else [0]ϕi ̸∈ w and hence [0]ϕi ̸∈ v for all v ∈ MCw. In other words, Xϕi 0 ∈ {∅,MCw}. But the empty set is excluded from E0 by definition, which means that X = MCw, as needed.

Now, if α + β ≤ γ and X ∈ Eα, Y ∈ Eβ, we have that X = Xϕ1 α1 ∩ . . . ∩ Xϕn αn and Y = Xϕn+1 αn+1 ∩ . . . ∩ Xϕn+m αn+m for some sequence of formulas ϕ1, . . . , ϕn+m ∈ Σ and α1, . . . , αn+m ∈ Ω such that α1 + . . . + αn ≤ α and αn+1 + . . . + αn+m ≤ β. But then, α1 + . . . + αn+m ≤ α + β ≤ γ, hence X ∩ Y = Xϕ1 α1 ∩ . . . ∩Xϕn+m αn+m ∈ Eγ.

Lemma 7.5. Fix w0 ∈ MC. Then, for all w ∈ MCw0 and all formulas ϕ, ϕ ∈ w if and only if Mw0 , w |= ϕ.

Proof. A standard induction on formulas, of which only the case [α]ϕ is interesting. Suppose [α]ϕ ∈ w; then, Xϕ α ̸= ∅, hence w ∈ Xϕ α ∈ Eα. By the truth axiom, for all v ∈ Xϕ α we have that ϕ ∈ v, hence by the induction hypothesis, Xϕ α ⊆ JϕK, which means that Mw0 , w |= [α]ϕ.

Conversely, if Mw0 ,w |= [α]ϕ, then there are formulas [β1]ψ1, . . . , [βn]ψn ∈ Σ such that β1 +. . .+βn ≤ α, Xψi βi ̸= ∅, and

Define ψ = [β1]ψ1 ∧ . . . ∧ [βn]ψn.

Let us use the notation wα to denote the set of θ ∈ wα of the forms [α]θ′ or ¬[α]θ′ . We claim that there exists a finite Θ ⊆ (w0)0 such that Θ ⊢ ψ → ϕ; otherwise (w0)0 ∪ {ψ, ¬ϕ} would be consistent, hence extendible to a maximal consistent v ⊆ Σ, and then we would have that v ∈ X \ JϕK, contrary to (1).

Let θ = ∧ Θ; observe that

by axioms T 4 and N0, and thus ⊢ ([0]θ ∧ ψ) → ϕ. By the monotonicity rule, it follows that

On the other hand, since β1 + . . . + βn ≤ α, by Lemma 3.1 we obtain

and by (2) and (3), we see that ⊢ (θ ∧ ψ) → [α]ϕ. But,

and hence w ⊢ [α]ϕ; since [α]ϕ ∈ Σ by assumption, it follows that [α]ϕ ∈ w, as needed.

Proof of Theorem 7.1. For strong completeness, let Φ be a consistent set of formulas and Σ = LΩ. Then, Φ can be extended to a maximal consistent set w∗. The model Mw∗ is a stratified evidence model and for any ϕ ∈ Φ, from ϕ ∈ w∗ and Lemma 7.5 we obtain Mw∗ , w∗ |= ϕ, as needed.

For weak completeness, let ϕ be a consistent formula and let Σ be the least admissible set with ϕ ∈ Σ. Clearly MC is finite and since ϕ is consistent, ϕ ∈ w∗ for some w∗ ∈ MC. Thus Mw∗ is a finite stratified evidence model satisfying ϕ.

8 Ranks and Decidability

Note that Ω may be infinite, and as such, in a stratified evidence frame F = (W, E) the hierarchy E is technically an infinite object, even when W is finite. However, E may admit a finite representation using ranks.

Definition 8.1. Given a stratified evidence frame F = (W, E) and X ∈ 2W , we define rk(X) = α if α ∈ Ω is least such that X ∈ Eα, rk(X) = ∞ if there is no such α.

Recall that ∞ is a symbol that is decreed to be larger than all cardinals. Some properties of the rank function are as follows:

Lemma 8.2. Let F = (W, E) be a stratified evidence frame. Then:

1. If X ∈ Eα for some α ∈ Ω then rk(X) <∞.
2. If α ≥ rk(X) then X ∈ Eα.

Thus the frame (W, E) gives rise to a structure (W, rk). Moreover rk(X) = 0 iff X = W and rk(X ∩Y ) ≤ rk(X)+ rk(Y ). Similarly, we can reconstruct (W, E) from (W, rk).

Lemma 8.3. Let W be a set and r : 2W → Ω a function such that r(X) = 0 iff X ∈ {∅,W} and for all X, Y ∈ 2W , r(X ∩ Y ) ≤ r(X) + r(Y ). Define E r by (α,X) ∈ E r if and only if rk(X) ≤ α. Then, (W, E r ) is a stratified evidence frame with rank function r.

Moreover, if (W, E) is any evidence frame with rank function rk then E = E rk .

The upshot is that (W, rk) is a finite object (since 2W is finite, as is each of its elements) and we can computably check if rk satisfies the required properties, provided that the relevant operations on Ω are computable.

Theorem 8.4. Given a cardinal degree set Ω, the set of theorems of SELΩ is decidable.

Proof. This is an immediate consequence of Theorems 4.3 and 7.1, since any formula ϕ is either derivable or refutable in a finite model (W, E). Note that E may be infinite even if W is finite; however in view of Lemma 8.3 we may represent it in the form (W, rk), which is finite since rk has finite domain.

9 The Representation Theorem

Now we show that SELΩ is also complete for the class of strict stratified models. In this case we will rely on finite models given by Theorem 7.1, so we will no longer obtain strong completeness. Moreover, the finite model property will inevitably be lost if Ω contains any uncountable cardinals; note however that this is not an issue in the 'intended' case where Ω = N ∪ {ω}.

The idea is to start with a finite stratified model and use that to construct a new strict stratified model. The relation between the two models will be witnessed by an honest map, as defined below.

Definition 9.1. Let A = (W A, E A, V A) and B = (W B , E B , V B ) be stratified evidence models. Let Ξ be a set of cardinals. A map π: W A → W B is reliable (for Ξ) if, whenever ξ ∈ Ξ and X ∈ E A ξ , it follows that π[X] ∈ E B ξ . It is forthright (for Ξ) if, whenever ξ ∈ Ξ, Y ∈ E B ξ , π-1 [Y ] ∈ E A ξ . A map that is reliable and forthright is honest (for Ξ).

Note that honest maps are automatically surjective provided 0 ∈ Ξ, since from π[W A] ∈ E B 0 we obtain π[W A] = W B . Honest maps are useful because they preserve the truth of formulas. The following is easily verified by a standard induction on formulas.

Lemma 9.2. Let A = (W A, E A, V A) and B = (W B , E B , V B ) be stratified evidence models and π : W A → W B be an honest map such that for all w ∈ W A and p ∈ P, π-1 [V B (p)] = V A(p). Let ϕ be any formula and Ξ a set containing all cardinals that appear in ϕ. Then for any w ∈ W A we have that A, w |= ϕ if and only if B, π(w) |= ϕ.

Thus if given a finite stratified evidence model Mwe can obtain a strict stratified evidence model A and an honest map π : W A → W M, we will immediately obtain a completeness result for the class of strict stratified models. The following proposition shows that this is indeed the case.

Proposition 9.3. Let M = (W M, EM) be a finite stratified evidence frame and Ξ be a finite set of cardinals. Then, there exists a stratified evidence model A = (W A, E A 1 , V A) and an honest map π : W A → W M.

Proof. Define EM Ξ := EM ∩ (Ξ × 2W M ) and let H ⊆ EM Ξ be maximal with the property that there exists a stratified evidence frame A = (W A, E A 1 ) and a reliable map π : W A → W M with π-1 [X] ∈ E A ξ whenever X ∈ Hξ.

We claim that H = EM Ξ . If not, let (α,N) ∈ EM Ξ \ H. Since Ξ is finite, choose β < α + 1 such that if β < α′ + 1 and α′ ∈ Ξ it follows that α ≤ α′ . Define a new model B and a map σ: W B → W A as follows. Let Iβ be a set with cardinality β and set B = W A × Iβ, and σ(w, i) = w. Then, set ρ = πσ : W B → W M. For elements of B, we will write Xi instead of X ×{i}.

As B is a strict stratified evidence model, we only need to define E B 1 . We will define E B 1 = N ∪O (for 'new' and 'old') as follows. We set N = {Ni : i ∈ Iβ}, where

and we set O = {σ-1 [A] : A ∈ E A 1 }.

We have that ρ-1 [Y ] ∈ E B γ whenever Y ∈ Hγ, since π-1 [Y ] ∈ E A γ and thus there are ζ < γ + 1, a set Iζ with cardinality ζ and a collection {Ai : i ∈ Iζ} ⊆ E A 1 so that π-1 [Y ] = ⋂i∈Iζ Ai, and therefore ρ-1 [Y ] = σ-1π-1 [Y ] = σ-1 [⋂i∈Iζ Ai] = ⋂i∈Iζ σ-1 [Ai] ∈ E B γ , where the last step holds because σ-1 [Ai] ∈ O and B is a strict stratified evidence frame and |Iζ | = ζ < γ + 1. Moreover,

We conclude that ρ-1 [Y ] ∈ Hγ whenever (γ, Y ) ∈ Hγ ∪ {(α, N )}.

Next we check that π is reliable. Let X ∈ (E B 1 γ ). We need to check that ρ[⋂ X ] ∈ EM δ whenever γ < δ + 1. Let J = {j ∈ Iβ : Nj ∈ X} and Y = X∩O. By definition of O, there is Z ⊆ E A 1 such that |Z| = |Y| and Y = {σ-1 [Z] : Z ∈ Z}.

Consider two cases. If J = Iβ, then

and hence

the last equality being because σ is surjective. Now, note that π[⋂ Z] ∈ EM |Y| since π is reliable, and β + |Y| = γ < δ + 1, hence ρ[⋂ X ] ∈ EM δ , as needed.

Otherwise, there is some j < β such that Nj ̸∈ X. Here, we claim that

To see this, note that clearly ρ[⋂ X] ⊇ ρ[W A j ∩ ⋂ Y], since W A j ⊆ ⋂i∈J Ni. For the other direction, take w ∈ ρ[⋂ X]. Then, w = ρ(w, i) for some (w, i) ∈ ⋂ X. But, for any i ∈ J, (w, i) ∈ Nj, and for any Y = σ-1 [Z] ∈ Y, since (w, i) ∈ Y it follows that w ∈ Z and hence (w, j) ∈ σ-1 [Z]. Thus w = ρ(w, j) ∈ ρ[W A j ∩ ⋂ Y], and (4) holds as claimed. From this, we see that

which is an element of EM δ by our assumption on A and the fact that |Z| ≤ |X| < δ + 1.

Thus B is a stratified evidence model and ρ-1 [Y ] ∈ E B whenever Y ∈ Hγ ∪ {(α, N)}, contradicting the maximality of H. Hence we conclude that H = E A Ξ , and π is honest, as needed.

Theorem 9.4. The logic SELΩ is sound and (weakly) complete for the class of strict stratified evidence models.

Proof. If ϕ is consistent then it is satisfiable on some finite stratified evidence model M on some world w∗. Let Ξ be a finite set containing 0 and all cardinals appearing in ϕ. Then by Proposition 9.3 there is a strict stratified evidence model A and an honest map π: W A → W M. Since 0 ∈ Ξ, π is surjective, so for v∗ with π(v∗) = w∗ we have that M, v∗ |= ϕ, as needed.

10 Concluding Remarks

We have presented a new family of logics called stratified evidence logics. In contrast to traditional evidence logics that only account for the qualitative aspects of the connection between evidence and belief, our logics focus on the quantitative aspects. In particular, they allow us to represent the amount of pieces of evidence that are sufficient for an agent to form a certain belief. We have studied the mathematical and computational properties of our framework by providing a complete deductive calculus and proving that its satisfiability problem is decidable. Moreover, we have shown that existing evidence logics can be embedded in our framework.

There are at least three directions that we plan to explore in future work. First of all, we plan to study complexity of the satisfiability problem of our stratified evidence logic and to provide a decision procedure for it based on tableaux. The latter will make it exploitable in the context of AI applications, such as the one briefly described in Section 5. Secondly, we plan to move from a static to a dynamic perspective by adapting the "model update" approach of dynamic epistemic logic [van Ditmarsch et al., 2007] to our setting. The idea is to formalize two basic operations on evidence, conceived as update operations on strict stratified evidence models: evidence expansion and evidence contraction. The former consists in adding a new piece of evidence to the agent's evidence set E1, while the latter consists in removing a piece of evidence from it. Thirdly, we plan to generalize our framework to the multi-agent setting in which different agents may have different evidence sets and exchange pieces of evidence through communication.