# stratified_evidence_logics__8ae4a4ef.pdf

Stratiﬁed Evidence Logics

Philippe Balbiani1 , David Fern andez-Duque2 , Andreas Herzig1 and Emiliano Lorini1

1Institut de Recherche en Informatique de Toulouse, Toulouse University 2Ghent University {philippe.balbiani,andreas.herzig,emiliano.lorini}@irit.fr, david.fernandezduque@ugent.be

Evidence logics model agents belief revision process as they incorporate and aggregate information obtained from multiple sources. This information is captured using neighbourhood structures, where individual neighbourhoods represent pieces of evidence. In this paper we propose an extended framework which allows one to explicitly quantify either the number of evidence sets, or effort, needed to justify a given proposition, provide a complete deductive calculus and a proof of decidability, and show how existing frameworks can be embedded into ours.

1 Introduction

Evidence logics were ﬁrst 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 justiﬁcation 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 stratiﬁed 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 ﬁnite 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 justiﬁed using up to one piece of evidence, [2]ϕ that ϕ can be justiﬁed using up to two pieces of evidence, and [ω]ϕ that ϕ can be justiﬁed using some ﬁnite (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 stratiﬁed evidence logics provide a powerful and useful alternative to existing logics of evidence suitable for applications in artiﬁcial intelligence (AI), where an artiﬁcial agent such as a chatbot or a conversational agent is expected to gather information, to ﬁlter 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., Netﬂix, Rotten Tomatoes, IMDb). Stratiﬁed evidence logics allow us to identify the number of recommendations that are sufﬁcient 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 stratiﬁed evidence logic has a natural axiomatization and is decidable.

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

2 Preliminaries

We will need a few basic facts from cardinal arithmetic, which we brieﬂy review. The cardinality of a set X is denoted |X|, and recall that cardinal addition is deﬁned 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 inﬁnite, then α + β = max{α, β}. We use ω to denote the cardinality of N (i.e., of the set of natural numbers), and ω1 to denote the ﬁrst 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, A 0 = { }, A 1 is the set containing all singletons {a} with a A, A ω is the set of countably inﬁnite 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 inﬁnite set P of propositional variables. We deﬁne a language LΩby the following grammar:

ϕ, ψ ::= | p | (ϕ ψ) | ϕ | [α]ϕ,

where p P and α Ω. Other Boolean connectives are deﬁned by the usual abbreviations, α ϕ is deﬁned by [α] ϕ, and we follow the standard rules for elimination of parentheses. We read [α]ϕ as ϕ can be justiﬁed using α pieces of evidence and α ϕ as ϕ cannot be refuted using α pieces of evidence . We deﬁne the stratiﬁed evidence logic SELΩby the following axioms and rules, where the nomenclature follows the modal logic literature.

(Taut) : All classical propositional tautologies

(Mon) : [α]ϕ [β]ϕ (if α < β)

(Dist+) : [α]ϕ [β]ψ [γ](ϕ ψ) (if α + β γ)

(T) : [α]ϕ ϕ

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

(50) : 0 ϕ [0] 0 ϕ

(MP) : ϕ ϕ ψ

(N0) : ϕ [0]ϕ

(RM) : ϕ ψ [α]ϕ [α]ψ

1For 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, deﬁned 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

([α1]ϕ1 . . . [αn]ϕn) [α]([α1]ϕ1 . . . [αn]ϕn)

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 stratiﬁed evidence frames.

Deﬁnition 4.1. Fix a cardinal degree set Ω. A stratiﬁed 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

Hα = {X W : (α, X) H}.

We say that F is a stratiﬁed 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 stratiﬁed evidence frame if it is a stratiﬁed 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 = T X. In this case, we will identify F with (W, E1). As usual, (strict) stratiﬁed evidence models are frames with a valuation V : P 2W .

