Mohua Banerjee

Didier Dubois

A simple logic for reasoning about incomplete knowledge

The semantics of modal logics for reasoning about belief or knowledge is often described in terms of accessibility relations, which is too expressive to account for mere epistemic states of an agent. This paper proposes a simple logic whose atoms express epistemic attitudes about formulae expressed in another basic propositional language, and that allows for conjunctions, disjunctions and negations of belief or knowledge statements. It allows an agent to reason about what is known about the beliefs held by another agent. This simple epistemic logic borrows its syntax and axioms from the modal logic KD. It uses only a fragment of the S5 language, which makes it a two-tiered propositional logic rather than as an extension thereof. Its semantics is given in terms of epistemic states understood as subsets of mutually exclusive propositional interpretations. Our approach offers a logical grounding to uncertainty theories like possibility theory and belief functions. In fact, we define the most basic logic for possibility theory as shown by a completeness proof that does not rely on accessibility relations.

Motivation

Reasoning about knowledge and beliefs requires more than the language of classical propositional logic. In the syntax of classical propositional logic, it is only possible to express that certain propositions are known or believed. A set of logical formulae is then often called a knowledge base, or a belief base [START_REF] Nebel | Belief revision and default reasoning: syntax-based approaches[END_REF], and when it is deductively closed, a belief set [START_REF] Gärdenfors | Knowledge in Flux[END_REF]. The latter is used in belief revision for representing the dynamics of knowledge upon receiving new information. However, stating that some propositions are acknowledged as being unknown to an agent requires the use of a more expressive language, since the language of classical propositional logic cannot really express the difference between statements like "not knowing α" and "knowing not α" (in fact it can only express the latter as ¬α). This distinction can only be made in the metalanguage (interpreting believing or knowing as proving [START_REF] Dubois | Possibility theory, probability theory and multiple-valued logics: A clarification[END_REF]). In modal logic, the first statement writes ¬✷α, and the second one is ✷¬α. This kind of syntax is used in epistemic logic [START_REF] Hintikka | Knowledge and Belief[END_REF][START_REF] Halpern | Reasoning About Knowledge[END_REF], but the usual semantics in terms of accessibility relations, often motivated by the modeling of introspection, does not easily fit with uncertainty formalisms like probability or possibility theories, that rely on weights assigned to possible worlds. Kripke semantics are better tailored for other applications such as temporal logic.

The aim of this paper is to define a minimal language that makes it possible to reason about partial information provided by a logically sophisticated agent. A set of formulae in this language represents what an agent can sincerely reveal about his or her knowledge or beliefs. An agent is viewed here as a source of information, or a witness. In this language, atomic propositions are expressed as ✷α, where α is any formula from a propositional language and ✷, expressing belief * Corresponding author at: IRIT, CNRS Université de Toulouse, France.

or knowledge, 1 is borrowed from modal logics. The language is then completed by means of classical negation and conjunction. However, the nesting of modalities is not allowed because we are not concerned with introspective nor multiagent reasoning. The obtained language is an elementary fragment of well-known modal systems. This "minimal epistemic logic" can also be understood as a meta-epistemic logic (MEL) since we take an imperfect external point of view on the agent knowledge, in the sense of Aucher [START_REF] Aucher | An internal version of epistemic logic[END_REF].

At the semantic level, we use the simplest basic representation of incomplete information common to all uncertainty theories. Incomplete knowledge about the real world possessed by an agent will be represented just by a non-empty subset of interpretations, one and only one of which is, according to this agent's beliefs, 2 the actual state of the world. This is what is usually called an epistemic state. Moreover, all that is known about the agent's epistemic state stems from what this agent sincerely reported. So we have incomplete knowledge about this epistemic state (we call it a meta-epistemic state). This kind of representation of higher order incomplete knowledge already exists in uncertainty theories. In Shafer's theory of evidence [START_REF] Shafer | A Mathematical Theory of Evidence[END_REF], a belief function is represented by a probability distribution over epistemic states.

The semantics of the proposed logic is in terms of epistemic states. It does not use full-fledged Kripke-style semantics nor does it evaluate modal formulae on propositional valuations. In this sense MEL, even if syntactically a fragment of a known modal logic, is not really in the spirit of the standard modal logic trend for representing and reasoning about knowledge.

The originality of the paper lies in its concern for a minimal language for reasoning about incomplete information revealed by an agent, the non-Kripke semantics of the system MEL, and the connection between modal logic and uncertainty theories it suggests. In fact, such a link is briefly outlined in a book of Hájek [START_REF] Hájek | The Metamathematics of Fuzzy Logics[END_REF] who developed it with colleagues for probability theory [START_REF] Hájek | Fuzzy logic and probability[END_REF], gradual possibility theory [START_REF] Hájek | On modal logics for qualitative possibility in a fuzzy setting[END_REF] or belief functions [START_REF] Godo | A fuzzy modal logic for belief functions[END_REF] using formal fuzzy logics. The paper considers the simplest Boolean core of such logics, so as to highlight its central role in logics of uncertainty.

The paper 3 is organized as follows. In the next section, the syntax and the axiomatic setting of the logic MEL are provided. The set-valued semantics of the logic is then supplied in Section 3; soundness and a proof of completeness with respect to the intended semantics is established, that relies only on the completeness of propositional logic, and the use of possibility theory. We explain how to encode any set of epistemic models as a MEL-formula. We also show in which sense MEL is a two-tiered propositional logic, rather than a usual modal logic. The relationship to uncertainty theories, like probability, possibility and Shafer's theory of evidence is described in Section 4. It is shown that there is a MEL-formula encoding a single epistemic state, that is the logical counterpart to the Möbius transform of a belief function. The latter can then be viewed as a probabilistic rendering of a meta-epistemic state. In Section 5, some related works are discussed further. Finally, perspectives are outlined in Section 6.

The logic MEL: syntax and axioms

The language of the proposed logic aims at enabling an agent to sincerely provide some information about his or her beliefs on the outside world, so as to enable another agent to reason about it. As hinted in the introduction, in this paper, we interchangeably use the words knowledge and belief, as the formalism is too elementary to make the distinction. Note that while this is in opposition to the philosophical tradition, it is in line with Artificial Intelligence, where the terms "knowledge base" and "belief base" are often used indifferently. Moreover while the philosophic tradition often interprets knowledge as true belief, other authors [START_REF] Moses | Belief as defeasible knowledge[END_REF] consider belief as defeasible knowledge. MEL is essentially a logic for reasoning under uncertainty based on an agent's revealed incomplete information about the world. Whether this information is in conformity with the real world or not is not the point here. Moreover, we exclude introspection from our concerns. The proposed syntax makes it possible to express whether a classical proposition is believed, or unknown to the agent. The information possessed by the agent is said to be incomplete, when the truth of some proposition remains unknown for this agent.

Syntax

Let us consider classical propositional logic PL, with (say) k propositional variables, p 1 , . . . , p k . Let α, β, . . . denote PL-formulae obtained as usual by Boolean connectives ¬, ∧, forming the language L. The main idea of the proposed syntax is to encapsulate PL inside a language equipped with a modality denoted by ✷. This is in contrast with usual epistemic modal logics that extend PL with this additional symbol. The intended purpose here is to completely separate propositions in L referring to the real world and propositions that refer to an agent's epistemic state, where the symbol ✷ appears.

We thus construct atoms of MEL by adding the unary connective ✷ in front of all sentences in L -so atomic formulae of MEL are of the form ✷α, α ∈ L, and form the set At. The intended meaning of ✷α is that an agent knows (or believes) proposition α is true, that is, α holds in every possible world compatible with this agent's epistemic state.

The set of MEL-formulae, denoted by φ, ψ, . . . forms a propositional language L ✷ generated recursively from the set At of atomic formulae, with the help of the same Boolean connectives ¬, ∧:

