Evidence Logic: A New Look at Neighborhood
Structures
Johan van Benthem 1
Institute for Logic, Language and Computation
University of Amsterdam
Department of Philosophy
Stanford University

David Fernández-Duque 2
Department of Computer Science and Artificial Intelligence
University of Seville

Eric Pacuit 3
Department of Philosophy
University of Maryland, College Park

Abstract
Two of the authors (van Benthem and Pacuit) recently introduced evidence logic as away to model epistemic agents faced with possibly contradictory evidence from different sources. For this the authors used neighborhood semantics, where a neighborhood
N indicates that the agent has reason to believe that the true state of the world lies
in N . A normal belief modality is defined in terms of the neighborhood structure.
In this paper we consider four variants of evidence logic which hold for different
classes of evidence models. For each of these logics we give a representation theorem
using extended evidence models, where the belief operator is replaced by a standard
relational modality. With this, we axiomatize all four logics, and determine whether
each has the finite model property.
Keywords: Neighborhood Models, Logics of Belief, Combining Logics

1

Introduction

Neighborhood models are a generalization of the usual relational semantics formodal logic. In a neighborhood model, each state is assigned a collection ofsubsets of the set of states. Such structures provide a semantics for both normal
1johan.vanbenthem@uva.nl
dfduque@us.es
3 epacuit@umd.ed2

98

Evidence Logic: A New Look at Neighborhood Structuresand non-normal modal logics. See [17] for an early discussion of neighborhood
semantics for modal logic, and [6,12,7] for modern motivations and mathematical details. Concrete uses of neighborhood models include logics for knowledge[22], players’ powers in games [13,14], concurrent PDL [15], and beliefs in the
epistemic foundations of game theory [24,10].
In this paper, we study yet another concrete interpretation of neighborhoodmodels. The idea is to interpret the neighborhood functions as describing theevidence that an agent has accepted (in general, we assume the agent accepts
different evidence at different states). The agent then uses this evidence toform her beliefs. A dynamic extension of this logic of evidence-based belief wasintroduced in [21]. The main technical contribution of that paper is a series ofof relative completeness results in the style familiar to much of the literatureon dynamic epistemic logic: validity in a language with dynamic modalities isreduced to a modal language without the dynamic modalities via the validity ofso-called recursion axioms (see [19] for a general discussion of this technique).
In this paper, we continue the project started in [21] focusing on the underlying
static logics of belief and evidence.
To do this, we shall consider four variants of evidence logic, which dependon the fundamental assumptions one may make about evidence models. For
each of the resulting logics, we prove two main results.
The first is a characterization theorem in terms of extended evidence models.
These differ from evidence models only in that belief is interpreted via an explicit accessibility relation rather than in terms of the neigbhorhood structure.
We show that, up to p-morphism, the class of extended evidence models andthe class of evidence models are equivalent for each logic considered.
The second is to give a complete deductive calculus for each logic. Here ourrepresentation using extended evidence models is crucial, since it permits us toemploy familiar techniques from modal logic.

2

A Logic of Evidence and Belief

We start by presenting our formal framework for evidence logics, leaving a moredetailed discussion of its motivation to the end of this section. Given a set W
of possible worlds or states, one of which represents the “actual” situation,
an agent gathers evidence about this situation from a variety of sources. To
simplify things, we assume these sources provide binary evidence, i.e., subsetsof W which (may) contain the actual world. The agent uses this evidence (i.e.,collection of subsets of W ) to form her beliefs.
The following modal language can be used to describe what the agent believes given her available evidence (cf. [21]).
Definition 2.1 Let At be a fixed set of atomic propositions. Let L be thesmallest set of formulas generated by the following grammarp | ¬ϕ | ϕ ∧ ψ | Bϕ | 2ϕ | Aϕ
where p ∈ At. Additional propositional connectives (∧, →, ↔) are defined asvan Benthem, Fernández-Duque and Pacuit99

b and A,b respectively.
usual and the duals 4 of 2, B and A are 3, B
The intended interpretation of 2ϕ is “the agent has evidence for ϕ” andBϕ says that “the agents believes that ϕ is true.” We also include the universal
modality (Aϕ: “ϕ is true in all states”) for technical convenience. 5
Since we do not assume that the sources of the evidence are jointly consistent(or even that a single source is guaranteed to be consistent and provide all theavailable evidence), the “evidence for” operator (2ϕ) is not a normal modal
operator. That is, the agent may have evidence for ϕ and evidence for ψ(2ϕ ∧ 2ψ) without having evidence for their conjunction (¬2(ϕ ∧ ψ)). Of
course, both the belief and universal operators are normal modal operators.
So, the logical system we study in this paper combines a non-normal modal
logic with a normal one.
2.1 Neighborhood Models for L
In the intended interpretation of evidence logic, there are many possible statesof the world, and the agent possesses evidence for these states in the form ofneighborhoods; all other epistemic operators are derived from this neighborhood structure.
Thus we define evidence models as follows:
Definition 2.2 An evidence model is a tuple M = hW, E, V i, where W isa non-empty set of worlds, E ⊆ W × ℘(W ) is an evidence relation, V : At →℘(W ) is a valuation function. We write E(w) for the set {X | wEX}. Twoconstraints are imposted on the evidence sets: For each w ∈ W , ∅ 6∈ E(w) andW ∈ E(w). A uniform evidence model is an evidence model where E(·) isa constant function (each state has the same set of evidence).
We do not assume that the collection of evidence sets E(w) is closed under
supersets. Also, even though evidence pieces are non-empty, their combination
through the obvious operations of taking intersections need not yield consistentevidence: we allow for disjoint evidence sets, whose combination may lead (andshould lead) to trouble. But importantly, even though an agent may not be able
to consistently combine all of her evidence, there will be maximal collectionsof admissible evidence that she can safely put together to form scenarios:
Definition 2.3 A w-scenario is a maximal collection X ⊆ E(w) thathas the fip (i.e., theTfinite intersection property: for each finite subfamily{X1 , . . . , Xn } ⊆ X , 1≤i≤n Xi 6= ∅). A collection is called a scenario if it
is a w-scenario for some state w.
Truth of formulas in L is defined as follows:
Definition 2.4 Let M = hW, E, V i be an evidence model. Truth of a formulaϕ ∈ L is defined inductively as follows:•

M, w |= p iff w ∈ V (p)4b = ¬B¬, and similarly for other operators.
In other words, B
A natural interpretation of Aϕ in the context of this paper is “the agent knows that ϕ”.

5(p ∈ At)

100

Evidence Logic: A New Look at Neighborhood Structures•