The inequality β < α + 1 is a succinct way of writing β α if α is ﬁnite, β < α 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 ﬁnitely many evidence sets whose intersection is X : as we will see, this coincides with the interpretation of 2 of Baltag et al. (note that ω + 1 = ω by the deﬁnition of cardinal addition). If we want to consider countable intersections, we write [ω1]ϕ. We remark that, by set-theoretic convention, T = W, which is the reason that we stipulate E0 = {W}. Note that our deﬁnitions then imply that W Eα for all α Ω.

Deﬁnition 4.2. Let Ωbe a cardinal degree set and M = (W, E, V ) a stratiﬁed evidence model. The truth set of ϕ is deﬁned as follows:

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

Jp K = V (p); J ϕK = W \ JϕK; Jϕ ψK = JϕK 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 satisﬁability and validity are deﬁned as usual.

Theorem 4.3. Given a degree set Ω, the logic SELΩis sound for the class of stratiﬁed evidence models.

Proof. Let M = (W, E, V ) be an arbitrary stratiﬁed 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 deﬁne the strict evidence model M = (W, E1, V ). We claim that M |= h [1]h. Indeed, if G Jh K then G has a Hamiltonian cycle given by some permutation v. We then note that G Hv Jh K, which witnesses that G J[1]p K. 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 h K. However, we do have that M |= h [ω] h, since J h K = T 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 deﬁne a non-strict evidence model M = (W, E, V ). Then, M |= h [ω]h, since if T Jh K it follows that T halts after n steps for some n and thus T Hn Jh K. 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, T n<ω Nn = J h K, which is a countably inﬁnite 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:

ϕ, ψ ::= p | | (ϕ ψ) | ϕ | Eϕ | Bϕ | 20ϕ | 2ϕ | ϕ.

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 202 (in both cases, additional deﬁnable operators are also considered, as well as some proper extensions). Models are deﬁned over evidence frames, which are pairs (W, E) where E 2W ; such frames can be seen as a special case of stratiﬁed evidence frames where Ω= {0, 1}, and viewing E1 as the set of neighbourhoods. Semantics are given as in Deﬁnition 4.2, with the new clauses

w JEϕK iff there is X E such that X JϕK;

w J20ϕK iff there is X E such that w X JϕK;

w J2ϕK iff there is ﬁnite X E such that w T X JϕK;

w J ϕK iff JϕK = W.

The semantics for Bϕ are somewhat more elaborate. Say that S E is consistent if any ﬁnite 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 T S JϕK. We do not claim that Bϕ is deﬁnable in our language in general, but as pointed out in [Baltag et al., 2016a], E is deﬁnable in Lev 202 by Eϕ 2ϕ and B is also deﬁnable over the class of ﬁnite structures by Bϕ 32ϕ. Thus we will focus on comparing LΩand Lev 202 .

Theorem 6.1. Over the class of strict stratiﬁed evidence models, L{0,1,ω} is expressively equivalent to Lev 202 .

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

Proof. By induction we show that for every ϕ Lev 202 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 20ψ does (as the semantics are identical), and inspection on the semantics of [ω]ψ shows that it is equivalent to 2ψ, as both require that x T X JψK IH= Jψ K for some ﬁnite X E1. Note that the translation ϕ 7 ϕ is invertible, so the two languages are expressively equivalent.

On the other hand, Lev 202 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 ﬁnite 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 Stratiﬁed Evidence Models

The main result of this paper is that SELΩis complete for the class of strict stratiﬁed evidence models. As an intermediate step, we ﬁrst show that it is complete for the class of all stratiﬁed evidence models. This intermediate result is interesting since SELΩhas the ﬁnite 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 stratiﬁed evidence models and sound and (weakly) complete for the class of ﬁnite, stratiﬁed evidence models.

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

Deﬁnition 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 deﬁne the evidence sets in our canonical model.

Deﬁnition 7.3. Fix a degree set Ω, an admissible set Σ LΩ and w MC. For α Ωand ϕ Σ, deﬁne

Xϕ α = {v MCw : [α]ϕ v}.

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

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