✷α ∈ L ✷ , whenever α ∈ L; ¬φ ∈ L ✷ , φ ∧ ψ ∈ L ✷ , whenever φ, ψ ∈ L ✷ .
One defines disjunction φ ∨ ψ := ¬(¬φ ∧ ¬ψ) and the modality ✸α := ¬✷¬α, where α ∈ L, in the usual way. In MEL, modalities ✷ and ✸ only apply to PL-formulae, contrary to usual modal logics. In the following, we denote by Γ a set of MEL-formulae, while B is used for sets of PL-formulae. Any set Γ of formulae in this language is interpreted as the sincere testimony of an agent. For instance, ✷α ∈ Γ means that the agent has said to believe α. The agent can assert beliefs in PL propositions α in this language, but some other statements are allowed as follows:

• If ✸α ∈ Γ , it means to the agent, α is possibly true, that is (s)he has no argument as to the falsity of α. All that we can conclude is that the agent either believes α is true, or ignores whether α is true or not. • If ✸α ∧ ✸¬α ∈ Γ , it means the agent explicitly ignores whether α is true or not.

• If ✷α ∨ ✷¬α ∈ Γ , it means the agent said he or she knows whether α is true or not, but his or her belief about α remains unknown.

On this basis, we (another agent receiving the testimony) may try to reconstruct the epistemic state of the witnessing agent.

Of course, the language allows for more sophisticated (maybe unlikely) assertions like (✸α ∧ ✸β) ∨ ✷γ , which means that either the agent has no reason to disbelieve α or to disbelieve β, or (s)he believes γ , or both. It reduces to the two assertions ✸α ∨ ✷γ and ✸β ∨ ✷γ . Note that the language allows to express that the agent ignores whether a proposition α is true or not, but it cannot express that we ignore if the agent knows anything about α. To do it, we should expand the language of MEL to include additional external modalities encapsulating MEL.

Remark 1.

1. PL-formulae are not MEL-formulae, as the languages L and L ✷ are disjoint. PL-formulae can only appear in the scope of modalities.

2. Iteration of the modal operators ✷, ✸ is not allowed in MEL, because we are not concerned with introspective reasoning, e.g. whether the agent believing α believes or not that (s)he believes α.

The language is modal-like but the spirit of the approach is different: we aim at nesting a logic inside another one, so as to avoid mixing sentences referring to the real world with sentences referring to what an agent believes about it. 4 Nevertheless, our setting is clearly similar to the one proposed by Halpern and colleagues [START_REF] Halpern | Reasoning About Knowledge[END_REF] reinterpreting knowledge bases as being fed by a "Teller" that makes statements supposed to be true in the real world. Important differences are that we are mainly concerned with beliefs held by the Teller (hence making no assumptions as to the truth of such beliefs), that these beliefs are incomplete, and that the Teller is allowed to explicitly express partial ignorance about specific statements.

The language of MEL is similar to the one of the early non-monotonic modal logic Ground S5 [START_REF] Halpern | Toward a theory of knowledge and ignorance: Preliminary report[END_REF]. The latter also has the ambition of reasoning about partial ignorance with the same interpretation for modal operators, but the perspective is different. Only one agent reflecting on its own belief is considered in Ground S5. Then a formula like ✷α ∨ ✷¬α is considered to be dishonest because an agent "cannot know one of α or ¬α without knowing one of them" [START_REF] Halpern | Toward a theory of knowledge and ignorance: Preliminary report[END_REF]. However, in our approach, the point of view is external and we may only know that the agent knows one of α or ¬α without knowing which of them is known by the agent.

The MEL axioms

In the following, for any set B ∪ {α} of PL-formulae, B ⊢ PL α denotes that α is a syntactic PL-consequence of B. In particular, ⊢ PL α indicates that α is a PL-theorem. The fact that we deal with knowledge and belief immediately suggests that the axioms of the modal system KD can be adopted. We consider the following axioms and rule of inference [START_REF] Hughes | A New Introduction to Modal Logic[END_REF].

Consider any φ, ψ, µ ∈ L ✷ , and α, β ∈ L.

Axioms.

(PL): (i) φ → (ψ → φ); (ii) (φ → (ψ → µ)) → ((φ → ψ) → (φ → µ)); (iii) (¬φ → ¬ψ) → (ψ → φ). (K ): ✷(α → β) → (✷α → ✷β).
(N): ✷α, whenever ⊢ PL α. (MP): If φ, φ → ψ then ψ .

The three axioms PL are those of propositional logic. Axiom K is not surprising as, if the agent believes a proposition is entailed by another, whenever (s)he believes the former (s)he should believe the latter. Axiom D comes down to considering that asserting the certainty of α is stronger than asserting its plausibility. It is a counterpart of numerical inequality between belief and plausibility functions [START_REF] Shafer | A Mathematical Theory of Evidence[END_REF], necessity and possibility measures [START_REF] Dubois | Possibilistic logic[END_REF] etc. in uncertainty theories.

Through N (necessitation), one asserts that the agent is expected to believe all tautologies. But note that in MEL it is an axiom. It cannot be an inference rule as α / ∈ L ✷ . Finally, the modus ponens rule MP enables the inference of additional beliefs held by the agent on the basis of his testimony. It allows to construct a better picture of the agent's epistemic state.

Axioms K and N imply the following, for any α, β ∈ L. (The nomenclature follows Chellas [START_REF] Chellas | Modal Logic: An Introduction[END_REF].) MEL is a fragment of the normal modal system KD (= EMCND [START_REF] Chellas | Modal Logic: An Introduction[END_REF]) with a restricted language. In other words, Γ ⊢ MEL φ if and only if Γ ⊢ KD φ, for any set Γ ∪ {φ} of MEL-formulae. In fact, MEL is also obtained as a fragment of KD45 or S5 (it is the fragment sometimes called subjective S5). But here, axioms 4, 5 of positive and negative introspection are pointless and cannot be expressed in the language (as per item 2 of Remark 1). In fact, modal logics are often defined starting with the most general syntax extending PL, and adding axioms (like 4, 5) that subsequently allow to simplify the syntax. Here we take the opposite stance, going from the PL language to a simple modal logic.