M, w |= ¬ϕ iff M, w 6|= ϕ•M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψM, w |= 2ϕ iff there exists X such that wEX and for all v ∈ X, M, v |= ϕT• M, w |= Bϕ for each w-scenario X and for all v ∈X , M, v |= ϕ••M, w |= Aϕ iff for all v ∈ W , M, v |= ϕThe truth set of ϕ is the set [[ϕ]]M = {w | M, w |= ϕ}. The standard logicalnotions of satisfiability and validity are defined as usual.
Our notion of having evidence for ϕ need not imply that the agent believes
ϕ. In order to believe a proposition ϕ, the agent must consider all her evidence
for or against ϕ. The idea is that each w-scenario represents a maximallyconsistent theory based on (some of) the evidence collected at w. 6 Note thatthe definition of truth of the “evidence for” operator builds in monotonicity.
That is, the agent has evidence for ϕ at w provided there is some evidence
available at w that implies ϕ.
The class of evidence models we have described gives the most general setting such an agent may face. However, there are natural additional assumptions
one may consider:
Definition 2.5 An evidence model M is flat if every scenario on M has nonempty intersection. In the interest of brevity, we may write [-evidence model
instead of flat evidence model.
An evidence model M = hW, E, V i is uniform if E is a constant. In thiscase, we shall treat E as a set (of neighborhoods) rather than a function.
Flatness and uniformity are natural assumptions which, as we will see, may
be captured by adding different axioms to our logic.
2.2 The Logics
We now turn to logics for reasoning about distinct classes of evidence models.
Our first observation is that the language L is sensitive to flatness:b
Lemma 2.6 If M is a [-evidence model, then M |= 2ϕ → Bϕ.
Proof. If X ∈ E(w) is an evidence set witnessing ϕ (i.e., X ⊆ [[ϕ]]M ), then the
singleton {X} can be extended to a w-scenario using Zorn’s Lemma, which, inflat structures, has non-empty intersection.
2b
Meanwhile, the formula 2ϕ → Bϕ is not valid in general: Consider auniform evidence model M∞ = hW, E, V i with domain W = N and evidence
sets E(w) = {[N, ∞) | N ∈ N} for each w ∈ W . The valuation is unimportant,soon M∞ is all of E, but
T we may let V = ∅. Clearly, the only scenario
b yet M∞ |= 2> (this formulaE = ∅. Hence M∞ |= B⊥, i.e., M∞ 6|= B>;
is universally valid), and we concludeb
M∞ 6|= 2> → B>.
6

Analogous ideas occur in semantics of conditionals [9,23] and belief revision [3,16].

van Benthem, Fernández-Duque and Pacuit

101

From this we get the following corollary:
Corollary 2.7 The logic of evidence models does not have the finite model
property, nor does the logic of uniform evidence models.
b
Proof. Every finite model is flat, and hence validates 2> → B>;
but as wehave just shown, this formula is not valid over all uniform evidence models. 2
With this in mind, we state a list of axioms and rules for evidence logics:
taut

all propositional tautologies

S5A

S5 axioms for A

KB

K axioms for B>-evidence2>

pullout

2ϕ ∧ Aψ ↔ 2(ϕ ∧ Aψ)universal belief

Aϕ → BAϕ2-monotonicity

ϕ→ψ
2ϕ → 2ψ[b
2ϕ → Bϕ-uniformity

ϕ→A

ϕ for

MP

Modus Ponens

N

Necessitation for

b 2, 3= B, B,= A, BWe let Log denote the logic which uses all axioms and rules except for [ orthe uniformity axioms. The subscripts [, u denote the addition of the respective
axioms. We will denote derivability in the logic λ by `λ , where λ is any one of
the four combinations that we may form, that is, λ ∈ {Log, Log[ , Logu , Log[u }.
The weakest logic Log will be called general evidence logic, while Log[ , Log[uwill be called flat logics and Logu , Log[u will be called uniform logics. We will
write λ-consistency for consistency over the logic λ.
2.3 Extended Neighborhood Models for L
The finite model property fails for evidence logic, a fact which may be rather
inconvenient. Fortunately, there is a way to sidestep this problem.
In evidence models, the belief operator is interpreted using the neighborhoods by taking intersections of scenarios. There is another natural class ofmodels for the language L which avoids the use of scenarios. The key idea is

102

Evidence Logic: A New Look at Neighborhood Structures

to extend a neighborhood model with a relation R that will be used to interpret the belief modality. These models will allow us, later, to employ standard
techniques from modal logic to prove completeness.
Definition 2.8 An extended evidence model is a structure M =hW, R, E, V i where such that W is a set, R an (arbitrary) binary relation on
W , E ⊆ W × ℘(W ) is a relation such that w E W and w 6E ∅ for all w ∈ W ,and V : At → ℘(W ).
Truth in an extended evidence model is defined in the standard way:
Boolean connectives are as usual, M, w |= Aϕ iff for all v ∈ W , M, v |= ϕ;M, w |= Bϕ iff for all v ∈ W , if wRv then M, v |= ϕ; and M, w |= 2ϕ iff there
exists a X ⊆ W such that w E X and for all v ∈ X, M, v |= ϕ. We write[[ϕ]]M = {w | M, w |= ϕ} for the truth set of ϕ in M.
As we shall see below, for every evidence model M there is an extended
evidence model which is naturally associated to it and satisfies the same Lformulas. But first, let us also define a notion of “flatness” for extended evidence models:Definition 2.9 Given w E X, we will say X is flat for w if there is v ∈ Xsuch that w R v. The set X is flat if it is flat for all w ∈ W such that w E X.
The extended evidence model M is flat if every evidence set is flat.
For uniform extended evidence models, we will also demand that the accessibility relation be independent of the current state:
Definition 2.10 An extended evidence model M = hW, R, E, V i is uniform if
both R and E are constant; that is, given w, v, u ∈ W and X ⊆ W , w R u if
and only if v R u and, likewise, w E X if and only if v E X.
2.4 Motivating the Logics
Having stated our formal framework, we digress from the main technical goalof this paper to discuss the intended interpretation of evidence models in somemore detail. The reader who is interested in technical aspects only can safely
skip ahead to the next section.
In a number of areas, the need has long been recognized for models thatkeep track of the reasons, or the evidence for beliefs and other informational
attitudes (cf. [11,8]). At one extreme, the evidence is encoded as the current
range of worlds the agent considers possible. However, this ignores how theagent arrived at this epistemic state. At the other extreme, models record thecomplete syntactic details of what the agent has learned so far (including the
precise formulation and sources for each piece of evidence). In this paper, we
explore an intermediate level, viz. neighborhood structures, where evidence isrecorded as a family of sets of worlds. In particular, we want to mention three
general issues:
We start by making explicit the underlying assumptions motivating the
logical framework defined in Section 2.1. Let W be a set of states (or possible
worlds) one of which represents the “actual” state. We are interested in asituation where an agent gathers evidence about this state from a variety ofvan Benthem, Fernández-Duque and Pacuit

103

sources. To simplify things, we assume these sources provide binary evidence,i.e., subsets of W which (may) contain the actual world. The following basic
assumptions are implicit in the above definitions:(i) Sources may or may not be reliable: a subset recording a piece of evidence
need not contain the actual world. Also, agents need not know whichevidence is reliable.
(ii) The evidence gathered from different sources (or even the same source)
may be jointly inconsistent. And so, the intersection of all the gatheredevidence may be empty.
(iii) Despite the fact that sources may not be reliable or jointly inconsistent,
they are all the agent has for forming beliefs. 7
The evidential state of the agent is the set of all propositions (i.e., subsetsof W ) identified by the agent’s sources. In general, this could be any collectionof subsets of W ; but we do impose some constraints:•

No evidence set is empty (evidence per se is never contradictory),•

The whole universe W is an evidence set (agents know their ‘space’).

In addition, one might expect a ‘monotonicity’ assumption:
If the agent has evidence X and X ⊆ Y then the agent has evidence Y .
To us, however, this is a property of propositions supported by evidence, notof the evidence itself. Therefore, we model this feature differently through thedefinition of our “evidence for” modality (2).
This brings us to a second point of discussion. The evidence models discussed in this paper do not directly represent the agent’s sources of evidence.
However, the neighborhood models can be used to distinguish between a wide
range of evidential situations. Consider the following three evidential states:
p

q

p

q

X2
p

q

X1
E1 = {X1 }X3
E2 = {X2 , X3 }

q

p

X4

q
X5

E3 = {X4 , X5 }In each state, the agent has evidence that p ∨ q is true (but not both).
However, the evidential situation underlying each state is very different. In
the first situation, the agent has received the information from a single source(which the agent “trusts”) that the actual state satisfies either p ∧ ¬q or ¬p ∧ q.
In the second situation, the agent has received the same information from two
7

Modeling sources and agents’ trust in these is possible – but we will not pursue this here.

104

Evidence Logic: A New Look at Neighborhood Structuresdifferent sources (or perhaps the same source reinforced its evidence). The
sources agree that either p ∧ ¬q or ¬p ∧ q is true, but disagree about theconditions under which these formulas are true. Finally, the most interestingcase is the third one where the agent received information from two sourcesthat agree on the conditions under which p ∧ ¬q is true, but disagree about
the conditions needed to make ¬p ∧ q true. In this case, the agent believes p,
whereas in the first two situations the agent only believes the weaker proposition
that p ∨ q is true. Note that our language (see Definition 2.1) can distinguishbetween the third situation and the first two, but cannot distinguish between
the first two evidential situations.
Our final point of discussion concerns the relationship between evidence
models and existing modal logics of knowledge and belief based on so-called“plausibility models”. 8 The models proposed here are not intended to replace
plausibility models, but rather to complement them. So, what exactly is therelationship between these two frameworks for modeling beliefs? This questionis explored in detail in [21, Section 5], but we only mention the highlights here.
Every plausibility model can be transformed into a uniform evidence model
where the set of evidence are all the downward closed subsets (according to
the plausibility ordering). This, in part, motivates our interest in the logic ofuniform evidence models. There is also a translation from evidence models toplausibility models (using the well-known definition of a specialization (pre)order). However, it is easy to see that not every evidence model, not even a
uniform one, comes from a plausibility model. So, evidence models generalize
the standard plausibility models which have been successfully used to represent
an agent’s knowledge and different flavors of belief. Once again, this shows the
additional level of generality provided by neighborhood models. 93

Representation Theorems

It is generally more convenient to work with extended evidence models thanwith standard evidence models, since it is easier to control accessibility relations
than scenarios. Fortunately, as we shall show in this section, the two classes ofmodels are equivalent with respect to our logics.
As it turns out, any evidence model may be represented as an extended
evidence model with the same truth sets. The converse does not hold; yet,every extended evidence model is a p-morphic image of an evidence model.
The first claim is straightforward to check given the following construction.
Definition 3.1 Given an evidence model M = hW, E, V i, define an extended
evidence model M∗ = hW, RE , E, V i where w RE v if and only if v lies in theintersection of some w-scenario.
8 A plausibility model is a tuple hW, , V i where W is a nonempty set, V is a valuation
function and  is a reflexive, transitive and well-founded order on W . We assume the reader
is familiar with these well-studied models and the modal languages used to reason about
them (see [19] for details and pointers to the relevant literature).
9 Both transformations extend to ternary world-dependent plausibility relations.

van Benthem, Fernández-Duque and Pacuit

105

The following result is obvious by the definition of RE and we present it
without proof:
Theorem 3.2 Given any evidence model M and any formula ϕ,[[ϕ]]M∗ = [[ϕ]]M .
Further, it is immediate that if M is uniform then so is M∗ . Flatness is alsopreserved by this operation; if w E X, thenT use Zorn’s lemma to extend {X}T
to a w-scenario X . Then, if M is flat, X 6= ∅, and hence for any v ∈ X
we have that w RE v ∈ X.
Thus every (flat, uniform) evidence model can be represented as a (flat,
uniform) extended evidence model. The opposite is true as well, but a bit
more subtle. For this, we first recall the definition of a p-morphism:
Definition 3.3 Given extended evidence models M1 = hW1 , R1 , E1 , V1 i andM2 = hW2 , R2 , E2 , V2 i, we say a function π : W1 → W2 is a p-morphism if thefollowing conditions hold:atoms V1 = π −1 V2forthR if w R1 v then π(w) R2 π(v)backR if π(w) R2 u then there is v ∈ π −1 (u) such that w R1 v
forthE if w E1 X then there is Y ⊆ W2 such that π(w) E2 Y and π[X] = Y
backE if π(w) E2 Y then there is X such that π[X] = Y and w E1 X
Then we obtain the following familiar result which we present without proof:
Theorem 3.4 If π is a p-morphism between extended evidence models M1 andM2 and ϕ is any formula, then[[ϕ]]M1 = π −1 [[[ϕ]]M2 ].
If a surjective p-morphism exists from M1 to M2 , we will write M1  M2 .
Our goal is to show now that, given an extended evidence model M, there isan evidence model M+ such that M+  M; or, more precisely, (M+ )∗  M.
Thus an extended evidence model may also be represented as a p-morphic
image of an evidence model. The latter evidence model, however, is oftenmuch larger.
Definition 3.5 Given a extended evidence model M = hW, R, E, V i, we define
an evidence model M+ = hW + , E + , V + i and a map π : W + → W as follows:(i) W + is the set of all triples hw, X, ni such that X ⊆ W and either(a) X is flat and n ∈ {0, 1} or(b) X is not flat and n ∈ N.
(ii) π(hw, X, ni) = w(iii) V + (p) = π −1 [V (p)]S(iv) E + (hw, X, ni) = wEY B Y (w) ∪ {W + }, where106

Evidence Logic: A New Look at Neighborhood Structures(a) if Y is flat for w, then B Y (w) = {U0 , U1 }, with
Ui = {hv, Y, 0i |there is a v with w R v and v ∈ Y }∪{hv, Y, ii |v ∈ Y } ;(b) if Y is not flat for w, then B Y (w) = {Vn }n∈N , where
VN = {hv, Y, ni | v ∈ Y, n ≥ N } .
As a simple example, consider two extended evidence models, M1 =hW, R, E, V i and M2 = hW, R0 , E, V i, so that the two are very similar, differing only on the accessibility relation. Suppose that W = {w}, w R w but
R0 = ∅, and E(w) = {W }. The valuations are not too important for thisexample, so we may assume V ≡ ∅.
+++Then, M1 is flat, but M2 is not. Thus we have that M+
1 = hW1 , E1 , V1 i,+
where W1 consists of two copies of w (hw, W, 0i and hw, W, 1i, but let us
call them w0 , w1 for simplicity). Both points have the same evidence sets,
namely {w0 } and {w0 , w1 }; thus the only scenario is {w0 }, {w0 , w1 } which
has intersection {w0 }.
Meanwhile, M+
2 consists of countably many copies of w (of the form
hw, W, ni, but let us call them wn ) and is isomorphic to the model M∞ usedin the proof of Corollary 2.7. As we saw then, the only scenario on M+
2 has
empty intersection.
More generally, it is always the case that flat, finite extended evidence
models give rise to finite models, and uniform extended evidence models giverise to uniform evidence models:Lemma 3.6 If M is flat and finite, then M+ is finite. Further, if M is uniform, then so is M+
Proof. If all evidence sets are flat, we have W + = W × ℘(W ) × {0, 1}, which
is a finite set (provided W is finite).
The second claim is easy to check using the definition of E + .
2
The following key lemma shows a close relationship between the accessibility
relations on M and (M+ )∗ .
Lemma 3.7 Let M = hW, R, E, V i be a extended evidence model with associated evidence model M+ . Let α ∈ W + and v ∈ W be arbitrary.
Then, π(α) R v if and only if there is β ∈ π −1 (v) such that α RE + β.
The proof can be found in Appendix A. With this one can check that π isa p-morphism and (M+ )∗  M:Theorem 3.8 If M is an extended evidence model and π is the associated map
for M+ , then π is a surjective p-morphism between (M+ )∗ and M.
Proof. The atoms clause holds by the definition of V + and the clauses for R
hold by Lemma 3.7.
It remains to check that forthE and backE hold as well.

van Benthem, Fernández-Duque and Pacuit107

To check that forthE holds, note that neighborhoods of α = hw, X, ni are
all of the form
N = {hv, Y, mi : v ∈ Y and w E Y };but then, π[N ] = Y and hence π(α) = w E Y .
Meanwhile, backE holds because if w E Y and π(α) = w, we note thatα E N , where
N = Y × {Y } × {0}2and π[N ] = Y .
Corollary 3.9 Given a extended evidence model M with map π : W
and a formula ϕ ∈ L0 , [[ϕ]]M+ = π −1 [[[ϕ]]M ].
Proof. Immediate from Theorems 3.8 and 3.4.

+

→W
2

From this we obtain the following, very useful result:
Theorem 3.10 A set of formulas Φ is satisfiable on a (flat, uniform) extended
evidence model if and only if it is satisfiable on a (flat, uniform) evidence model.

4CompletenessIn view of the previous section, it suffices to build extended evidence models forconsistent sets of formulas in order to prove completeness. Extended evidence
models are much closer to standard semantics of modal logic than evidence
models and hence we can apply familiar techniques.
We assume that all formulas are in ‘negation-normal form’ in which negations are only applied to propositional variables. Of course, in order to do thisb A)
b to appear. Henceforth, we assume
we must allow for dual operators (3, B,
all formulas are in this form unless we explicitly indicate otherwise. Note that
this convention is only for the sake of exposition, as we allow negation in our
calculus and dual operators are really abbreviations.
We denote the normal-form negation of ϕ by ∼ ϕ. The closure of ϕ, denoted cl(ϕ) contains all subformulas of ϕ, is closed under normal-from negation(if ψ ∈ cl(ϕ) then ∼ ψ ∈ cl(ϕ)), and we stipulate that
S >, 2>, 3> and B> are
all in cl(ϕ). If Ω is a set of formulas, then cl(Ω) = {cl(ϕ) | ϕ ∈ Ω}. As usual,the states in our canonical extended evidence model are maximally consistentsets of formulas (which we call types).
In the remainder of this paper, by an evidence logic we will mean exclusively
an element of {Log, Log[ , Logu , Log[u }.
Definition 4.1 Let Ω be a set of formulas and λ an evidence logic. An (Ω, λ)type is a maximal λ-consistent subset of cl(Ω).
A set of formulas Γ is a λ-type if it is a (Γ, λ)-type, i.e., Γ is λ-consistentand for each ψ ∈ cl(Γ), either ψ ∈ Γ or ∼ ψ ∈ Γ.
Note that (Ω, λ)-types may be finite or infinite, depending on whether Ω is.
We denote the set of (Ω, λ)-types by typeλ (Ω). Given an (Ω, λ)-type Φ, defineΦA as {ψ | Aψ ∈ Φ}, and similarly for the other modalities.

108

Evidence Logic: A New Look at Neighborhood Structures

Of course, in a given model all points must satisfy the same universal formulas, so it is convenient to consider the collection of all such types.
b Ab; if
Given a set of formulas Γ, if λ ∈ {Log, Log[ }, define Γλ = AΓA ∪ AΓ
λ ∈ {Logu , Log[u }, define[b B, B,b 2, 3}.
Γλ = { Γ := A, A,
Definition 4.2 Given a λ-type Φ, we defineλλ(i) typeAλ (Φ) to be the set of all (Φ, λ)-types Ψ such that Ψ = Φ ;AB(ii) typeBλ (Φ) = Ψ ∈ typeλ (Φ) | Φ ⊆ Ψ .

Now we need to define evidence sets on our extended evidence models.
Definition 4.3 Given a λ-type Φ with 2α ∈ Φ, we define the α-neighborhoodof Φ asNλα (Φ) = Ψ ∈ typeA
λ (Φ) | α ∈ Ψ .
We are now ready to define a canonical extended evidence model :Definition 4.4 Let Φ be a λ-type. The λ-canonical extended evidence
model for Φ is the extended evidence model Mλ (Φ) = WλΦ , EλΦ , RλΦ , VλΦ
where(i) WλΦ = typeAλ (Φ)(ii) For each p ∈ At ∩ Γ, Γ ∈ VλΦ (p) iff p ∈ Γ,(iii) EλΦ (Γ) = {Nλα (Γ) | 2α ∈ Γ} .
B(iv) Γ RλΦ ∆ iff ∆ ∈ typeBλ (Γ) (i.e., Γ ⊆ ∆).

Note that our ‘canonical’ extended evidence models are not unique as they
depend on the type Φ we wish to satisfy and the logic λ we wish to work in;in this sense they could be considered ‘semicanonical’. Considering different
extended evidence models is unavoidable, given that our language includes auniversal modality and it is impossible to satisfy all types on a single model.
However, we are also taking advantage of this in order to obtain the finite(extended) model property directly, since canonical extended evidence models
for finite types are themselves finite.
Let us observe that canonical models for uniform types are uniform:
Lemma 4.5 If λ ∈ {Logu , Log[u } and Φ is λ-consistent, then the model Mλ (Φ)
is uniform.
Proof. Given Ψ ∈ WλΦ , we have that both the accessible states and the neighborhoods of Ψ depend only on Ψλ , which is constant amongst all of WλΦ . 2
Our goal will now be to prove a version of the Truth Lemma which will
imply that the canonical extended evidence model s we have defined satisfy theright formulas. For this, we need some preliminaries. We start by gathering themain results about the axiom system that we use to prove the Truth Lemma.
We defer proofs to the Appendix.

van Benthem, Fernández-Duque and Pacuit109

Lemma 4.6 Let Γ, ∆ be sets of formulas and λ an evidence logic.
b `λ ψ. Then, 2ϕ, AΓ, A∆b `λ 2ψ.
(i) Suppose that ϕ, AΓ, A∆b `λ ψ. Then, BΦ, AΓ, A∆b `λ Bψ.
(ii) Suppose that Φ, AΓ, A∆
It will be very useful to draw some dual conclusions from the above result.
Lemma 4.7 Let Γ be a set of formulas and λ an evidence logic.
(i) If Γ is λ-consistent, α ∈ Γ2 and δ ∈ Γ3 , then {α, δ} ∪ Γλ is λ-consistent.
(ii) If Γ is λ-consistent and ψ ∈ ΓB , then {ψ} ∪ ΓB ∪ Γλ is λ-consistent.
b(iii) If λ ∈ {Log[ , Log[u }, Γ is λ-consistent and ψ ∈ Γ2 , then {ψ} ∪ ΓB ∪ Γλ is
λ-consistent.
The next lemmas show the key steps in the proof of the Truth Lemma.
Lemma 4.8 Let Γ be a (Φ, λ)-type.
(i) If 2α, 3β ∈ Γ, there is ∆ ∈ Nλα (Γ) with β ∈ ∆.
(ii) If λ ∈ {Log[ , Log[u } and α ∈ Γ2 , then Nλα (Γ) ∩ typeBλ (Γ) is non-empty.
b ∈ Γ. Then, there is ∆ ∈ typeB (Γ) with β ∈ ∆.
(iii) Suppose that Bαλ

The proofs of the above three lemmas can be found in Appendix B. For
what follows, it will be convenient to flesh out some of the model-theoretic
consequences of Lemma 4.8.
Lemma 4.9 Given a λ-type Φ with a λ-canonical extended evidence modelMλ (Φ) = WλΦ , RλΦ , EλΦ , VλΦ ,(i) for each Γ ∈ WλΦ , Γ EλΦ WλΦ ;(ii) if 2α ∈ Φ, Nλα (Φ) is non-empty; and(iii) if Φ is flat and Γ EλΦ X, there is ∆ ∈ X such that Γ RλΦ ∆.
Proof. Suppose Γ is a (Φ, λ)-type and let Mλ (Φ) be as above.
(i) Recall that we stipulated that 2>, > ∈ cl(Φ), and these formulas are valid
so it follows that > ∈ ∆ for all ∆ ∈ WλΦ ; thus Nλ> (Φ) = WλΦ . Similarly,
2> ∈ Γ, so that Γ EλΦ WλΦ , as claimed.
(ii) Put β = > in Lemma 4.8(i).
(iii) Immediate from the definition of the accessibility relation and neighborhoods on canonical extended evidence models and Lemma 4.8(ii).
2
Putting everything together, we have:
Corollary 4.10 If λ is an evidence logic and Φ is λ-consistent, then Mλ (Φ)
is a extended λ-evidence model.
Proof. From Lemma 4.9(i) we see that, given Γ ∈ WλΦ , Γ E WλΦ , while from
Lemma 4.9(ii) we obtain Γ 6E ∅. It follows that Mλ (Φ) is a extended evidence
model.

110

Evidence Logic: A New Look at Neighborhood Structures

If further we have that λ ∈ {Log[ , Log[u }, by Lemma 4.9(iii), every neighborhood on Mλ (Φ) is flat, i.e., Mλ (Φ) is flat.
Finally, if λ ∈ {Logu , Log[u }, we use Lemma 4.5 to see that the modelMλ (Φ) is uniform.
2
We are now ready to prove our own version of the ‘Truth Lemma’:
Proposition 4.11 (Truth Lemma) For every formula ψ ∈ cl(Φ) and every
set Γ ∈ typeA
λ (Φ),ψ ∈ Γ ⇒ Γ ∈ [[ψ]]Mλ (Φ) .
Proof. The proof is by induction on the structure of ψ. The only interestingcases are the modalities 2 and B (and their duals).
Suppose first that 2ψ ∈ Γ, and let X = Nλψ (Γ). By definition, we haveψ ∈ Θ for every Θ ∈ X, and by the induction hypothesis this implies that foreach Θ ∈ X, Θ ∈ [[ψ]]Mλ (Φ) . Thus, X is a neighborhood of Γ (X ∈ E Φ (Γ))
with X ⊆ [[ψ]]Mλ (Φ) , and so, Γ ∈ [[2ψ]]Mλ (Φ) , as desired.
Now, assume that 3ψ ∈ Γ. Let X be any neighborhood of Γ. Then
X = N α (Γ) for some α. Hence, 2α ∈ Γ and 3ψ ∈ Γ. By Lemma 4.8.1, thereis Θ ∈ N α (Γ) with ψ ∈ Θ. By the induction hypothesis, Θ ∈ [[ψ]]Mλ (Φ) , and,since X was arbitrary, we conclude that Γ ∈ [[3ψ]]Mλ (Φ) .
Assume that Bψ ∈ Γ. Now, suppose that ΓRλΦ ∆. Then, by definitionψ ∈ ∆, which by the induction hypothesis implies ∆ ∈ [[ψ]]Mλ (Φ) . Thus,Γ ∈ [[Bψ]]Mλ (Φ)
b ∈ Γ. By Lemma 4.8.3, ψ ∈ Θ for some Θ ∈ typeB (Γ).
Assume that Bψλb M (Φ) .
But then Γ RλΦ Θ, and thus Γ ∈ [[Bψ]]2λ4.1 Proof of the Main Theorem
With the work developed in previous sections, we are ready to state and prove
our main results.
Theorem 4.12 Each evidence logic λ is sound and strongly complete both forthe class of λ-evidence models and the class of extended λ-evidence models.
Proof. Let Φ be λ-consistent and let Mλ (Φ) be the canonical extended evidence model for Φ. By Corollary 4.10, Mλ (Φ) is a λ-extended evidence model,and Φ can be extended to a (Φ, λ)-type Γ. By Proposition 4.11, given ϕ ∈ Γ,Γ ∈ [[ϕ]]Mλ (Φ) , so that Φ is satisfiable in Mλ (Φ).
By Lemma 3.9, (M(Φ))+ is a λ-model also satisfying Φ.
2Theorem 4.13 The flat evidence logics Log[ , Log[u have the finite model prop`
erty. In fact, if ϕ has length `, then it has a λ-model of size at most 10 2` ·22 ·2.
Non-flat evidence logics do not have the finite model property, but they dohave the finite extended evidence model property.
Proof. If ϕ is λ-consistent, we can extend it to a ({ϕ} , λ)-type Φ and let M
be the canonical extended λ-evidence model for Φ. Clearly, M has at most 2`
states, where ` is the length of ϕ, and thus it is finite.
10 This bound could be improved to 2` · ` · 2.

van Benthem, Fernández-Duque and Pacuit111

If ϕ is further [-consistent, then the model M+ is finite as well, and it has`
at most 2` · 22 · 2 points.
2
Corollary 4.14 Both flat and general evidence logic are decidable.
Our analysis does not yield the exact computational complexity of deciding validity or satisfiability. Note however that the general evidence logic is aconservative extension of Ku (i.e., K with a universal modality) and hence thevalidity problem is ExpTime-hard; the same should be true of Log[ . Meanwhile, we expect the uniform logics to be much simpler, as they extend S5
rather than K, but do not have a specific conjecture on their complexity.

5

Language Extensions

The logical systems studied in the previous sections are interesting in their own
right as they combine features of both normal and non-normal modal logics. An
additional appealing feature of the logical systems studied here and in [21] is the
fresh new interpretation of neighborhood structures. In particular, interpretingneighborhoods as bodies of evidence suggests a number of new and interesting
modalities beyond the usual repertoire studied in modal neighborhood logics.
In this section, we briefly explore this rich landscape of extensions of our basic
language, and point out some resulting problems of axiomatization.
Two operators that immediately suggest themselves in anticipation of the
dynamic extensions found in [21] are conditional versions of our evidence andbelief operators. The conditional belief operator (B ϕ ψ: “the agent believes ψ
conditional on ϕ”) is well-known, but is given a new twist in our setting. Someof the agent’s current evidence may be inconsistent with ϕ (i.e., disjoint with[[ϕ]]M ). If one is restricting attention to situations where ϕ is true, then suchinconsistent evidence must be “ignored”. Here is how we do this:Definition 5.1 (Relativized maximal overlapping evidence.) Supposethat X ⊆ W . Given a collection X of subsets of W (i.e., X ⊆ ℘(W )), therelativization of X to X is the set X X = {Y ∩ X | Y ∈ X }. We say that acollection X of subsets of W has the finite intersection
property relativeTto X (X-f.i.p.) if, for each {X1 , . . . , Xn } ⊆ X X , 1≤i≤n Xi 6= ∅. We say that
X has the maximal X-f.i.p. if X has X-f.i.p. and no proper extension X 0 of
X has the X-f.i.p.
To simplify notation, when X is the truth set of formula ϕ, we write “maximal ϕ-f.i.p.” for “maximal [[ϕ]]M -f.i.p.” and “X ϕ ” for “X [[ϕ]]M ”. Now we definea natural notion of conditional belief:
T ϕ• M, w |= B ϕ ψ iff for each maximal ϕ-f.i.p. X ⊆ E(w), for each v ∈X ,M, v |= ψThis notion suggests a logical investigation beyond what we have provided
so far. First of all, strikingly, Bϕ → B ψ ϕ is not valid. One can compare thisto the failure of monotonicity for antecedents in conditional logic. In our moregeneral setting which allows inconsistencies among accepted evidence, we also
see that even the following variant is not valid: Bϕ → (B ψ ϕ ∨ B ¬ψ ϕ). To see

112

Evidence Logic: A New Look at Neighborhood Structures

this, consider an evidence model with E(w) = {X1 , Y1 , X2 , Y2 } where the setsare defined as follows:¬p, ¬q

p, q

X1

Y1
p, ¬q

X2

p, ¬q

¬p, q

¬p, ¬qY2

Then, M, w |= Bq; however, M, w 6|= B p q ∨ B ¬p q. This is interesting as it
is valid on connected plausibility models for conditional belief (cf. [2] for acomplete modal logic of conditional belief on such models). Extending ourcompleteness proof from the previous section requires new ideas as there is no
obvious way to interpret conditional belief operators on our auxiliary “extended
evidence models”.
The conditional evidence operator 2ϕ ψ (“the agent has evidence that ψ istrue conditional on ϕ being true”) is a new modality on neighborhoods. We
say that X ⊆ W is consistent (compatible) with ϕ if X ∩ [[ϕ]]M 6= ∅. Truthof conditional evidence can then be defined as follows:•

M, w |= 2ϕ ψ iff there exists an evidence set X ∈ E(w) which is consistent
with ϕ such that for all worlds v ∈ X ∩ [[ϕ]]M , M, v |= ϕ.

In particular, if there is no evidence consistent with ϕ, then 2ϕ ψ is false.
This, in turn means that 2ϕ ψ is not equivalent to 2(ϕ → ψ). 11 Indeed,a simple bisimulation argument shows that no definition exists for conditional
evidence in the language with absolute evidence and belief. The conditional
evidence operators satisfy the monotonicity inference rule (from ϕ → ψ infer
2α ϕ → 2α ψ) and, for example, the axiom scheme 2α ϕ → 2α α; however, acomplete logic will be left for future work.
Both of these operators are special cases of more general modalities thatwere discovered in [21] as static counterparts to natural dynamic modalities ofadding or removing evidence.
For the conditional evidence operator 2ϕ ψ, we can require the witnessing evidence set to be “compatible” with a sequence of formulas. Let ϕ =(ϕ1 , . . . , ϕn ) be a finite sequence of formulas. We say that a set of states X
is compatible with ϕ provided that, for each formula ϕi , X ∩ [[ϕi ]]M 6= ∅.
Then, we define the general conditional evidence operator 2α
ϕ ψ as follows:•

M, w |= 2αϕ ψ iff there is X ∈ E(w) compatible with ϕ, α such thatX ∩ [[α]]M ⊆ [[ψ]]M .

11 To see this, consider a model where ϕ is false at all worlds. Then 2ϕ ψ is also false at all
worlds, but 2(ϕ → ψ) will be true at all worlds, since ϕ → ψ is true everywhere.

van Benthem, Fernández-Duque and Pacuit

113

The conditional belief operator can be generalized in two ways. The firstway is to incorporate the above notion of compatibility with a sequence of formulas. The intended interpretation of Bγϕ ψ is “the agent believes χ conditionalon ϕ assuming compatibility with each of the γi ”. The formal definition is astraightforward generalization of the earlier definition of B ϕ ψ. A maximal f.i.p.
set X is compatible with a sequence of formulas ϕ provided for each X ∈ X ,X is compatible with ϕ. Then,•

M, wT|= Bϕα ψ iff for each maximal α-f.i.p. X compatible with ϕ, we havethat X α ⊆ [[ψ]]M .

The second generalization focuses on the conditioning operation. Note thatB ϕ ψ may be true at a state w without having
any w-scenarios that imply ϕT(i.e., there is no w-scenario X such that X ⊆ [[ϕ]]M ). A more general formof conditioning is B ϕ,α ψ where “the agent believe ψ, after having settled on α
and conditional on ϕ”. Formally,T• M, w |= B ϕ,ψ χ iff for all maximally ϕ-compatible sets X ⊆ E(w), ifX∩
T[[ϕ]]M ⊆ [[ψ]]M , then X ∩ [[ϕ]]M ⊆ [[χ]]M .
Note that B +ϕ can be defined as B ϕ,> .
This splitting of notions shows that neighborhood structures are a goodvehicle for exploring finer epistemic and doxastic distinctions than those foundin standard relational models for modal logic. Moreover, they support interesting matching forms of reasoning beyond standard axioms. Validities include interesting connections between varieties of conditional belief such as:
B ϕ ψ → B(ϕ → ψ) and B(ϕ → ψ) → B >,ϕ ψ.
At the same time, this richness means that new techniques may be neededin the logical analysis of this richer form of neighborhood semantics. Modeltheoretically, we need stronger notions of bisimulation and -morphism matchingthese more expressive languages, while proof-theoretically, we need to lift ourearlier completeness technique to this setting.

6

Conclusion and Future Work

There are two main contributions in this paper. First, our completeness theorems solve an important problem left open in [21] contributing to the general
study of basic evidence logic and its dynamics. Second, in doing so, we develop a new perspective on neighborhood models that suggests extensions of
the usual systems. For the modal logician, the pleasant surprise of our language
extensions is that there is a lot of well-motivated new modal structure to be
explored on these simple models.
Clearly, many open problems remain. These start at the base level of the
motivations for our framework, touched upon lightly earlier on. For instance,
our framework still needs to be related to other modal logics of evidence [18,5],
justification [1] and argumentation [4]. Here are a few more specific technicalavenues for future research:114

Evidence Logic: A New Look at Neighborhood Structures•

Further interpretations: By imposing additional constraints on the evidence
relations (i.e., the neighborhood functions), we get evidence models thatare topological spaces. Can we give a spatial interpretation to our belief
operator and the new modalities discussed in Section 5? This suggests new,richer spatial logics for reasoning about topological spaces (cf. [20]).

•

Computational complexity: Neighborhood logics are often NP-complete,
while basic modal logics on relational models are often Pspace-complete.
What about mixtures of the two? By Corollary 4.14 we know that the validity problem for flat and general evidence logic is decidabile. What is theprecise complexity?

•

Extended model theory: Combining existing notions of bisimulation for relational models and neighborhood models takes us only so far. What new
notions of bisimulation directly on evidence models will match our extended
modal languages? And in this setting, can the key representation method of
this paper (cf. Theorem 3.8) be extended to deal with such richer languages,
perhaps starting from richer extended evidence models carrying plausibility
relations?

•

Extended proof theory: How can we axiomatize the richer modal logic ofneighborhood models that arises in Section 5? Will modifying existing techniques, including our approach in this paper, still work, or do we need a newstyle of analysis of canonical models?

Appendix
A Proof from Section 3
Lemma A.1 (Lemma 3.7) Let M = hW, R, E, V i be a extended evidence
model with associated evidence model M+ . Let α ∈ W + and v ∈ W be arbitrary.
Then, π(α) R v if and only if there is β ∈ π −1 (v) such that α RE + β.
Proof. Assume that α ∈ W + and π(α) = w. We first claim that every αscenario on M+ is of the form B Y (α) ∪ {W + }.
For this, suppose that α E + X and α E + Y with X ∩ Y 6= ∅ and X, Y 6=+
W . This means that there is a hv, Z, ni ∈ X ∩ Y . By inspecting the definitionof E + , this implies X, Y ∈ B Z (α). Hence, any collection X ⊆ E + (α) with thefinite intersection property must be contained in B Z (α) ∪ {W + } for some Z.
Meanwhile, it is easy to see that for every Z ⊆ W , B Z (α) ∪ {W + } alreadyhas the fip (by case-by-case inspection), hence everyTscenario is of this form.
Now, if Y is not flat forTw, one can check that B Y (w) = ∅. If Y is flatfor w, then all elementsTof B Y (w) are of the form hv, Y, 0i with w R v andv ∈ Y . In either case, π[ B Y (w)] ⊆ R(w). It follows that, whenever α RE + β,then w R π(β).
It is also straightforward to see that\
B W (w) = R(w) × {W } × {0} ,van Benthem, Fernández-Duque and Pacuit

115

T
so that π[ B W (w)] = R(w). Thus, if w R v thenT there is an α-scenario U(namely U = B W (w) ∪ {W + }) with hv, W, 0i ∈U, so that α RE + β =hv, W, 0i.
2

B

Proofs from Section 4

Lemma B.1 (Lemma 4.6) Let Γ, ∆ be sets of formulas.
b `λ ψ. Then, 2ϕ, AΓ, A∆b `λ 2ψ.
(i) Suppose that ϕ, AΓ, A∆b `λ ψ. Then, BΦ, AΓ, A∆b `λ Bψ.
(ii) Suppose that Φ, AΓ, A∆
Without loss of generality we can assume Γ, ∆, Φ to be finite, since in general
we have that Θ `λ α if and only if for some finite Θ0 ⊆ Θ, Θ0 `λ α.
Proof. Note that
^

AΓ ∧

^

b ↔A
A∆

^

AΓ ∧

^

b
A∆



b by a single formula Aγ.
is derivable in S5, so we can replace AΓ, A∆(i) If ϕ, Aγ `λ ψ, then`λ ϕ ∧ Aγ → ψ.
By the monotonicity rule`λ 2 (ϕ ∧ Aγ) → 2ψ.
Applying the pullout axiom we get`λ 2ϕ ∧ Aγ → 2ψ,that is,2ϕ, Aγ `λ 2ψ.
(ii) If Φ, Aγ `λ ψ, since B is a normal operator, we also haveBΦ, BAγ `λ Bψ.
But since Aα → BAα is an axiom, we get
BΦ, Aγ `λ Bψ.

2bAb , while
Below, recall that, if λ ∈ {Log, Log[ }, we defined Γλ = AΓA ∪ AΓif λ ∈ {Logu , Log[u },[b B, B,b 2, 3}.
Γλ = { Γ := A, A,
Lemma B.2 (Lemma 4.7) Let Γ be a set of formulas.
(i) If Γ is λ-consistent, α ∈ Γ2 and δ ∈ Γ3 , then {α, δ} ∪ Γλ is λ-consistent.
(ii) If Γ is λ-consistent and ψ ∈ ΓB , then {ψ} ∪ ΓB ∪ Γλ is λ-consistent.
b116

Evidence Logic: A New Look at Neighborhood Structures(iii) If λ is flat, Γ is λ-consistent and ψ ∈ Γ2 , then {ψ} ∪ ΓB ∪ Γλ is λconsistent.
Proof. Assume Γ is λ-consistent.
Note that we have Γλ ≡ AΓλ independently of λ; over the non-uniformb → AAϕ,b while over the uniform case (i.e.,case, this follows from the axiom Aϕ
if λ ∈ {Logu , Log[u }), this is because Γ is equivalent to A Γ over λ forany modality .
λAs before, we may assume
V λΓ is finite. Thus we may replace Γ by a single
formula Aγ equivalent to Γ over λ.
(i) Suppose otherwise. Then, we would haveα, Aγ `λ ¬δ.
Thus by Lemma 4.6.1,
2α, Aγ `λ 2¬δ,so that{¬2¬δ, 2α, Aγ}
is λ-inconsistent. But this is a subset of Γ, contradicting our assumptionthat Γ is λ-consistent.
(ii) Suppose ψ ∈ ΓB . If the claim was false, then we would haveb

ΓB , Aγ `λ ¬ψ,and hence, by Lemma 4.6.2,
BΓB , Aγ `λ B¬ψ.
Thus{¬B¬ψ, Aγ} ∪ BΓB
would be λ-inconsistent. If ψ ∈ ΓB , this contradicts the consistency of Γ.
b(iii) If ψ ∈ Γ2 , the claim follows from item 2 above using the axiom 2ψ → Bψ.
2b

Lemma B.3 (Lemma 4.8) Let Γ be a (Φ, λ)-type.
(i) If 2α, 3β ∈ Γ, there is ∆ ∈ Nλα (Γ) with β ∈ ∆.
(ii) If λ ∈ {Log[ , Log[u } and α ∈ Γ2 , then Nλα (Γ) ∩ typeBλ (Γ) is non-empty.
Bb ∈ Γ. Then, there is ∆ ∈ type (Γ) with β ∈ ∆.
(iii) Suppose that Bαλ

Proof. Let Γ be a (Φ, λ)-type (for some λ-consistent set of formulas Φ).
(i) Since Γ is λ-consistent and 2α, 3β ∈ Γ, we have, by Lemma 4.7.1, that{α, β} ∪ Γλis λ-consistent. This can be extended to a Φ-type ∆. Then, by definition
we have ∆ ∈ Nλα (Γ) and β ∈ ∆, as desired.

van Benthem, Fernández-Duque and Pacuit

117(ii) By Lemma 4.7.3, if Γ is λ-consistent and λ is flat, then {α} ∪ ΓB ∪ Γλ is
λ-consistent as well, and hence can be extended to a Φ-type ∆. Obviously,∆ ∈ Nλα (Γ) ∩ typeBλ (Γ).
(iii) By Lemma 4.7.2, since Γ is λ-consistent, we have that{β} ∪ ΓB ∪ Γλis λ-consistent as well. Thus, it can be extended to a Φ-type ∆. Evidently,∆ ∈ typeBλ (Γ) and β ∈ ∆.
2

References[1] Artemov, S. and E. Nogina, Introducing justification into epistemic logic, Journal of
Logic and Computation 15 (2005), pp. 1059–1073.
[2] Board, O., Dynamic interactive epistemology, Games and Economic Behavior 49 (2004),
pp. 49–80.
[3] Gärdenfors, P., “Knowledge in Flux: Modeling the Dynamics of Epistemic States,”
Bradford Books, MIT Press, 1988.
[4] Grossi, D., On the logic of argumentation theory, in: W. van der Hoek, G. Kaminka,
Y. Lesperance, M. Luck and S. Sandip, editors, Proceedings of the 9th International
Conference on Autonomous Agents and Multiagent Systems (AAMAS’10), 2010, pp.
409–416.
[5] Halpern, J. and R. Pucella, A logic for reasoning about evidence, Journal of AI Research
26 (2006), pp. 1–34.
[6] Hansen, H. H., “Monotonic Modal Logic,” Master’s thesis, Universiteit van Amsterdam(ILLC technical report: PP-2003-24) (2003).
[7] Hansen, H. H., C. Kupke and E. Pacuit, Neighbourhood structures: Bisimilarity andbasic model theory, Logical Methods in Computer Science 5 (2009), pp. 1–38.
[8] Horty, J. F., Reasons as defaults, Philosophers’ Imprint 7 (2007), pp. 1–28.
[9] Kratzer, A., What must and can must and can mean, Linguistics and Philosophy 1(1977), pp. 337–355.
[10] Lismont, L. and P. Mongin, A non-minimal but very weak axiomatization of common
belief, Artificial Intelligence 70 (1994), pp. 363–374.
[11] List, C. and F. Dietrich, Reasons for (prior) belief in bayesian epistemology (2012),
unpublished manuscript.
[12] Pacuit, E., Neighborhood semantics for modal logic: An introduction (2007), ESSLLI2007 course notes (ai.stanford.edu/~epacuit/classes/).
[13] Parikh, R., The logic of games and its applications, in: M. Karpinski and J. v. Leeuwen,
editors, Topics in the Theory of Computation, Annals of Discrete Mathematics 24,
Elsevier, 1985 pp. 111 – 140.
[14] Pauly, M., A modal logic for coalitional power in games, Journal of Logic andComputation 12 (2002), pp. 149–166.
[15] Peleg, D., Concurrent dynamic logic, Journal of the ACM 34 (1987), pp. 450–479.
URL http://doi.acm.org/10.1145/23005.23008[16] Rott, H., “Change, Choice and Inference: A Study in Belief Revision and Nonmonotonic
Reasoning,” Oxford University Press, 2001.
[17] Segerberg, K., “An Essay in Classical Modal Logic,” Filosofisska Stuier, Uppsala
Universitet, 1971.
[18] Shafer, G., “A Mathematical Theory of Evidence,” Princeton University Press, 1976.

118

Evidence Logic: A New Look at Neighborhood Structures[19] van Benthem, J., “Logical Dynamics of Information and Interaction,” Cambridge
University Press, 2011.
[20] van Benthem, J. and G. Bezhanishvili, Modal logics of space, in: M. Aiello, I. PrattHartmann and J. van Benthem, editors, Handbook of Spatial Reasoning, 2007, pp. 217–
298.
[21] van Benthem, J. and E. Pacuit, Dynamic logics of evidence-based beliefs, Studia Logica
99 (2011), pp. 61–92.
[22] Vardi, M., On epistemic logic and logical omniscience, in: J. Halpern, editor, Theoretical
Aspects of Reasoning about Knowledge: Proceedings of the 1986 Conference (1986), pp.
293–305.
[23] Veltman, F., Prejudices, presuppositions and the theory of conditionals, in:J. Groenendijk and M. Stokhof, editors, Amsterdam Papers in Formal Grammar (1976),
pp. 248–281.
[24] Zvesper, J., “Playing with Information,” Ph.D. thesis, ILLC University of Amsterdam
Dissertation Series DS-2010-02 (2010).