Lemma 7.4. Given w MC, the structure Mw is a stratiﬁed 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 deﬁnition, 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 X := Xψ1 β1 . . . Xψn βn JϕK. (1)

Deﬁne ψ = [β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 ﬁnite Θ (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 θ = V Θ; observe that

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

[α]([0]θ ψ) [α]ϕ. (3)

On the other hand, since β1 + . . . + βn α, by Lemma 3.1 we obtain [0]θ ψ [α]([0]θ ψ),

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

and by (2) and (3), we see that (θ ψ) [α]ϕ. But, Θ {[β1]ψ1, . . . , [βn]ψn} w, 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 stratiﬁed 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 ﬁnite and since ϕ is consistent, ϕ w for some w MC. Thus Mw is a ﬁnite stratiﬁed evidence model satisfying ϕ.

8 Ranks and Decidability Note that Ωmay be inﬁnite, and as such, in a stratiﬁed evidence frame F = (W, E) the hierarchy E is technically an inﬁnite object, even when W is ﬁnite. However, E may admit a ﬁnite representation using ranks.

Deﬁnition 8.1. Given a stratiﬁed evidence frame F = (W, E) and X 2W , we deﬁne 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 stratiﬁed 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 ). Deﬁne Er by (α, X) Er if and only if rk(X) α. Then, (W, Er) is a stratiﬁed evidence frame with rank function r. Moreover, if (W, E) is any evidence frame with rank function rk then E = Erk.

The upshot is that (W, rk) is a ﬁnite object (since 2W is ﬁnite, as is each of its elements) and we can computably check if rk satisﬁes 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 ﬁnite model (W, E). Note that E may be inﬁnite even if W is ﬁnite; however in view of Lemma 8.3 we may represent it in the form (W, rk), which is ﬁnite since rk has ﬁnite domain.

9 The Representation Theorem Now we show that SELΩis also complete for the class of strict stratiﬁed models. In this case we will rely on ﬁnite models given by Theorem 7.1, so we will no longer obtain strong completeness. Moreover, the ﬁnite 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 ﬁnite stratiﬁed model and use that to construct a new strict stratiﬁed model. The relation between the two models will be witnessed by an honest map, as deﬁned below.

Deﬁnition 9.1. Let A = (W A, EA, V A) and B = (W B, EB, V B) be stratiﬁed evidence models. Let Ξ be a set of cardinals. A map π: W A W B is reliable (for Ξ) if, whenever ξ Ξ and X EA ξ , it follows that π[X] EB ξ . It is forthright (for Ξ) if, whenever ξ Ξ, Y EB ξ , π 1[Y ] EA ξ . A map that is reliable and forthright is honest (for Ξ).

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

Lemma 9.2. Let A = (W A, EA, V A) and B = (W B, EB, V B) be stratiﬁed 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 ﬁnite stratiﬁed evidence model M we can obtain a strict stratiﬁed evidence model A and an honest map π: W A W M, we will immediately obtain a completeness result for the class of strict stratiﬁed models. The following proposition shows that this is indeed the case.

Proposition 9.3. Let M = (W M, EM) be a ﬁnite stratiﬁed evidence frame and Ξ be a ﬁnite set of cardinals. Then, there exists a stratiﬁed evidence model A = (W A, EA 1 , V A) and an honest map π: W A W M.

Proof. Deﬁne EM Ξ := EM (Ξ 2W M) and let H EM Ξ be maximal with the property that there exists a stratiﬁed evidence frame A = (W A, EA 1 ) and a reliable map π: W A W M with π 1[X] EA ξ whenever X Hξ. We claim that H = EM Ξ . If not, let (α, N) EM Ξ \ H. Since Ξ is ﬁnite, choose β < α + 1 such that if β < α + 1 and α Ξ it follows that α α . Deﬁne 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 stratiﬁed evidence model, we only need to deﬁne EB 1 . We will deﬁne EB 1 = N O (for new and old ) as follows. We set N = {Ni : i Iβ}, where

Ni = ρ 1[N] [

j Iβ\{i} W A j ,

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

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

i Iβ Ni EB α .

We conclude that ρ 1[Y ] Hγ whenever (γ, Y ) Hγ {(α, N)}. Next we check that π is reliable. Let X EB 1 γ . We need to check that ρ T X EM δ whenever γ < δ + 1. Let J = {j Iβ : Nj X} and Y = X O. By deﬁnition of O, there is Z EA 1 such that |Z| = |Y| and Y = {σ 1[Z] : Z Z}. Consider two cases. If J = Iβ, then \

i J Ni = N Iβ = ρ 1[N]

ρ h\ X i = ρ h \

i Iβ Ni \ Y i = ρ h ρ 1[N] \ Y i

= N ρ h\ Y i = N πσ h\ Y i

Z Z σ 1[Z] i

= N πσσ 1 h\ Z i = N π h\ Z i ,

the last equality being because σ is surjective. Now, note that π[T Z] EM |Y| since π is reliable, and β + |Y| = γ < δ + 1, hence ρ[T X] EM δ , as needed. Otherwise, there is some j < β such that Nj X. Here, we claim that

ρ h \ X i = ρ h W A j \ Y i . (4)

To see this, note that clearly ρ[T X] ρ[W A j T Y], since W A j T i J Ni. For the other direction, take w ρ[T X]. Then, w = ρ(w, i) for some (w, i) T 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 T Y], and (4) holds as claimed. From this, we see that

ρ h \ X i = ρ h W A j \ Y i = πσ h W A j \ Y i

= πσ h W A j \

Z Z σ 1[Z] i

= πσ h W A j σ 1[ \ Z] i

= π h σ[W A j ] \ Z i = π h W A \ Z i

= π h \ Z i ,

which is an element of EM δ by our assumption on A and the fact that |Z| |X| < δ + 1. Thus B is a stratiﬁed evidence model and ρ 1[Y ] EB whenever Y Hγ {(α, N)}, contradicting the maximality of H. Hence we conclude that H = EA Ξ , and π is honest, as needed.

Theorem 9.4. The logic SELΩis sound and (weakly) complete for the class of strict stratiﬁed evidence models.

Proof. If ϕ is consistent then it is satisﬁable on some ﬁnite stratiﬁed evidence model M on some world w . Let Ξ be a ﬁnite set containing 0 and all cardinals appearing in ϕ. Then by Proposition 9.3 there is a strict stratiﬁed 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 stratiﬁed 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 sufﬁcient 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 satisﬁability 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 satisﬁability problem of our stratiﬁed 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 brieﬂy 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 stratiﬁed 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.

[Artemov, 2008] S. N. Artemov. The logic of justiﬁcation. The Review of Symbolic Logic, 1(4):477 513, 2008. [Balbiani et al., 2016] P. Balbiani, D. Fern andez-Duque, and E. Lorini. A logical theory of belief dynamics for resourcebounded agents. In Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, May 9-13, 2016, pages 644 652, 2016.

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

[Balbiani et al., 2018] P. Balbiani, D. Fern andez-Duque, and E. Lorini. The dynamics of epistemic attitudes in resourcebounded agents. Studia Logica, 2018. [Baltag and Occhipinti Liberman, 2017] A. Baltag and A. Occhipinti Liberman. Evidence logics with relational evidence. In Logic, Rationality, and Interaction - 6th International Workshop, LORI 2017, Sapporo, Japan, September 11-14, 2017, Proceedings, pages 17 32, 2017. [Baltag et al., 2016a] A. Baltag, N. Bezhanishvili, A. Ozg un, and A. Smets. Justiﬁed belief and the topology of evidence. In Logic, Language, Information, and Computation - 23rd International Workshop, Wo LLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings, pages 83 103, 2016. [Baltag et al., 2016b] A. Baltag, V. Fiutek, and S. Smets. Beliefs and evidence in justiﬁcation models. In Advances in Modal Logic, pages 156 176, 2016. [Baltag et al., 2017] A. Baltag, A. Ozg un, and A.L. Vargas Sandoval. Topo-logic as a dynamic-epistemic logic. In Logic, Rationality, and Interaction, pages 330 346, 2017. [Benferhat et al., 1993] S. Benferhat, D. Dubois, and H. Prade. Argumentative inference in uncertain and inconsistent knowledge bases. In Uncertainty in Artiﬁcial Intelligence, pages 411 419, 1993. [Benferhat et al., 1995] S. Benferhat, D. Dubois, and H. Prade. How to infer from inconsisent beliefs without revising? In International Joint Conference on Artiﬁcial Intelligence, pages 1449 1457, 1995. [Dubois et al., 2016] D. Dubois, W. Liub, J. Mac, and H. Prade. The basic principles of uncertain information fusion. An organised review of merging rules in different representation frameworks. Information Fusion, 32:12 39, 2016. [Falappa et al., 2013] M.A. Falappa, A.J. Garc ıa, G. Kern Isberner, and G.R. Simari. Stratiﬁed belief bases revision with argumentative inference. J. Philosophical Logic, 42(1):161 193, 2013. [Fitting, 2005] M. Fitting. The logic of proofs, semantically. Annals of Pure and Applied Logic, 132(1):1 25, 2005. [Liu and Lorini, 2017] F. Liu and E. Lorini. Reasoning about belief, evidence and trust in a multi-agent setting. In Proceedings of the 20th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2017), volume 10621 of LNCS, pages 71 89. Springer, 2017. [Miller, 1976] L.W. Miller. Normal functions and constructive ordinal notations. Journal of Symbolic Logic, 41(2):439 459, 1976. [Moss and Parikh, 1992] L. S. Moss and R. Parikh. Topological reasoning and the logic of knowledge: preliminary report. In Proceedings of the 4th conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pages 95 105. Morgan Kaufmann Publishers Inc., 1992. [Naumov and Tao, 2015] P. Naumov and J. Tao. Budgetconstrained knowledge in multiagent systems. In Proceedings of the 2015 International Conference on Autonomous