(RM): ✷α → ✷β, whenever ⊢ PL α → β. (M): ✷(α ∧ β) → (✷α ∧ ✷β). (
Note that MEL can also be viewed as a standard propositional logic. By construction, deduction in MEL is deduction in PL for a specific propositional language induced by At, enforcing specific additional axioms:

Γ ⊢ MEL φ ⇐⇒ Γ ∪ {K , N, D} ⊢ PL φ.
Here {K , N, D} stands for all instances of axioms K , N, D; φ is any MEL-formula and '⊢ PL ' is also being used as a consequence relation for this propositional language. So the deduction theorem and its converse hold in MEL. Syntactically, MEL's axioms can be viewed as a Boolean version of those of the fuzzy logic of necessities briefly suggested by Hájek [28, p. 232], replacing Łukasiewicz logic by PL.

The logic MEL: semantics and completeness

In this section, we propose an epistemic semantics for MEL, and show it is closely related to its standard propositional semantics, since MEL is also a propositional logic defined on a specific set of atoms. We prove that completeness with respect to the epistemic semantics is enforced by axioms K , D, N, which bridges the gap with possibility theory [START_REF] Dubois | Possibility theory: qualitative and quantitative aspects[END_REF]. Unlike the proof we gave in [START_REF] Banerjee | A simple modal logic for reasoning about revealed beliefs[END_REF], this one is direct, and does not explicitly appeal to accessibility relations.

A propositional valuation, as usual, is a map w : PV → {0, 1}, where PV := {p 1 , . . . , p k }. The set of all propositional valuations (interpretations) is denoted by V.5 For a PL-formula α, w | α indicates that w satisfies α or w is a model of α, i.e. w(α) = 1 (true). If w | α for every α in a set B of PL-formulae, we write w | B. We denote by [α] the set of {w: w | α} of models of α. Note that 2 V = {[α]: α ∈ L}.

Epistemic semantics

We follow Hintikka's definition of the truth of ✷α verbatim [START_REF] Hintikka | Knowledge and Belief[END_REF]: "in all possible worlds compatible with what the agent believes, it is the case that α", 6 and we denote by E "all possible worlds compatible with what the agent believes". In other words, we assume that an epistemic state is represented by a subset of mutually exclusive propositional valuations. Each valuation represents a 'possible world' compatible with the epistemic state of the agent. So, E ⊆ V, and it is further assumed that E is non-empty (otherwise the agent is inconsistent).

The satisfaction of MEL-formulae is defined recursively, as follows. For any α ∈ L, φ, ψ ∈ L ✷ , E( = ∅) ⊆ V:

• E | ✷α, if and only if E ⊆ [α]. • E | ¬φ, if and only if E | φ. • E | φ ∧ ψ , if and only if E | φ and E | ψ . Observe that if α is a valid PL-formula, E | ✷α, for all E ⊆ V. When E | φ, E is called an epistemic model of φ. It means
that in the epistemic state E, the agent may assert φ. If E | φ for all E, φ ∈ L ✷ is said to be a valid MEL-formula (the agent may assert it without providing any information). This semantics is called the epistemic semantics of MEL. It is then clear that:

E | ✸α if and only if E ∩ [α] = ∅,
i.e. there is at least one possible world where α holds for the agent. As a consequence, the epistemic state of the agent is known to be consistent with [α]. Note that ✸α can be interpreted as an expression of partial ignorance. Specifically,

E | ✸α ∧ ✸¬α corresponds to full ignorance about α, since E ∩ [α] = ∅, E ∩ [α] c = ∅, where A c is the complement of A.
It brings non-trivial information about the agent's epistemic state, even if it does not bring any information about the real world.

Likewise, formula ✷α ∨ ✷¬α is not tautological. More generally, epistemic models of a disjunction ✷α ∨ ✷β form the set {E:

E ⊆ [α]} ∪ {E: E ⊆ [β]}. It is clearly more informative than ✷(α ∨ β)
, since the latter allows epistemic states where none of α or β can be asserted. Restricting the epistemic states to singletons (assuming a totally informed agent), so as to mimic the classical semantics, would make these two formulae equivalent.

As usual, we have the notion of semantic equivalence of formulae:

Definition 2. φ is semantically equivalent to ψ , written φ ≡ ψ , if for any epistemic state E, E | φ, if and only if E | ψ . If Γ is a set of MEL-formulae, E | Γ means E | φ, for each φ ∈ Γ .
So the set of epistemic models of Γ , also denoted by [Γ ], is precisely {E: E | Γ }. For singleton Γ := {φ}, we simply write [φ] for the set of epistemic models of φ. Now we define semantic entailment:

Definition 3. For any set Γ ∪ {φ} of MEL-formulae, φ is a semantic consequence of Γ , written Γ | MEL φ, provided for every epistemic state E, E | Γ implies E | φ.
Note that in MEL, semantic consequence is classical, hence monotonic, as it is based on all epistemic models of Γ , while the logic Ground S5 [START_REF] Halpern | Toward a theory of knowledge and ignorance: Preliminary report[END_REF], despite its syntactic similarity with MEL, is non-monotonic, since its semantic consequence produces formulae true in the least informative (largest in the sense of inclusion) epistemic states of Γ .

From propositional to epistemic semantics: the uncertainty measure connection

We can also define a standard propositional semantics, since L ✷ is a propositional language. A propositional model of a MEL-formula is an interpretation v of L ✷ , that is, a mapping from At to {0, 1}. Let V ✷ be the set of such propositional valuations. We can use the standard semantic inference:

Γ | PL φ if and only if for all v ∈ V ✷ , if v | ψ for each ψ ∈ Γ , then v | φ.
It is clear that the propositional logic thus defined from atoms in At, using language L ✷ , axioms PL and inference rule MP is sound and complete with respect to this propositional semantics. Now for the logic MEL, one must restrict to standard interpretations v that satisfy axioms K , D and N, forming a subset of V ✷ denoted by V MEL . In the following, we show that V MEL is in one-to-one correspondence with the set of epistemic states {E: ∅ = E ⊆ V}, and that the epistemic semantics is equivalent to the standard propositional semantics restricted to V MEL . We then get soundness and completeness of MEL directly from the one of propositional logic. Given a valuation v ∈ V ✷ , we can define a Boolean set-function g v : 2 V → {0, 1} such that:

g v [α] := v(✷α), ✷α ∈ At.
As noted earlier, 2 V = {[α]: α ∈ L}, i.e. we assume that any subset E of V is representable by the set of models [α] of some formula α. This always makes sense provided that E is finite, which is the case here as V is finite.

A set-function is typically used as a representation of uncertainty. In other words, a propositional valuation of the modal language can be viewed as an uncertainty measure. In the case of MEL, we can define exactly which kind of uncertainty measure is induced by valuations. Proposition 1. The following statements hold for all v ∈ V ✷ .

1. If axiom N holds, then g v (V) = 1. 2. If axiom D holds, then for all A ⊆ V, g v (A) 1 -g v (A c
), and, if moreover N holds, then g v (∅) = 0. 3. If axioms K and N hold, then for all A, B ⊆ V, g v (A ∩ B) = min(g v (A), g v (B)).

Proof.

1. Axiom N restricts the choice of v to those such that v(✷α) = 1, where α is a tautology of PL, which reads

g v (V) = 1. 2. Axiom D reads v(✸α) = 1 -v(✷¬α) v(✷α); it restricts the choice of v to those such that v(✷¬α) = 0 whenever v(✷α) = 1. Since v(✸α) = 1 -g v ([α] c ), we have g v ([α]) + g v ([α] c ) 1. In particular, g v (∅) 1 -g v (V) = 0 (due to N). 3. Axiom K restricts the choice of v to those such that v(✷(¬α ∨ β)) max(1 -v(✷α), v(✷β)), which reads for all A, B ⊆ V, g v A c ∪ B max 1 -g v (A), g v (B) . Note that if A c ∪ B = V, that is, A ⊆ B,
and g v (A) = 1 this property, together with N implies g v (B) = 1, so that K and N enforce the monotonicity of the set-function g v . So g v is a (Boolean) capacity. Moreover replacing B by A ∩ B in the above inequality yields the equivalent form:

for all A, B ⊆ V, g v A c ∪ B max 1 -g v (A), g v (A ∩ B) ,
which, in the Boolean case is equivalent to

min g v A c ∪ B , g v (A) g v (A ∩ B).
In particular min(g v (B),

g v (A)) g v (A ∩ B), which along with monotonicity yields for all A, B ⊆ V, g v (A ∩ B) = min(g v (A), g v (B)). ✷
The reverse implication holds for item 1, and partly for item 2 (i.e. the given condition implies D, but the additional condition alone does not imply N), and does not hold for item 3. The main problem in the last two cases is that g v (V) = 1 (i.e. N) does not follow from the given conditions.

A set-function N with range on the unit interval that satisfies

N (∅) = 0, N (V) = 1, N (A ∩ B) = min(N (A), N (B))
is well-known to be a necessity measure in possibility theory [START_REF] Dubois | Possibility theory: qualitative and quantitative aspects[END_REF]. It is a special case of belief function and lower probability measure. In the Boolean finite case it is well-known that for each such necessity measure N there exists a unique non-empty subset E ⊆ V such that

N (A) = 1 if E ⊆ A; 0 otherwise.
The characteristic function of E is the possibility distribution generating N . Moreover the corresponding possibility measure is

Π(A) = 1 -N (A c ) = 1 if E ∩ A = ∅
Π({w}) = 1 = N (V \ {w}).
Finally, the following result is the converse of the previous proposition. It ensures that MEL is the logic of Boolean possibility theory and can be checked straightforwardly:

Proposition 2. Given a Boolean necessity measure N on 2 V , the valuation v defined by v(✷α) := N ([α]), for all α ∈ L, satisfies all instances of axioms K , N, D.

The above result is unsurprising as it comes down to the connection between axioms K and N, and axioms RM, C , M in the KD logic. But it is better here to give a direct proof. Note that in the multivalued case, the rendering of the original axiom K as the (numerical) inequality

g v (A c ∪ B) max(1 -g v (A), g v (B)
) is stronger than the axiom of necessity measures. Indeed, assume g v ranges on [0, 1] then assume A = B: it yields max(1 -g v (A), g v (A)) 1, which enforces g v to be a Boolean set-function. However, one alternative writing of

K using N is min(g v (A c ∪ B), g v (A)) g v (A ∩ B), which is
equivalent to the axiom of necessity measures in the gradual case.

Remark 2. Note that Proposition 2 holds for Boolean versions of more general set-functions than necessity measures, namely, super-additive ones, i.e., such that g( A ∪ B) g( A) + g(B) whenever A ∩ B = ∅, since if the range of g is the set {0, 1} then the super-additivity axiom is equivalent to g( A ∩ B) = min(g( A), g(B)) for all A, B. MEL thus lays bare a natural relationship between modal logic and uncertainty theories. But then ✷α is many-valued, as studied by Hájek [START_REF] Hájek | The Metamathematics of Fuzzy Logics[END_REF] who replaces classical logic with atoms ✷α by a fuzzy logic.

Note that it is clear that the modal atoms in At are no longer logically independent in MEL. In fact, knowing the truth-values of all atoms of the form ✷( i∈I ℓ i ), where ℓ i is a PL-literal, the truth-values of the other atoms in At are determined by axioms K , D, N.

Completeness

From the previous section, for any propositional valuation of the modal language of MEL from the set V MEL (i.e. satisfying MEL axioms), we can construct a single epistemic state and conversely. Given a valuation v satisfying MEL axioms, define an associated epistemic state

E v := w ∈ V: g v V \ {w} = 0 .
From the definition of E v , the following holds.

(i) Since g v is a necessity measure, E v is unique and non-empty.

(ii) v | φ (in the propositional semantics) if and only if E v | φ (in the epistemic semantics).

Conversely, given an epistemic state E, we can define a valuation of the modal language of MEL as follows:

v E (✷α) :=

Logical representation of sets of epistemic models

In a previous paper [2] we discussed how to represent a family of non-empty subsets of propositional valuations in V (understood as a meta-epistemic state: what is known about an agent's epistemic state) by means of a MEL-formula. We did show that the set of MEL-formulae, quotiented by semantic equivalence are in one-to-one correspondence with the power set of V (minus the empty set). The completeness proof explained above enables such results to be much more simply retrieved.

It is clear that any consistent subset (or conjunction) of MEL-formulae Γ has a non-empty set of epistemic models that forms a family [Γ ] = {E: E | Γ } of epistemic states. Consider the case of a single epistemic set E. It can be fully characterized by elementary constraints on a Boolean possibility or necessity measure. Namely, Π({w}) = 1 if w ∈ E and 0 otherwise. The impossibility of non-E valuations can be more simply expressed by the constraint N (E) = 1, while Π({w}) = 1 reads N (V \ {w}) = 0. Let α E be a PL-formula such that E = [α E ], and α w := w(p)=1 p ∧ w(p)=0 ¬p be the PL-conjunction characterizing w. 7 In MEL, using the one-to-one correspondence between epistemic states E and MEL valuations v E , it is clear that v E is uniquely characterized by the constraints v E (✷¬α w ) = 0, for all w ∈ E, and v E (✷α E ) = 1, which yields the MEL-formula

δ E := ✷α E ∧ w∈E ¬✷¬α w = ✷α E ∧ w∈E ✸α w .
The set [δ E ] of epistemic models is clearly equal to the singleton {E}. This formula describes complete (meta-)knowledge of an agent's epistemic state. It is clear that there is a one-to-one correspondence between MEL-valuations (satisfying MEL axioms) and formulae δ E .

At the syntactic level, formulae δ E may benefit from the introduction of an extra symbol , similar to ✷, such that α is short for w∈E ✸α w . One can see that E | α if and only if [α] ⊆ E, which is similar to E | ✷α, reversing the inclusion symbol at the semantic level. This modality has been introduced in [START_REF] Dubois | Knowledge-driven versus data-driven logics[END_REF] in order to account for the idea of "guaranteed possibility" (as for instance explicit permission in a deontic meaning). 8 Then δ E has the simpler form ✷α E ∧ α E , and expresses the idea of "only knowing" [START_REF] Levesque | All I know: A study in autoepistemic logic[END_REF]. Namely, ✷α ∧ α ∈ Γ means that the agent only knows that α is true, since [✷α ∧ α] = {[α]}. The formula ✷α ∧ α ∈ Γ is also a special case of the cover modality studied in [START_REF] Bílková | Proof systems for the coalgebraic cover modality[END_REF] which is shown to provide an alternative formulation of standard modal logic. Note also that δ E is a kind of canonical form of the Jankov-Fine style, familiar in modal logics.

More generally, let E := {E 1 , . . . , E n } be any non-empty collection of non-empty sets of propositional valuations, one of which is the agent's correct epistemic state. A MEL-formula whose set of epistemic models is exactly E can be thus constructed as

δ E := 1 i n δ E i = 1 i n (✷α E i ∧ α E i ).
It means that any MEL-base Γ with set [Γ ] of epistemic models can be put into a kind of normal form as δ [Γ ] , that has the same epistemic models as Γ thus preserving their set of MEL consequences Con(Γ ) = Con(δ [Γ ] ). We can summarize these findings in the following result, which is the counterpart of the correspondence between propositional bases and subsets of classical interpretations.

Proposition 3.

(a) The Boolean algebra consisting of the set L ✷ of MEL-formulae quotiented by semantical equivalence ≡, is isomorphic to the power set Boolean algebra with domain 2 2 V \{∅} . The correspondence, for any MEL-formula φ, is given by: {ψ:

ψ ≡ φ} → [φ]. (b)
There is a bijection between the set of all sets of epistemic states and the set of all (deductively closed) belief sets of MEL, i.e. Γ such that Con(Γ ) = Γ . For any family E ⊆ 2 V \ {∅}, the correspondence is given by: E → Con(δ E ).

This result could be used for a proper development of MEL-theory revision in the style of Gärdenfors [START_REF] Gärdenfors | Knowledge in Flux[END_REF] (whereby one could revise what is explicitly known and what is explicitly unknown) since his treatment relies on deductively closed sets of formulae, in place of sets of possible worlds.

The encapsulation of PL into MEL

Encoding a belief α by ✷α in MEL stands in contrast to, e.g., the belief revision literature [26], where beliefs are repre- sented by propositions of PL, keeping the modality implicit. But the MEL language is more expressive because α and ✷α have models of a different nature, as shown above, which avoids confusion between ¬✷α(≡ ✸¬α) and ✷¬α.

Using soundness and completeness of MEL, we get the following result, which demonstrates that deriving a ✷-formula, say ✷α, in MEL from another ✷-formula ✷β is equivalent to deriving α from β in PL. It may be noted that the result was proved in [START_REF] Dubois | Knowledge-driven versus data-driven logics[END_REF] for the modal system K having the standard Kripke semantics. As we shall see below, the proof immediately carries over to MEL. Axiom D is not used.

For any set B of PL-formulae, let ✷B := {✷β: β ∈ B}, ✸B := {✸β: β ∈ B}. Particularly, IM and IC enable any set of MEL formulae of the form ✷B to be put in the form of a set of boxed PL clauses, a form that enables the last inference rule to be applied (or equivalently the axioms and inference rule of PL, dropping the ✷ in front of clauses). This result clearly indicates that the added value of MEL with respect to classical logic is to make it possible to reason about formulae the truth-values of which are explicitly ignored. For believed PL-formulae, the logic behaves classically. Theorem 2 also confirms that propositional logic is encapsulated in MEL; MEL is not a usual modal extension of propositional logic: it is a two-tiered logic.

We could iterate the encapsulation process, namely prefix MEL-sentences with an external ✷ modality, expressing the beliefs of a third agent on the beliefs of the second one, concerning the original agent's epistemic state. Such prefixed MELsentences would be atoms of a third level propositional logic, with language (L ✷ ) ✷ . Models of formulae in this language would be subsets of epistemic states.

Inferring ignorance

The following results shed more light on the connection between propositional logic and the higher order language. We begin with a few corollaries to Theorem 2.

Corollary 1. The 'converse' of (RM) holds:

⊢ PL α → β, if ⊢ MEL ✷α → ✷β.
In other words, we have the equivalence:

⊢ MEL ✷α → ✷β, if and only if ⊢ PL α → β.
In fact, this also yields the equivalence:

⊢ MEL ✷α → ✷β if and only if ⊢ MEL ✷(α → β).
⊢ MEL ✷α → ✸β, if and only if ⊢ PL α → β.
Proof. The 'if' part is a consequence of Theorem 2 and axiom D. The proof of the converse part again follows the same lines as for the 'only if' part of Theorem 2. ✷ With the help of all the above, it is easy to derive some inference rules in MEL, that apply to the encapsulated PLformulae.

Proposition 4.

(1) {✷α,

✸(α → β)} ⊢ MEL ✸β. (2) {✷(¬α ∨ β), ✷(α ∨ γ )} ⊢ MEL ✷(β ∨ γ ). (3) {✷(¬α ∨ β), ✸(α ∨ γ )} ⊢ MEL ✸(β ∨ γ ).
Proof. These inference rules can be proved with theorems of the MEL-fragment of K , Theorem 2 and Corollary 2. ✷ Rule (1) is a weakened form of PL modus ponens, which from the point of view of encapsulated PL-formulae, preserves consistency, not certainty (hence not truth) of inner formulae. Rule ( 2) is related to the resolution rule in possibilistic logic [START_REF] Dubois | Possibilistic logic[END_REF] which preserves the weakest degree of certainty of premises. Rule (3) is the resolution counterpart of Rule (1) and was first proposed and semantically validated in the multivalued setting of possibility theory in [START_REF] Dubois | Resolution principles in possibilistic logic[END_REF]. Consistency-preserving inference rules (i.e. with premises and conclusion involving ✸-prefixed formulae) indicate that reasoning about explicit partial ignorance is not completely trivial: via reasoning steps, one can better figure out what the agent is supposed to ignore (when both ✸α and ✸¬α can be derived from Γ ).

MEL as a basis for reasoning about uncertainty

Epistemic or doxastic logics have a claim to reason about incomplete knowledge or about beliefs. Uncertainty theories also consider belief as a central notion. However, they correspond to different streams of thought and different communities. Nevertheless, uncertainty theories and doxastic logic must share some common ground. Due to its set-valued semantics in terms of epistemic states, or equivalently possibility distributions, it is easier to relate uncertainty theories to MEL than to modal logics that extensively use accessibility relations, since the latter play no role in uncertainty theories. In the uncertain reasoning perspective, the accessibility relation appears as an artefact, while it is very natural in other settings like temporal logic. Moreover, the nesting of modalities allows expressing very complex formulae whose meaning may become very hard to grasp. In contrast, the simple encapsulation of classical propositions (then often called 'events') by means of degrees of belief is typical of uncertainty theories. In the following, we briefly discuss connections between MEL and uncertainty theories.

Möbius transform and MEL-formulae

A connection between MEL and belief functions was hinted at in Section 1. A belief function [START_REF] Shafer | A Mathematical Theory of Evidence[END_REF] Bel is a non-additive monotonic set-function (a capacity) with domain 2 V and range in the unit interval, that is super-modular at any order (also called ∞-monotone), that is, it verifies a strong form of super-additivity, and as such belief functions generalize probability measures. The degree of belief Bel( A) in proposition A evaluates to what extent this proposition is logically implied by the available evidence. The plausibility function Pl( A) := 1 -Bel( A c ) evaluates to what extent events are consistent with the available evidence. The pair (Bel, Pl) can be viewed as quantitative randomized versions of KD modalities (✷, ✸) [START_REF] Smets | Comments on R.C. Moore's autoepistemic logic[END_REF], hence of MEL. Interestingly, elementary forms of belief functions arose first, in the works of Bernoulli, for the modeling of unreliable testimonies [START_REF] Shafer | Nonadditive probabilities in the work of Bernoulli and Lambert[END_REF], while a set of formulae in MEL also encodes the testimony of an agent. The connection between epistemic logic and belief functions was studied in details quite early by Mongin [START_REF] Mongin | Some connections between epistemic logic and the theory of nonadditive probability[END_REF], who proposes a modal logic (with nested modalities) for propositions with maximal degrees of belief, and a semantics in terms of neighborhoods. He shows that KD offers a sound and complete axiomatization, thus getting very close to MEL.

The function Bel can be mathematically defined from a (generally finite) random set on V, that has a very specific interpretation. A so-called basic assignment m assigns to each subset E of V a non-negative value m(E) ∈ [0, 1] for all E ⊆ V; moreover:

∅ =E⊆V m(E) = 1.
The degree m(E) is understood as the weight given to the fact that all an agent knows is that the value of the variable of interest lies somewhere in set E, and nothing else. In other words, the probability allocation m(E) could eventually be shared between elements of E, but remains suspended for lack of knowledge. A set E such that m(E) > 0 is called a focal set. In the absence of conflicting information it is generally assumed that m(∅) = 0. It is then clear that a collection of focal sets is a meta-epistemic state in our terminology. A belief function Bel can be expressed in terms of the basic assignment m [START_REF] Shafer | A Mathematical Theory of Evidence[END_REF]:

Bel [α] = E| ✷α m(E),
using the terminology of MEL semantics. It is clear that the assertion of a MEL-formula ✷α is faithfully expressed by Bel([α]) = 1. Specifically, Bel([α]) can be interpreted as the probability of ✷α [START_REF] Smets | Comments on R.C. Moore's autoepistemic logic[END_REF], more precisely as P ({E: E ⊆ [α]}), where P is a probability measure on 2 V , such that m(E) = P ({E}).

The converse problem, namely, reconstructing the basic assignment from the belief function, has a unique solution via the so-called Möbius transform

m(E) = A⊆E (-1

) |E\A| Bel( A).

There is a similarity between the problem of reconstructing a mass assignment from the knowledge of a belief function and the problem of representing an epistemic state E in the language of MEL as in Section 3.4 by the formula ✷α E ∧ ¬ w∈E ✷¬α w = δ E . We can show that this expression is an exact symbolic counterpart of the Möbius transform. To see it, in fact, rewrite the Möbius transform as

m(E) = A⊆E: |E\A| even Bel( A) - A⊆E: |E\A| odd Bel( A),
where |A| is the cardinality of set A. Now translate into , Bel( A) into ✷α, "-" into ∧¬.

Proposition 5. The logical rendering of the Möbius transform for computing m(E):

α| α E : |E\[α]| even ✷α ∧ ¬ α| α E : |E\[α]| odd ✷α is logically equivalent to δ E := ✷α E ∧ w∈E ✸α w .
Proof. Indeed, note first that if β | α, ✷α ∨ ✷β ≡ ✷α in MEL (using Theorem 2), so, α| α

E : |E\[α]| even ✷α ≡ α| α E : |E\[α]|=0 ✷α, which is ✷α E . Likewise, α| α E : |E\[α]| odd ≡ α| α E : |E\[α]|=1
, which is just w∈E ✷α E\{w} . Hence the term ¬ α| α E : |E\[α]| odd ✷α boils down to the equivalent formula ¬ w∈E ✷α E\{w} , which is exactly w∈E ✸α w . ✷ So one may consider belief (resp. plausibility) functions as numerical generalizations of MEL boxed (resp. diamonded) formulae. More specifically, while Bel([α]) can be interpreted as P ([✷α]), the above result is consistent with the understanding of the mass function as:

m(E) = P [δ E ] = P ✷α E ∧ ¬ w∈E ✷¬α w = P [✷α E ∧ α E ] .
It is, literally, the probability P ({E}) of only knowing E.

This point (it also appears in Lemma 5.1 of [START_REF] Godo | A fuzzy modal logic for belief functions[END_REF]) suggests a logic of belief functions that builds on MEL syntax and semantics. At the syntactic level, one could handle graded modal propositions ✷ r α where α is a proposition in PL, and r ∈ [0, 1] stands for a lower bound for the degree of belief of α (Bel([α]) r). At the semantic level, the satisfaction relation should be of the form m | ✷ r α whenever E⊆[α] m(E) r. This is clearly one of the perspectives opened by our framework.

It would be useful to compare a belief function counterpart of MEL with the fuzzy logic of belief functions devised by Godo and colleagues [START_REF] Godo | A fuzzy modal logic for belief functions[END_REF] (which uses multivalued modal formulae and again appeals to accessibility relations).

MEL and generalized possibilistic logic

Possibilistic logic has been essentially developed as a formalism for handling qualitative graded belief with an inference mechanism that remains close to the one of classical logic [14,19]. A standard possibilistic logic expression is a pair (α, a), where α is a propositional formula and a ∈ (0, 1]. Any discrete linearly ordered scale can be used in place of [0, 1]. The weight a is interpreted as a (positive) lower bound of the degree of necessity of α, i.e. N (α) a, where the function N is a necessity measure. A possibilistic belief base is a conjunction of such weighted formulae. Disjunctions and negations of possibilistic formulae are not allowed in basic possibilistic logic, which is only a simple totally ordered extension of classical logic. 9Possibilistic knowledge bases have semantics in terms of a weak order over the set V of interpretations, encoded by means of a single possibility distribution π : V → [0, 1]. For a weighted formula (α, a): π (α,a) (w) = 1 if w | α, and 1 -a otherwise. In other words, an interpretation violating α is all the less tolerated as α is more certain. It can be checked that N (α) = min w | α 1 -π (α,a) (w) = a. The possibility distribution induced by a possibilistic belief base is obtained by the pointwise minimum of the possibility distributions induced by each possibilistic formula in it. It generalizes the standard propositional logic semantics.

Possibilistic logic (POSLOG) is another two-tiered logic like MEL. It is propositional logic embedded within a multivalent logic, as the semantics of weighted formulae (α, a) is clearly many-valued. This multivalent logic is a fragment of Gödel logic (as stressed by Hájek [START_REF] Hájek | The Metamathematics of Fuzzy Logics[END_REF]), where the only allowed connective is conjunction expressed by the minimum.

Assuming only maximal weights a = 1, and identifying (α, 1) with ✷α, possibilistic logic actually coincides with the fragment of MEL containing only conjunction of boxed formulae that was proved equivalent to propositional logic itself in Section 3.5. At the semantic level, a possibility distribution is a graded extension of an epistemic model of MEL. The satisfiability of a possibilistic formula (α, a) by any possibility distribution is such that:

π | (α, a) ⇐⇒ N (α) = min v | α 1 -π(v) a.
So the semantics of possibilistic logics can be described in terms of generalized MEL epistemic models. This kind of semantics was proposed by Boldrin and Sossai [START_REF] Boldrin | Local possibilistic logic[END_REF] under the name forcing semantics.

Inference rules valid in MEL suggested in Section 3.6 are Boolean versions of the two resolution rules in possibility theory

• {(¬α ∨ β, a), (α ∨ γ , b)} ⊢ POSLOG (β ∨ γ , min(a, b))
, where a and b are degrees of necessity [14]: Rule (2) in Proposition 4 is retrieved when a = b = 1.

• {N (¬α ∨ β) a, Π (α ∨ γ ) b} | Π(β ∨ γ ) a, whenever a + b > 1 [START_REF] Dubois | Resolution principles in possibilistic logic[END_REF]. This rule cannot be expressed in standard possibilistic logic but its syntactic rendering is Rule (3) in Proposition 4, when a = b = 1.

It is thus patent that MEL and possibilistic logic are two extensions of standard propositional logic PL in two complementary directions: the syntactic handling of incomplete information on the one hand (MEL), and graded beliefs on the other hand (POSLOG). It is natural to consider the joint extension of PL to a graded version of MEL, providing a full-fledged uncertainty logic enabling certainty and partial ignorance to be handled at a syntactic level. Such a generalized possibilistic logic is suggested by Dubois and Prade [START_REF] Dubois | Generalized possibilistic logic[END_REF]. In particular, disjunctions and negations of possibilistic formulae were interpreted similarly to disjunctions and negations of MEL-formulae, in terms of union and setcomplement of families of generalized epistemic models of weighted formulae. The introduction of connectives other than idempotent conjunctions between possibilistic formulae was studied by Boldrin and Sossai [START_REF] Boldrin | Local possibilistic logic[END_REF] in the scope of data fusion. More recently, generalized possibilistic logic was shown to capture answer-set programming [START_REF] Dubois | Stable models in generalized possibilistic logic[END_REF]: an ASP rule rewritten in such an extension of MEL is much easier to interpret. In fact, modal logics capturing possibility and necessity measures have been around since the early nineties [START_REF] Del Cerro | A modal analysis of possibility theory[END_REF][START_REF] Boutilier | Modal logics for qualitative possibility theory[END_REF][START_REF] Hájek | On modal logics for qualitative possibility in a fuzzy setting[END_REF], but they were devised with a classical view of modal logic (not so much under our two-tiered view) and Kripke semantics, and used Łukasiewicz logic with multivalued atoms ✷α for the higher order language.

Link with probabilistic logic

MEL can, in fact, be also considered as a degenerated probabilistic logic by interpreting ✷α as Prob(α) = 1, and hence ✸α as Prob(α) > 0. The semantics of MEL can then be described in terms of probability measures with distributions p on V, with w∈V p(w) = 1. To each probability measure P , define the epistemic state E P := {w: p(w) > 0} which is the support of p. We can define P | ✷α as E P | MEL ✷α, which corresponds indeed to P ([α]) = 1. Then P | ✸α means E P | MEL ✸α, which corresponds indeed to P ([α]) > 0. Conversely, if P E is the set of probabilities with support E, then E | ✷α if and only if w∈E p(w) = 1. Of course there are many probability distributions with the same support, so MEL can be considered as a very coarse imprecise probability logic.

More generally, reasoning under graded uncertainty in a logical format can be addressed with three approaches:

• by logics such as generalized possibilistic logic [START_REF] Dubois | Generalized possibilistic logic[END_REF][START_REF] Dubois | Stable models in generalized possibilistic logic[END_REF], that handle elementary expressions of the form g(α) a, where g is some uncertainty measure, along with their negations and their conjunctions [START_REF] Fagin | A logic for reasoning about probabilities[END_REF][START_REF] Nilsson | Probabilistic logic[END_REF] using weighted modalities,

• by logics that handle many-valued higher order propositions [START_REF] Hájek | Fuzzy logic and probability[END_REF][START_REF] Godo | A fuzzy modal logic for belief functions[END_REF][START_REF] Hájek | On modal logics for qualitative possibility in a fuzzy setting[END_REF]. For instance, a degree of probability Prob(α) = P ([α]), where P is a probability measure on V, can be modeled as the truth-value of the proposition "Probable(α)"

(which expresses the statement that α is probably true), where Probable is a many-valued predicate [START_REF] Hájek | Fuzzy logic and probability[END_REF]. The possibility logic in [START_REF] Hájek | On modal logics for qualitative possibility in a fuzzy setting[END_REF] and the logic of belief functions [START_REF] Godo | A fuzzy modal logic for belief functions[END_REF] are of the same vein.

• by conditional logics of relative uncertainty, that can express that one proposition is more certain than another one, following the pioneering work of Lewis on comparative possibility [START_REF] Lewis | Counterfactuals and comparative possibility[END_REF] (see also Halpern [31] and Hájek [28, p. 212]).

All such logics can be studied as graded extensions of (fragments of) MEL.

Related work

In this section, we briefly review past works that either share similar technical tools or are closely related to our proposal.

Epistemic logics

The modal logic approach to reasoning about knowledge often relies on the S5 modal logic and on KD45 for reasoning about beliefs [START_REF] Halpern | Reasoning About Knowledge[END_REF]. At the semantic level, it uses Kripke semantics based on an accessibility relation R among possible worlds. A proposition α is necessarily true (i.e. ✷α is true) at world w if and only if it is true at all accessible worlds w ′ (such that w R w ′ ). Indeed, modal logic was also tailored to account for relations having various properties. Formally, the possibility of nested modalities accounts for the composition of relations. In the area of epistemic and doxastic logics, the use of the accessibility relation has been often taken for granted in the literature. Basically, many authors, trying to justify Kripke semantics in this context, consider w R w ′ to mean that w ′ is possible for the agent at world w [START_REF] Halpern | Reasoning About Knowledge[END_REF], or that w and w ′ are not distinguishable [START_REF] Kraus | Knowledge, belief and time[END_REF]. However, such understandings are somewhat difficult to relate to the notion of belief as construed in uncertainty theories.

On the one hand, the lack of distinguishability of possible worlds may be a source of epistemic uncertainty but it is more closely related to the use of modal logics for rough sets [START_REF] Orłowska | Kripke semantics for knowledge representation logics[END_REF]. On the other hand, it is not very clear how the phrase "an agent at a possible world w" should be interpreted. It may mean some kind of condition like "given that the real world where the agent lives is w". However, it is hard to imagine that the agent beliefs are completely determined by what the real world is (unless we include the description of the agent itself in the vocabulary). In our paper, possible worlds are just interpretations of the language, and the real world is supposed to be external to the agent.

In any case, our approach has no ambition to consider all possible epistemic states of an agent in all possible worlds (in the philosophical sense), nor to model conditional beliefs, although this issue is certainly of interest for future investigations.

Here, the assumption that we rule out nested modalities and introspection (unlike Ground S5 [START_REF] Halpern | Toward a theory of knowledge and ignorance: Preliminary report[END_REF], already mentioned, and Moore's autoepistemic logic (AEL) [START_REF] Moore | Semantical considerations on nonmonotonic logic[END_REF]) makes the relational semantics too rich and not very natural in our context. More recently, Petruszczak [START_REF] Petruszczak | Simplified Kripke style semantics for modal logics K5, KB5 and KD45[END_REF] indicated that simplified Kripke frames could indeed be used for the semantics of systems K 45, KB5 and KD45, using subsets of propositional valuations in place of relations, as we proposed. He proves it by constructing specific accessibility relations equivalent to such subsets, as we did in [START_REF] Banerjee | A simple modal logic for reasoning about revealed beliefs[END_REF] for MEL, while our completeness proof here is direct. Our logic is even less expressive than S5 but the elementary, and very natural epistemic semantics in terms of mere subsets of propositional valuations is more in line with uncertainty theories as we have seen earlier.

Consensus logic

Pauly [START_REF] Pauly | Axiomatizing collective judgment sets in a minimal logical language[END_REF] presents a logic for consensus voting C that has a language and axiomatization identical to those of MEL, as well as a similar semantics, however set in a different context altogether. Suppose |PV| = k, so that the number of propositional valuations is |V| = 2 k . Let I be a finite set of n elements (n a positive integer), interpreted as voters. A vote is a mapping ν from I to the set V of PL valuations, whereby each voter i decides, by choosing w i = ν(i), which formulae α ∈ L he or she accepts and rejects. Instead of the set ν(I), Pauly considers the image of I through ν as a multi-set W ν (as several valuations may be identical). The multi-set W ν is interpreted as a collective valuation such that W ν (✷α) = 1, if and only if w i (α) = 1, i = 1, . . . , n, which can be written W ν | C ✷α.

:= {w ∈ V: ∃i, w = ν(i)}. It is clear that W ν | C ✷α implies E ν | MEL ✷α. Moreover, if n 2 k and E ν = V then W ν | C ✷α if
and only if ✷α is a MEL tautology. Beyond the formal similarity of MEL and C logics, there are significant differences, as C-models are multisets of PL-valuations, while MEL-models are sets. Moreover, an epistemic state in MEL is a disjunction of interpretations, and a multi-set W ν corresponds to a conjunction of voters in the C-logic: in the latter case it cannot be interpreted as a possibility distribution. The aims and scope of these two logics are at odds.

Partial logic

Partial logic Par [START_REF] Blamey | Partial logic[END_REF], like MEL, uses sets of valuations in place of valuations, albeit special ones under the form of partial models. A partial model σ assigns truth-values to a subset of propositional variables. The corresponding epistemic model is formed of all completions of σ . Specifically, Par adopts a truth-functional view, based on Kleene logic and assumes the equivalence σ | α ∨ β if and only if σ | α or σ | β. So it loses classical tautologies, which sounds paradoxical when propositional variables are Boolean [START_REF] Dubois | On ignorance and contradiction considered as truth-values[END_REF]. Actually, the basic Par keeps the syntax of classical logic, which forbids to make a difference between the fact of believing α ∨ β and that of believing α or believing β. In fact, it has been recently shown [START_REF] Ciucci | Three-valued logics for incomplete information and epistemic logic[END_REF] that Kleene logic can be mapped to a fragment of MEL, where modal atoms ✷α are restricted to literals inside (i.e. are of the form ✷p and ✷¬p) and only conjunctions and disjunctions of such modal atoms are allowed (no negation). In view of this recent work, disjunctions α ∨ β in partial logic should be encoded as ✷α ∨ ✷β in MEL. It is not possible to express pieces of knowledge encoded by the MEL-formulae ✷(α ∨ β) nor ¬✷α in partial logic. Besides, MEL-formulae could be expressed by pairs of the form (α, T) (T for "surely true") instead of ✷α, in the spirit of Labelled Deductive Systems (Gabbay [START_REF] Gabbay | Labelled Deductive Systems[END_REF]), where T is the reification of Kleene's "true". Then T lies in the Kleene-like three-valued truth set {T, F, U}, where (α, F) stands for ✷¬α and U means unknown, i.e. (α, U) stands for ✸α ∧ ✸¬α. See [12] for this translation. We are then even closer to Kleene logic formalism, except that the latter is truth-functional, while this rewriting of MEL is not, and it avoids the paradoxes of Kleene logic.

Conclusion and perspectives

This paper is an attempt to directly relate modal languages to uncertainty theories. It borrows from modal logic because it uses a fragment of the KD logic where standard modal symbols ✷ and ✸ respectively express ideas of belief or certainty understood as validity in an epistemic state, and plausibility understood as consistency with an epistemic state. It is simpler than usual modal logics (it is a sub-language of S5) by a deliberate stance on not nesting modalities, and not mixing modal and non-modal formulae, thus viewing the language as defining a two-tiered logic: it is a higher order propositional logic with additional axioms, rather than a standard modal logic. At the semantic level, this simple language is capable of accounting for incomplete information about an agent's epistemic state, modeled by a family of non-empty subsets of classical valuations. Clearly, MEL is the core uncertainty logic accounting for incomplete information, on which more sophisticated uncertainty logics can be built.

In some sense, MEL goes against the tradition of modern modal logics which, at the philosophical level are de re logics because even when the modalities have an epistemic flavor, they refer to the actual world via the Kripke relation. MEL is a de dicto logic, because formulae in MEL refer to an agent's epistemic state, not to any objective reality. Only beliefs (true or not) and doubts about the world can be stated in MEL, but no claim that a proposition is actually true. In this sense it is a minimally expressive doxastic or epistemic logic. Combinations of objective and epistemic statements like α ∨ ✷β are not allowed in this simple logic, which does not prevent the development of extensions of MEL to S5-like languages where meta-statements relating belief and actual knowledge, observations and objective truths could be expressed. In order to evaluate mixed formulae such as α ∨ ✷β, we should extend the notion of epistemic model E ⊂ V to pairs (w, E) ∈ V × 2 V , and define (w, E) | α ∨ ✷β as "w | α or E | ✷β".

One of the merits of MEL is to potentially offer a logical grounding to uncertainty theories of incomplete information. Indeed, basic uncertainty theories like imprecise probability, evidence theory and possibility theory handle generalized epistemic states, not accessibility relations. One important contribution of the paper is to show that MEL is the Boolean version of Shafer's theory of evidence, whereby a mass function is an extension of a meta-epistemic state. Some technical aspects of MEL require more scrutiny, like proof methods and computational complexity. The simplicity of the semantics and logical structure of the logic is counterbalanced by the large number of MEL atoms. The number of atoms is exponential in the number of propositional variables of the lower level propositional language. On this issue, though, existing results pertaining to the logic S5 [START_REF] Bienvenu | Knowledge compilation in the modal logic S5[END_REF] could be adapted.

The framework of MEL also suggests lines of further research. An obvious extension to be studied is to generalize MEL and possibilistic logic using (graded) multi-modalities, so as to accommodate generalized epistemic states such as possibility distributions and belief functions, as pointed out in Section 4. Since the inception of MEL [START_REF] Banerjee | A simple modal logic for reasoning about revealed beliefs[END_REF], this task has been under study [START_REF] Dubois | Generalized possibilistic logic[END_REF][START_REF] Dubois | Stable models in generalized possibilistic logic[END_REF]. Likewise it can be conjectured that some logics of comparative possibility as described by Lewis [38] and Hájek [28, p. 212] are conservative extensions of MEL.

The point of view adopted here, where a set of formulae in MEL is viewed as a testimony, is also somewhat reminding of Belnap's set-up based on information sources. His four-valued logic [START_REF] Belnap | A useful four-valued logic[END_REF] extends partial logic to the handling of contradictions. In Belnap's logic, each source of information declares atoms to be true, false or ignored, but sources can be conflicting. It suggests an extension of MEL to the setting where several emitter agents provide information, and conflicts can be handled; preliminary results along this line are in [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics vs. epistemic logic[END_REF]. Another interesting issue is to reconsider basic notions of belief change, like revision and contraction of MEL bases. More generally, assessing the role of a logic such as MEL and its possible extensions (to mutual or common beliefs) in the framework of multiagent systems is a topic for further research.

  (D): ✷α → ✸α.

  and 0 otherwise. In other words, N (A) = 1 corresponds to the epistemic semantics of assertion ✷α in MEL, where [α] = A. Note that E can be defined as follows: w ∈ E if and only if

  C): (✷α ∧ ✷β) → ✷(α ∧ β).RM obtains from K and N if ⊢ PL α → β, via modus ponens. Then M follows from RM. Noticing that K and RM give (✷(α → β) ∧ (✷α)) → ✷(α ∧ β), C follows from this last theorem and ⊢ PL β → (α → β) by another use of RM. Conversely, one can deduce K from a system containing axioms RM, M, C , N. Due to axioms M and C , RM is also equivalent to (E): ✷α ↔ ✷β whenever ⊢ PL α ↔ β. MEL φ, if and only if there is a finite sequence of MEL-formulae φ 1 , . . . , φ n with φ n := φ, and each φ i is either a MEL-axiom, or a member of Γ , or is derived from previous members of the sequence by the rule (MP).

	For any set Γ of MEL-formulae, one defines a compact syntactic consequence relation in MEL (written ⊢ MEL ), in the standard
	way.
	Definition 1. Γ ⊢

  1 if E ⊆ [α];

	0 otherwise.

By construction, v E | φ (in PL semantics) if and only if E | φ (in MEL semantics).

Theorem 1 (Soundness and completeness). For any set Γ ∪ {φ} of MEL-formulae,

Γ ⊢ MEL φ ⇐⇒ Γ | MEL φ. Proof. Soundness is clear. For completeness, suppose Γ ⊢ MEL φ. It means Γ ∪ {K , D, N} ⊢ PL φ. By PL completeness, it follows that there is a valuation v in V MEL such that v | Γ but v | φ. From the previous considerations, the epistemic state E v is such that E v | Γ but E v | φ in the epistemic semantics. ✷

  Thus by converse of deduction theorem and definition of ⊢ MEL , ✷B ⊢ MEL ✷α. ✷ Note that Theorem 2 holds for the fragment of MEL given by the formula scheme with grammar ✷α | φ ∧ ψ , keeping axiom N, and adding inference rules that account for axioms M, C and avoid the use of material implication:

Theorem 2. ✷B ⊢ MEL ✷α, if and only if B ⊢ PL α, for any α ∈ L. Proof. Assume ✷B ⊢ MEL ✷α. By Theorem 1, if E | MEL ✷B, then E | MEL ✷α, for any epistemic state E. Consider in particular E := {w}, where w is any propositional valuation. It is obvious that {w} | MEL ✷β is equivalent to w

| PL β, for any β ∈ L. So, {w} | MEL ✷B is equivalent to w | PL B. Summing up, w | PL B ⇐⇒ {w} | MEL ✷B ⇒ {w} | MEL ✷α ⇐⇒ w | α,

for any propositional valuation w. Thus by completeness of PL, B ⊢ PL α.

For the other direction, using compactness of the PL-consequence and the deduction theorem for PL, we get a finite subset of B, say

B ′ := {α 1 , . . . , α n }, such that ⊢ PL α 1 → (α 2 → . . . (α n → α) . . .). By (RM) and axiom K , ⊢ MEL ✷α 1 → (✷α 2 → . . . (✷α n → ✷α) . . .). (IC): If ✷α ∧ ✷β then ✷(α ∧ β); (IM): If ✷(α ∧ β) then ✷α ∧ ✷β;

• propositional "and" rules in MEL, in the form:

-If φ, ψ then φ ∧ ψ ; -If φ ∧ ψ then φ, if φ ∧ ψ then ψ ; • a modus ponens inference rule: if ✷α and ✷(α → β) then ✷β.

Corollary 2 .

 2 Theorem 2 holds for ✸-formulae, provided ✸B is a singleton (i.e. contains a single ✸-formula): {✸α} ⊢ MEL ✸β, if and only if {α} ⊢ PL β. the equivalence: ⊢ MEL ✸α → ✸β, if and only if ⊢ PL α → β. Note that {✸α} ⊢ MEL ✸β is equivalent to {✷¬β} ⊢ MEL ✷¬α, which, by Theorem 2, is clearly equivalent to {α} ⊢ PL β. ✷ ✷B ⊢ MEL ✸α, if and only if B ⊢ PL α.

	Hence Corollary 3. Therefore, in particular,

Proof.

  It is an n-consensus model of ✷α or a consensus model for n individuals. It can be mapped to a set of PL-interpretations E ν

In this elementary language, the distinction between belief and knowledge cannot be made.

We do not make any presupposition as to whether the beliefs are warranted or not.

A short preliminary version[START_REF] Banerjee | A simple modal logic for reasoning about revealed beliefs[END_REF] of this paper was presented at the 10th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Verona, July 2009, and at the Dagstuhl Seminar on "Information processing, rational belief change and social interaction", August 2009.

Note that V is finite.

There is also the variant with "knows" instead of "believes".

Keep in mind that V is finite.

The counterpart of in the setting of formal concept analysis is called "sufficiency operator" by some authors (see Düntsch and Orłowska[START_REF] Düntsch | Boolean algebras arising from information systems[END_REF]).

Alternatively, other authors use kappa-rankings[START_REF] Williams | Iterated theory base change: a computational model[END_REF] valued on integers to represent graded belief bases. However, the formalism is the same up to a change of the belief scale[START_REF] Dubois | Epistemic entrenchment and possibilistic logic[END_REF].

Acknowledgements

The first author acknowledges the support of IRIT, CNRS, for a visit during which the work was initiated. The second author wishes to thank colleagues for useful discussions on this paper, especially Guillaume Aucher, Laurence Cholvy, Lluis Godo, Andreas Herzig, and Vincenzo Marra. The authors also thank the anonymous reviewers for their valuable comments on previous versions.