Agents and Multiagent Systems (AAMAS 2015), IFAAMAS, pages 219 226, 2015. [Shafer, 1976] G. Shafer. A Mathematical Theory of Evidence. Princeton University Press, 1976. [van Benthem and Pacuit, 2011a] J. van Benthem and E. Pacuit. Dynamic logics of evidence-based beliefs. Studia Logica, 99(1-3):61 92, 2011. [van Benthem and Pacuit, 2011b] J. van Benthem and E. Pacuit. Logical dynamics of evidence. In Logic, Rationality, and Interaction - Third International Workshop, LORI 2011, Guangzhou, China, October 10-13, 2011. Proceedings, pages 1 27, 2011. [van Benthem et al., 2012] J. van Benthem, David Fern andez-Duque, and E. Pacuit. Evidence logic: A new look at neighborhood structures. In Advances in Modal Logic 9, papers from the ninth conference on Advances in Modal Logic, held in Copenhagen, Denmark, 22-25 August 2012, pages 97 118, 2012. [van Benthem et al., 2014] J. van Benthem, D. Fern andez Duque, and E. Pacuit. Evidence and plausibility in neighborhood structures. Ann. Pure Appl. Logic, 165(1):106 133, 2014. [van der Hoek and Meyer, 1991] W. van der Hoek and J.- J. Ch. Meyer. Graded modalities in epistemic logic. Logique et Analyse, 34(133-134):251 270, 1991. [van Ditmarsch et al., 2007] H. van Ditmarsch, W. van der Hoek, and B. Kooi. Dynamic Epistemic Logic. Berlin: Springer, 2007. [Vel azquez-Quesada, 2013] F. R. Vel azquez-Quesada. Explicit and implicit knowledge in neighbourhood models. In Proceedings of LORI 2013, volume 8196 of LNCS, pages 239 252. Springer, 2013.

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)