A Fuzzy Modal Logic for Belief Functions

1 Introduction

Reasoning under uncertainty is a key issue in many areas of Artificial Intelligence. From a logical view point, uncertainty basically concerns formulas, describing a situation, that can be either true or false, but their truth value is unknown due to incompleteness of the available information. When this uncertainty can be measured, then one may assign to propositions the degree of belief of being true. Among the different models of numerical uncertainty, in the sense of belief, that have been proposed, probability theory is undoubtedly the most relevant, however other interesting models have been also proposed trying to remedy different shortcomings of the pure Bayesian approaches. In particular, Demspter-Shafer belief functions [Shafer, 1975] provide a more general framework to assess uncertainty to events or propositions, generalizing not only the probabilistic model but also for instance the possibilistic model. In this framework propositions can be attached two uncertainty degrees, a lower and an upper estimate, and the lack of evidence on the truth of a proposition does not necessarily induce evidence for the falsity of that proposition.

One may find in the literature a number of uncertainty logics. As for probability, let us mention [Keisler, 1985] for a deep investigation of probabilistic quantifiers (probability of a0 is ✆ ✝ ✟ ✝ a fixed parameter) and [Fagin et al., 1990;

Francesc Esteva

AI Research Institute IIIA - CSIC

08193 Bellaterra, Spain

esteva@iiia.csic.es

Halpern, 1989] for logics to reason explicitly about probabilities; see also [Nilsson, 1982; Bacchus, 1990] for other probabilistic logical formalisms. As for other types of belief, see e.g. [Dubois et al., 1994] for a full overview on possibilistic logic, and [Fagin and Halpern, 1991; Saffiotti, 1992; Sossai et al., 1999] for different proposals of belief function logics. Another type of approaches, that may be called comparative, deal with a binary modality ☛ , the formula a0 ☛ ☞ meaning "belief of a0 is ✍ belief of ☞ "; this was adopted e.g. in [Boutilier, 1992; Bendova and H´ajek, 1993] (possilibity theory) and [Harmanec and H´ajek, 1994] (Dempster-Shafer belief). Let us remark that, as it is obvious, the above list of references of relevant works is far from being exhaustive, it is only for exemplifying purposes.

It is of worth noticing that all the above uncertainty logics (and in many others) are built on the basis that the representation of situations is done by means of two-valued (Boolean) propositions: they can only be either true or false. However, when we need to deal with propositions representing gradual notions ( e.g. high temperature, low income) it is natural to move from two-valued classical logic to a many-valued logical framework where propositions may be attached intermediate truth degrees. This is the realm of fuzzy logic 1 , which is completely different from the one of uncertainty logics, although in both propositions are usually attached with numbers between 0 and 1. It has been repeatedly stressed that truth degrees in fuzzy logic must be carefully and clearly distinguished from belief degrees (probabilities, or more generally belief degrees of Dempster-Shafer theory). Fuzzy logics are logics of comparative truth and are mainly understood as truth-functional: the truth degree of a compound formula (conjunction, disjunction, implication,. . . ) is determined by the truth degrees of its components via truth functions. On the other hand, uncertainty is basically concerned with degrees of belief that two-valued propositions are true. Belief degrees are obviously not truth-functional. This does not prevent to find proposals to extend the various notions of uncertainty to fuzzy propositions and hence to find in the literature also fuzzy belief logics of various kinds, for instance let us mention the paper [H´ajek et al., 1994] fuzzifying the comparative modality ✎ for possibilistic measures over a finitely valued Łukasiewicz logic).

1 Fuzzy logic has been developed as a strictly formal system in both propositional and predicate calculi, see e.g. [H´ajek, 1998].

In ✏ this paper we introduce a new logical approach to reason explicitly about Dempster-Shafer belief functions which combines classical uncertainty measures (probability and belief functions) with elements of fuzzy logic: the basic observation is that "uncertainty" or belief is itself a gradual notion, e.g. a proposition may be totally, quite, more or less, or slightly certain (in the sense of probable, possible, believable, plausible, etc.). Then, one just starts with Boolean formulas a0 and a probability on them; the probability of a0 is taken to be the truth degree of the fuzzy proposition ✑ a0 ✒ ✔ a0 is probable". This was already used in [H´ajek et al., 1995] and continued in [H´ajek, 1998; Godo et al., 2000] to define a fuzzy logic theory for probabilistic reasoning. Here we generalize this approach to deal with belief functions, i.e. we take the following identity

belief degree of a0 = truth degree of ✁ a0 ,

as our working assumption, where ✁ a0 stands for the fuzzy proposition " a0 is believed". For getting a complete axiomatization of "being (highly) believed" we use one of possible definitions of Dempster-Shafer belief, namely as probability of necessity. This enables us to combine the approach of [Godo et al., 2000] with the modal logic S5. In particular, our fuzzy logic is the logic Ł✂ ✄ ☎ "putting Łukasiewicz and Product logic together", which provides a nice and powerful logical setting where arithmetical operations are implicitly available.

We are forced to have extensive preliminaries: Section 2 contains preliminaries on belief functions and modal logic S5, Section 3 preliminaries on the logic Ł✂ ✄ ☎ and a variant of it suitable to handle infinite theories. Section 4 is devoted to the definition of our fuzzy belief logic FB(Ł ✂ ✄ ☎ ) for regular belief functions and main (completeness) results, while Section 5 contains an approach to handle Dempster combination rule in our fuzzy logic setting. Finally, Section 6 discusses a generalization to deal with general belief functions, i.e. belief functions ✖ ✗ ✙ with possibly ✖ ✗ ✙ ✛ ✢ ✤ positive. Due to space limitation proofs are not included here but can be found in [Godo et al., 2001].

2 Preliminaries I

We survey here some basic facts on belief functions. (The basic monograph is [Shafer, 1975].) We are interested in belief functions on propositional formulas in finitely or countably infinitely many propositional variables. Starting from the classical definition of Dempster (using what we call Dempster spaces) we explain a presentation using Kripke models of modal logic as well as a definition using a superadditivity condition. All results of this section, except the last one to the best of our knowledge, are already known modulo possibly a different notation.

Definition 1 A Dempster space (or d-space) is a structure ✦ ✒ ✛ ✧ ✟ ✩ ✟ ✫ ✟ ✭ ✤ where ✧ ✰ ✒ ✢ ✰ ✒ ✩ ✟ ✫ is a mapping of ✧ into the power set ✴ ✛ ✩ ✤ of ✩ and ✭ is a finitely additive probability on an algebra of subsets of ✧ ✷ For ✹ ✺ ✩ ✟ put ✖ ✗ ✙ ✽ ✛ ✹ ✤ ✒ ✭ ❂ ❄ ❆ ✫ ✛ ❄ ✤ ✺ ✹ ❋ (if this set is measurable). ✖ ✗ ✙ ✽ is the belief function given by D. D is regular if

✫ ✛ ❄ ✤ ✰ ✒ ✢ for each ❄ ■ then ✖ ✗ ✙ ✽ is a regular belief function ✛ ✖ ✗ ✙ ✽ ✛ ✢ ✤ ✒ ▲ ✤ ✷

Needless to say, a function ✖ ✗ ✙ mapping (some) subsets of ✩ into ▼ ▲ ✟ ◆ a80 is a belief function iff it is a belief function given by some d-space. Note that it may be given by various d-spaces; only properties independent of the choice of the underlying d-space are of interest.

Let Var be a set of propositional variables ❘ ❙ ✟ ❘ ✄ ✟ ✷ ✷ ✷ and let ✗ ❱ ✛ ✩ ❳ ❨ ❬ ❪ ✤ ❴ ❂ ▲ ✟ ◆ ❋ (value of a propositional variable in a world). The pair ✛ ✦ ✟ ✗ ✤ (or just ✛ ✧ ✟ ✩ ✟ ✫ ✟ ✭ ✟ ✗ ✤ is an evaluated d-space. For each formula a0 built from our propositional variables ✗ ✛ ❄ ✟ a0 ✤ is the truth value of a0 in ❄ defined in the obvious way. The belief of a0 is defined as

A function ✖ ✗ ✙ is a belief function on formulas if for some evaluated d-space ✛ ✦ ✟ ✗ ✤ ✟ ✖ ✗ ✙ ✒ ✖ ✗ ✙ ❣ ✽ ❜ ❞ ❤ ✷ Actually we shall deal only with total belief functions on formulas, i.e. with those belief functions for which the sets of worlds ❂ ❄ ✐ ✩ ❆ ✫ ✛ ❄ ✤ ✺ ❂ ❄ ♥ ❆ ✗ ✛ ❄ ♥ ✟ a0 ✤ ✒ ◆ ❋ ❋ are ✭ -measurable for any formula a0 . Evidently, if a0 and ☞ are logically equivalent then ✖ ✗ ✙ ❣ ♣ ❜ ❞ ❤ ✛ a0 ✤ ✒ ✖ ✗ ✙ ❣ ♣ ❜ ❞ ❤ ✛ ☞ ✤ , i.e. ✖ ✗ ✙ respects logical equivalence.

Now let us introduce some basic concepts of modal logic. Formulas of modal propositional logic are built form propositional variables using connectives and the modality a115 (necessarily); if a0 is a formula then a115 a0 is a formula. A Kripke model for the logic a116 ✉ (briefly a a115 -Kripke model) is a structure ✇ ✒ ✛ ✩ ✟ ① ✟ ✗ ✤ where ① is an equivalence relation on ✩ (reflexive, symmetric and transitive) and ✗ is an evaluation of propositional variables as above. The truth value of a115 a0 is defined as follows: ✗ ✛ ❄ ✟ a115 a0 ✤ ✒ ◆ if for each ❄ ♥ , ❄ ① ❄ ♥ implies ✗ ✛ ❄ ♥ ✟ a0 ✤ ✒ ◆ ✷ A formula a0 is an a116 ✉ -tautology if ✗ ✛ ❄ ✟ a0 ✤ ✒ ◆ for each a115 -Kripke model ✇ ✒ ✛ ✩ ✟ ① ✟ ✗ ✤ and each ❄ ✐ ✩ ✛ a0 is true in each world of each a115 -Kripke model). The following are axioms of a116 ✉ ❱ Axioms of classical propositional logic plus

• (T) a115 a0 ❴ a0
• a115 a0 ❴ a115 a115 a0
• (B) a0 ❴ a115 ⑨ a0

where ⑨ a0 is read "possibly a0 " and stands for ⑩ a115 ⑩ a0 . Deduction rules are modus ponens and necessitation (from a0 deduce a115 a0 ✤ ✷ a116 ✉ is complete with respect to the given semantics; a formula is provable in a116 ✉ iff it is a a116 ✉ -tautology.

A formula is without nested modalities if no box occurs in the scope of other box (box is applied only to box-free formulas). In a116 ✉ ✟ each formula is logically equivalent to a formula without nested modalities. This, together with the known normal form theorem of propositional logic, gives the following important fact.

Fact. If the set Var of propositional variables is finite then there is a finite set ❸ of formulas such that each formula is, over a116 ✉ ✟ logically equivalent to a formula from ❸ .

A a115 -probabilistic Kripke model is a pair ✛ ✇ ✟ ✭ ✤ , or just

✛ ✩ ✟ ① ✟ ✗ ✟ ✭ ✤ , where ✇ is a a115 -Kripke model and ✭ is a probabilistic ❹ (finitely additive) measure on an algebra of subsets of ✩ ✷ ✛ ✇ ✟ ✭ ✤ can be seen as an evaluated d-space ✛ ✦ ✟ ✗ ✤ ✒ ✛ ✩ ✟ ✩ ✟ ✫ ✟ ✭ ✟ ✗ ✤ where ✫ ✛ ❄ ✤ ✒ ❂ ❄ ♥ ✐ ✩ ❆ ❄ ① ❄ ♥ ❋ (the ① -class of ❄ ✤ ✷ Observe that then ✖ ✗ ✙ ❣ ✽ ❜ ❞ ❤ ✛ a0 ✤ ✒ ✭ ✛ ❂ ❄ ❆ ✗ ✛ ❄ ✟ a115 a0 ✤ ✒ ◆ ❋ ✤ , or briefly ✖ ✗ ✙ ✛ a0 ✤ ✒ ✭ ✛ a115 a0 ✤ , which tells us that the belief of a0 is the probability of the necessity of a0 .

Note that the belief function given by a a115 -probabilistic Kripke model is regular, thanks to reflexivity of ① . General (regular and non-regular) belief functions may be obtained e.g. from probabilistic Kripke models of provability logic GL, see [H´ajek, 1995]. We shall come back to general belief functions later in Section 6.

Now assume ✩ be finite non-empty. A basic belief assignment on ✩ is a mapping ❿ ❱ ✴ ✛ ✩ ✤ ❴ ▼ ▲ ✟ ◆ a80 such that ➂ ➃ ➄ ➅ ❿ ✛ ✹ ✤ ✒ ◆ ■ ❿ is regular if ❿ ✛ ✢ ✤ ✒ ▲ ✷ The belief function given by ❿ is defined by

This is indeed a belief function; moreover, given an evaluation ✗ ❱ ✩ ❳ ❨ ❬ ❪ ❴ ❂ ▲ ✟ ◆ ❋ , the corresponding belief function on formulas, ✖ ✗ ✙ ➉ ❜ ❞ ✛ a0 ✤ ✒ ✖ ✗ ✙ ➉ ✛ ❂ ❄ ❆ ✗ ✛ ❄ ✟ a0 ✤ ✒ ◆ ❋ ✤ , is regular iff it is given by a a115 -probabilistic Kripke model; namely by a model ✇ ✒ ✛ ✩ ♥ ✟ ✗ ♥ ✟ ① ✟ ✭ ✤ where

1. ✩ ♥ ✒ ❂ ✛ ➓ ✟ ❄ ✤ ❆ ➓ ✺ ✩ ✟ ❄ ✐ ✩ ❋ ,
2. ✗ ♥ ✛ ✛ ➓ ✟ ❄ ✤ ✟ ❘ ➣ ✤ ✒ ✗ ✛ ❄ ✟ ❘ ➣ ✤ ✟
3. ✛ ➓ ✟ ❄ ✤ ① ✛ a116 ✟ ❄ ✤ iff ➓ ✒ a116 and
4. ✭ is any probability on ✩ ♥ such that ✭ ✛ ❂ ✛ ➓ ✟ ❄ ✤ ❆ ❄ ✐ ➓ ❋ ✤ ✒ ❿ ✛ ➓ ✤ ✷

This construction is from [Harmanec et al., ]. Conversely, each belief function ✖ ✗ ✙ on a finite set ✩ is given by a basic belief assignment defined as follows [Shafer, 1975]:

Note that if Var (the set of propositional variables) is finite and ✖ ✗ ✙ is a belief function on the formulas built from Var, then we may assume that ✖ ✗ ✙ is given by a d-space with ✩ ✒ ➠ ➡ (the set of all ➢ -tuples of zeros and ones). Then if regular, ✖ ✗ ✙ is given by a finite a115 -probabilistic Kripke model.

Let ✛ ✦ ✟ ✗ ✤ be an evaluated d-space. For each ➢ and each tuple of formulas a0 ✄ ✟ ✷ ✷ ✷ ✟ a0 ➡ , the belief function ✖ ✗ ✙ given by ✛ ✦ ✟ ✗ ✤ satisfies the inequality (see[Shafer, 1975]):

We shall call it the generalized super-additivity condition, GSA for short, since it reduces to the usual super-additivity condition for ➢ ✒ ➠ and when a0 ✄ and a0 ☎ are mutually exclusive. Moreover, if ❨ ❬ ❪ is finite and ✖ ✗ ✙ is a function assigning numbers from ▼ ▲ ✟ ◆ a80 to formulas such that

1. ✖ ✗ ✙ ✛ ➵ ❪ ➸ ✗ ✤ ✒ ◆ ✟
2. ✖ ✗ ✙ ✛ ➺ ❬ ✙ ➻ ✗ ✤ ✒ ▲ ✟
3. ✖ ✗ ✙ respects logical equivalence, and
4. ✖ ✗ ✙ satisfies the GSA condition,

then ✖ ✗ ✙ is a regular belief function and the formula above defines a regular basic belief assignment defining ✖ ✗ ✙ ✷ Consequently, ✖ ✗ ✙ is given by a finite a115 -probabilistic Kripke model.

Our last aim in this section is to prove that this result can be extended to the case of Var being countable.

Theorem 1 If ❨ ❬ ❪ is countable and ✖ ✗ ✙ is a function satisfying ✖ ✗ ✙ ✛ ➵ ❪ ➸ ✗ ✤ ✒ ◆ ✟ ✖ ✗ ✙ ✛ ➺ ❬ ✙ ➻ ✗ ✤ ✒ ▲ ✟ the superadditivity condition (SA) and ✖ ✗ ✙ respects logical equivalence then there is a a115 -probabilisticKripke model K defining ✖ ✗ ✙ .

An sketch of the proof goes as follows. Let ➽ ➾ ➚ ✒ ❂ ❘ ✄ ✟ ❘ ☎ ✟ ✷ ✷ ✷ ✟ ❘ ➡ ✟ ✷ ✷ ✷ ❋ , and for each ➢ , let ➪ ➡ be the set of formulas in the variables ❘ ✄ ✟ ✷ ✷ ✷ ✟ ❘ ➡ . Let ✖ ✗ ✙ ➡ the restriction of ✖ ✗ ✙ to ➪ ➡ and let ➶ ➡ ✒ ✛ ✩ ➡ ✟ ✗ ➡ ✟ ① ➡ ✟ ✭ ➡ ✤ be the corresponding a115 -probabilistic Kripke model. Assume the sets ✩ ➡ to be pairwise disjoint and define the structure ✇ ✒ ✛ ✩ ✟ ✗ ✟ ① ✟ ✭ ✤ as follows:

1. ✩ ✒ ➹ ➡ ✩ ➡ .
2. ✗ ✛ ❄ ✟ ❘ ➣ ✤ ✒ ✗ ➡ ✛ ❄ ✟ ❘ ➣ ✤ , if ❄ ✐ ✩ ➡ and ➘ ✍ ➢ ; ✗ ✛ ❄ ✟ ❘ ➣ ✤ ✒ ▲ , otherwise.
3. ① ✒ ➹ ➡ ① ➡ .
4. for each ✹ ✺ ✩ , put ✭ ✛ ✹ ✤ ✒ ➷ if there exists ➢ ❙ such that ✭ ➡ ✛ ✹ ➬ ✩ ➡ ✤ ✒ ➷ for all ➢ ✆ ➢ ❙ , otherwise we let ✭ ✛ ✹ ✤ undefined. Observe that trivially ✭ ✛ ✢ ✤ ✒ ▲ and ✭ ✛ ✩ ✤ ✒ ◆ .

Then one can prove that ✇ ✒ ✛ ✩ ✟ ✗ ✟ ① ✟ ✭ ✤ is a a115 - probabilistic Kripke model such that ✭ ✛ ❂ ❄ ❆ ❄ ❆ ✒ ➱ a115 a0 ❋ ✤ ✒ ✖ ✗ ✙ ✛ a0 ✤ for each modality-free formula a0 .

This result is in the same spirit as the one by Fagin and Halpern [Fagin and Halpern, 1991, Theorem 3.3] connecting belief functions and inner measures induced by probability measures when the set Var of propositional variables is finite.

3 Preliminaries II

Here we survey the underlying system of fuzzy logic we shall use for our belief function logic.

Ł ✂ ✄ ☎ is a logic "putting Łukasiewicz and Product logics together", introduced in [Esteva et al., 2000]. Formulas are built from propositional variables and the truth constants ✃ ▲ and ✃ ✄ ☎ using connectives ❴ Ł ✟ ❴ ❐ ✟ ❮ (Łukasiewicz and Goguen implication and product conjunction) with the following truth functions 2 :

Evaluations of propositional variables ✗ into [0, 1] which are extended to arbitrary formulas using these rules will be called Ł ✂ ✄ ☎ -evaluations. Other definable connectives are:

2 Note that here we work only with the standard semantics, i.e. our set of truth degrees is the unit real interval a222 a223 a224 a225 a226 a227

with the following truth functions associated (as the reader easily verifies):

Definition 2

(i) Ł✂ is the logical system whose axioms and rules are as follows 3 :

• (Ł) Axioms of Łukasiewicz logic (for ❴ Ł ✟ a229 ✟ ✃ ▲ );
• (✂ ) Axioms for product logic (for ❴ ❐ ✟ ❮ ✟ ✃ ▲ );
• ( ⑩ ) ⑩ ❐ a0 ❴ Ł ⑩ Ł a0

The deduction rules are modus ponens and necessitation for a234 : from a0 infer a234 a0 .

(ii) Ł✂ ✄ ☎ is the logic obtained from Ł✂ by adding a truth constant ✄ ☎ together with the axiom: ✄ ☎ a231 Ł ⑩ Ł ✄ ☎ .

In this setting, a theory ➓ is just a set of formulas. A Ł✂ ✄ ☎ - evaluation ✗ is a model of ➓ if ✗ ✛ a0 ✤ ✒ ◆ for each a0 ✐ ➓ . The notion of proof in Ł ✂ ✄ ☎ is as usual.

Theorem 2 Ł ✂ ✄ ☎ is strongly complete for finite theories with respect to the given semantics. That is, if ➓ is finite then ➓ a243 a0 iff ✗ ✛ a0 ✤ ✒ ◆ for any evaluation ✗ model of ➓ .

It is interesting to remark that, as shown in [Esteva et al., 2000], rational truth constants ✃ ❪ (for each rational ❪ ✐ ▼ ▲ ✟ ◆ a80 ✤ are definable in Ł ✂ ✄ ☎ and the logic proves their basic properties. Thus the following definition is sound.

Definition 3 Rational Ł✂ logic, RŁ✂ for short, is the logic obtained from Ł✂ ✄ ☎ by adding the following infinitary rule:

The notion of proof in RŁ ✂ is as follows. If ➓ is a theory over RŁ✂ , then the set a245 a246 a247 ❐ ✛ ➓ ✤ of all provable formulas from ➓ is the smallest theory ➓ ♥ containing ➓ as a subset, containing all axioms of RŁ ✂ and closed under all deduction rules. For simplicity we shall denote a0 ✐ a245 a246 a247 ❐ ✛ ➓ ✤ by ➓ a243 a249 a0 . We shall keep the notation ➓ a243 a0 to denote finitary deduction, i.e. deduction under Ł✂ ✄ ☎ .

3 These axioms are actually a simplified formulation of [Esteva et al., 2000] proposed by P. Cintula in forthcoming paper.

Theorem 3 (Strong completeness) For any theory ➓ over RŁ✂ and any formula a0 , ➓ a243 a249 a0 iff a0 is 1-true in all [0, 1]-valued models of ➓ .

To close this section let us mention that in [Godo et al., 2000] the logics Ł✂ ✄ ☎ and RŁ✂ have been used to build the corresponding fuzzy probability logics FP(Ł ✂ ✄ ☎ ), FP(RŁ ✂ ). In the next section we shall elaborate the corresponding belief logics FB(Ł✂ ✄ ☎ ), FB(RŁ✂ ).

4 A logic for belief functions

After all these preliminaries we are prepared to define our logic. We distinguish two kinds of formulas:

1. Boolean formulas (or S5-formulas) are built from propositional variables ❘ ❙ ✟ ❘ ✄ ✟ ✷ ✷ ✷ using connectives ❴ ✟ ➤ ✟ a233 ✟ ⑩ (say) and the modality a115 as described above. Modality-free formulas do not contain a115 ■ a formula is closed if each propositional variable is in the scope of a modality. Closed formulas without nested modalities are called normal; they are just built form formulas of the form a115 a0 ✟ a0 modality free using the connectives above.
2. P-formulas (or many-valued formulas). Atomic Pformulas have the form ✑ ✛ ✝ ✤ , read "probably ✝ ", where ✝ is a normal S5-formula. P-formulas are built from atomic P-formulas using the connectives of Ł✂ ✄ ☎ , i.e. ❴ Ł ✟ ❴ ❐ ✟ ❮ , and truth constants ▲ and ✄ ☎ . We shall use ✁ a0 for ✑ ✛ a115 a0 ✤ where a0 is a modality-free formula; ✁ a0 reads " a0 is believed". Formulas built from these using Ł✂ ✄ ☎ -connectives and truth-constants are called belief formulas or B-formulas; they are of course particular P-formulas.

Examples: ✛ ❘ a233 a250 ✤ ❴ ❪ is a Boolean, modality free formula, a115 ✛ ❘ a233 a250 ✤ ❴ a115 ❪ is a normal S5-formula, ✑ ✛ a115 ✛ ❘ a233 a250 ✤ ❴ a115 ❪ ✤ is a P-formula, and ✑ ✛ a115 ✛ ❘ a233 a250 ✤ ✤ ❴ Ł ✑ ✛ a115 ❪ ✤ is a B-formula, equivalently expressed as ✁ ✛ ❘ a233 a250 ✤ ❴ Ł ✁ ✛ ❪ ✤ .

From a knowledge representation point of view, we want to point out the rich expressivity B-formulas provide with. As a matter of fact, we can express for instance simple numerical assignments like ✖ ✗ ✙ ✛ a0 ✤ ✆ ▲ ✷ a251 and ✖ ✗ ✙ ✛ ☞ ✤ ✒ ▲ ✷ a252 by formulas ▲ ✷ a251 ❴ a247 ✁ a0 and ▲ ✷ a251 a231 a247 ✁ a0 ; a positive belief ✖ ✗ ✙ ✛ a0 ✤ a244 ▲ by ⑩ ❐ ⑩ ❐ ✁ a0 ; comparisons of beliefs like ✖ ✗ ✙ ✛ a0 ✤ ✍ ✖ ✗ ✙ ✛ ☞ ✤ by the formula ✁ a0 ❴ a247 ✁ ☞ ; or even more complex conditions like ✖ ✗ ✙ ✛ a253 ✤ ✆ ▲ ✷ a251 a211 ✖ ✗ ✙ ✛ a0 ✤ a210 ✖ ✗ ✙ ✛ a242 ✤ a211 ✖ ✗ ✙ ✛ ☞ ✤ by the formula ✛ ✛ ▲ ✷ a251 ❮ ✁ a0 ✤ a228 ✛ ✁ a242 ❮ ✁ ☞ ✤ ✤ ❴ a247 ✁ a253 .

Semantics. Our language is interpreted in the obvious way in a115 -probabilistic Kripke models ✇ ✒ ✛ ✩ ✟ ① ✟ ✗ ✟ ✭ ✤ ✷ For each Boolean a0 and each ❄ ✐ ✩ ✟ ✗ ✛ ❄ ✟ a0 ✤ is defined (and is 0 or 1). Moreover, for each normal S5-formula ✝ ✟ the probability ✭ ✛ ✝ ✤ ✒ ✭ ✛ ❂ ❄ ❆ ✗ ✛ ❄ ✟ ✝ ✤ ✒ ◆ ❋ ✤ is well-defined; then the truth value of ✑ ✛ ✝ ✤ in K is defined as

This extends to other P-formulas using truth connectives of Ł ✂ ✄ ☎ ■ thus a255 ✂ a255 a0 is well defined for each P-formula ✂ ✷ In particular, a255 ✁ a0 a255 a0 is defined for each modality free formula a0 ✷

An obvious alternative semantics for B-formulas is given by an ✄ ✏ arbitrary regular belief function bel on modality-free formulas; take a255 ✁ a0 a255 ☎ ❞ ✝ ✒ ✖ ✗ ✙ ✛ a0 ✤ and extend using truth functions of connectives. Since each belief function on formulas is given by a a115 -probabilistic Kripkemodel this reduces to the former case.

A P-formula ✂ is a 1-tautology (or just tautology) of FB(Ł✂ ✄ ☎ ) if a255 ✂ a255 a0 ✒ ◆ for each a115 -probabilistic Kripke model K. It follows using [H´ajek, 1998] that the following formulas are tautologies, for any normal S5-formulas ✝ ✟ ✠ ❱

• (FP1) ✛ ✑ ✛ ✝ ✤ a229 ✑ ✛ ✝ ❴ ✠ ✤ ✤ ❴ Ł ✑ ✛ ✠ ✤
• (FP2) ✑ ✛ ⑩ ✝ ✤ a231 Ł ⑩ Ł ✑ ✛ ✝ ✤
• (FP3) ✑ ✛ ✝ ➤ ✠ ✤ a231 Ł ✛ ✑ ✛ ✝ ✤ ❴ Ł ✑ ✛ ✝ a233 ✠ ✤ ✤ ❴ Ł ✑ ✛ ✠ ✤ ✷

These three axioms axiomatize the (fuzzy) notion of being probable. Axiom (FP1) says that if both ✝ and ✝ ❴ ✠ are probable, then ✠ is probable as well. Axiom (FP2) says that ✝ is probable iff ⑩ ✝ is not probable. Finally, it is easy to check, by means of the truth function of ❴ a247 , that Axiom (FP3) expresses the condition that the probability of ✝ ➤ ✠ is the sum of the probabilities of ✝ and ✠ minus the probability of ✝ a233 ✠ .

Definition 4

Axioms of FB(Ł ✂ ✄ ☎ ) and FB(RŁ ✂ ) are the following:

• (i) ✝ , for each S5-formula ✝ provable in S5
• (ii) ✑ ✛ ✝ ✤ , for each normal S5-formula ✝ provable in S5 (call this axiom (FB0))
• (iii) The schemes (FP1)-(FP3) above for P-formulas
• (iv) Axioms of Ł ✂ ✄ ☎ for P-formulas.

Deduction rules of FB(Ł✂ ✄ ☎ ) are those of Ł✂ ✄ ☎ (modus ponens and ✎ -necessitation) and deduction rules of FB(RŁ✂ ) are those of RŁ ✂ (the above plus the infinitary rule (IR)).

This is a recursive axiom system since provability in S5 is decidable. Alternatively one may take axioms and rules of S5 (including classical propositional logic) for S5-formulas and add the rule "from ✝ infer ✑ ✛ ✝ ✤ " for a normal S5-formula, in this way one can obtain a system with finitely-many axiom schemes and rules.

Interestingly, one can easily check that FB(Ł✂ ✄ ☎ ) proves the following formulas ✛ a0 ➣ being modality free Boolean):

1. ✑ ✛ a115 a0 ✄ ➤ ✷ ✷ ✷ ➤ a115 a0 ➡ ✤ ❴ Ł ✁ ✛ a0 ✄ ➤ ✷ ✷ ✷ ➤ a0 ➡ ✤
2. ✁ ✛ ◆ ✤
3. ⑩ ✁ ✛ ▲ ✤

Moreover, if a0 ✟ ☞ are Boolean modality free, then

is a derived rule in FB(Ł ✂ ✄ ☎ ). The reader may notice that these theorems and rule correspond to the four properties characterizing belief functions on formulas (see Section 2), in particular (i) above corresponds to the GSA condition. Indeed, in semantic terms (i) expresses the inequality ✖ ✗ ✙ ✛ a0 ✄ ➤ ✷ ✷ ✷ ➤ a0 ➡ ✤ ✆ ✭ ✛ a115 a0 ✄ ➤ ✷ ✷ ✷ ➤ a115 a0 ➡ ✤ , but by the inclusion-exclusion rule for probabilities the last term is ✆ ✏ ➥ ➦ ➧ ➙ ➄ ➨ ✄ ➩ ➩ ➩ ➡ ➭ ✛ ➜ ◆ ✤ ➝ ➙ ➝ ➯ ✄ ✭ ✛ ✑ ➣ ➳ ➙ a115 a0 ➣ ✤ , and since ✑ ➣ ➳ ➙ a115 a0 ➣ is logically equivalent to a115 ✛ ✑ ➣ ➳ ➣ a0 ➣ ✤ , one has ✭ ✛ ✑ ➣ ➳ ➙ a115 a0 ➣ ✤ ✒ ✖ ✗ ✙ ✛ ✑ ➣ ➳ ➣ a0 ➣ ✤ .

After this preparation we can immediately state and prove two completeness theorems for belief theories, i.e. sets of Bformulas. Recall that a115 -probabilistic Kripke models that are models of a belief theory ➓ are in the obvious correspondence with regular belief functions bel that are models of ➓ ✟ i.e. such that a255 ✂ a255 ☎ ❞ ✝ ✒ ◆ for each axiom ✂ ✐ ➓ ✷

Theorem 4 (Completeness)

1. Strong completeness of FB(RŁ ✂ ). Let ➓ be a belief theory and ✂ a belief formula. ➓ a243 a249 ✂ (i.e. ➓ proves ✂ over ① ✓ ✂ ✤ iff a255 ✂ a255 ☎ ❞ ✝ ✒ ◆ for each belief function bel which is a model of ➓ (iff a255 ✂ a255 a0 ✒ ◆ for each a115 - probabilistic Kripke model of ➓ ✤ ✷
2. Strong finite completeness of FB(Ł✂ ✄ ☎ ). Let ➓ be a finite belief theory and ✂ a belief formula. ➓ a243 ✂ ✛ ➓ proves ✂ over Ł ✂ ✄ ☎ ✤ iff a255 ✂ a255 ☎ ❞ ✝ ✒ ◆ for each belief function bel which is a model of ➓ ✷

5 About Dempster's rule

In this section we shall give some hints about how our logical framework is powerful enough to enable the modelling of regular belief functions combination by means of the wellknown Dempster's rule, although in a bit cumbersome way and provided we work with a finite set ➽ ➾ ➚ ✒ ❂ ❘ ✄ ✟ ✷ ✷ ✷ ✟ ❘ ➡ ❋ of propositional variables.

Let us briefly recall that if ❿ ✄ and ❿ ☎ are two regular basic belief assignments on a finite ✩ , then the (regular) basic belief assignment ❿ ✄ ✖ ❿ ☎ corresponding to the Dempster rule combination of ❿ ✄ and ❿ ☎ is defined for ✢ ✰ ✒ ✹ ✺ ✩ as

The key point is that, in a such a finite framework, given a belief function on formulas, we can access to its corresponding mass distribution. Similarly to the fact that the belief of a Booleanmodality-free formula a0 can be obtained as the probability of the modal formula a115 a0 , the corresponding mass assignment for a0 can be obtained as the probability of another related modal formula ✧ a115 a0 . Indeed, let ✇ ✒ ✛ ✩ ✟ ✗ ✟ ① ✟ ✭ ✤ be a a115 -probabilistic Kripke model and let ✖ ✗ ✙ ➱ be its induced belief function, i.e. ✖ ✗ ✙ ➱ ✛ a0 ✤ ✒ a255 ✑ a115 a0 a255 ➱ . Call ❿ ➱ its correspondingmass distribution. Assume a0 to be decomposed in a disjunction of maximally elementary conjunctions (mec's for short), that is, a0 a231 ➤ ★ ➳ ✩ ✫ ✭ a253 , where each a253 is of the form

for some ➟ ✺ ❂ ◆ ✟ ✷ ✷ ✷ ✟ ➢ ❋ . Notice that since we have ➢ propositional variables, we have ➠ ➡ mec's, call them a253 ✄ ✟ ✷ ✷ ✷ ✟ a253 ☎ ✲ . Then one can prove the following lemma.

Lemma 1 For each modality free Boolean formula a0 , let ✧ a115 a0 stand✳ for

Then a255 ✑ ✧ a115 a0 a255 ➱ ✒ ❿ ➱ ✛ a0 ✤ .

Now, since we are able to identify mass distributions, and since Dempster's rule defines a new mass ❿ ✵ from two masses ❿ ✄ and ❿ ☎ with products and sums (available in the Ł✂ and RŁ✂ logics), the rest is easy, although a bit cumbersome as already mentioned. One has to introduce three pairs of modalities ✑ ➣ ✟ a115 ➣ , for ➘ ✒ ◆ ✟ ➠ ✟ ✶ , and construct formulas in the obvious way. Belief formulas now will be built from atomic belief formulas of the form ✑ ➣ a115 ➣ a0 , called ✁ ➣ a0 , using connectives and truth-constants from Ł✂ ✄ ☎ . Analogously to the simple case, we can restrict ourselves to belief Kripke models of the form ➶ ✒ ✛ ✩ ✟ ✗ ✟ ✖ ✗ ✙ ✄ ✟ ✖ ✗ ✙ ☎ ✟ ✖ ✗ ✙ ✵ ✤ , where the ✖ ✗ ✙ ➣ 's are belief functions on ➠ ➅ . For each non-modal formula a0 , let us denote by ✛ ✸ ✁ ✄ ✖ ✸ ✁ ☎ ✤ a0 , the following (cumbersome) formula:

where ➟ ✟ ✼ ✺ ❂ ◆ ✟ ✷ ✷ ✷ ✟ ➠ ➡ ❋ are such that ✛ ✾ ➣ ➳ ➙ a253 ➣ ✤ a233 ✛ ✾ ✯ ➳ ✺ a253 ✯ ✤ a231 a0 . Notice that, due to Lemma 1, the truth value of ✛ ✸ ✁ ✄ ✖ ✸ ✁ ☎ ✤ a0 in the model ✇ ✒ ✛ ✩ ✟ ✗ ✟ ✖ ✗ ✙ ✄ ✟ ✖ ✗ ✙ ☎ ✟ ✖ ✗ ✙ ✵ ✤ is

Then let FB ✵ (Ł✂ ✄ ☎ ) be like FB(Ł✂ ✄ ☎ ) but repeating FB(Ł✂ ✄ ☎ ) axioms for each pair of modalities and having

for each non-empty ➟ ✺ ❂ ◆ ✟ ✷ ✷ ✷ ✟ ➠ ➡ ❋ and

as additional axioms; analogously with FB ✵ (RŁ ✂ ✤ and FB(RŁ✂ ).

Corollary 1 Let ➓ be a belief theory over FB ✵ (RŁ✂ ✤ and let ✂ be belief formula. Then, ➓ a243 a249 ✂ iff a255 ✂ a255 ❣ ☎ ❞ ✝ ❄ ❜ ☎ ❞ ✝ ❅ ❜ ☎ ❞ ✝ ❆ ❤ ✒ ◆ for each triple of belief functions ✛ ✖ ✗ ✙ ✄ ✟ ✖ ✗ ✙ ☎ ✟ ✖ ✗ ✙ ✵ ✤ model of ➓ and with ✖ ✗ ✙ ✵ ✒ ✖ ✗ ✙ ✄ ✖ ✖ ✗ ✙ ☎ . In particular,

for each triple ✛ ✖ ✗ ✙ ✄ ✟ ✖ ✗ ✙ ☎ ✟ ✖ ✗ ✙ ✄ ✖ ✖ ✗ ✙ ☎ ✤ model of ➓ .

6 Final Remarks

In this final section we like to briefly comment about the extension of the approach developed in the previius sections to deal with "general" belief functions. By general we mean regular as well as singular, i.e. belief functions ✖ ✗ ✙ such that ✖ ✗ ✙ ✛ ✢ ✤ can be positive. A ❇ -space as defined in Definition 1 yields general belief functions; if ✖ ✗ ✙ is singular (nonregular), its regularization is defined as

There is no room for full details so we shall only sketch how an extension of our approach covering this can be done.

The main point is that when dealing with modal logic we have to allow possible worlds satisfying a115 ✃ ▲ (where ✃ ▲ is the truth constant for falsity), i.e. to allow for worlds ❄ such that ❄ ① ❄ ♥ for no ❄ ♥ . There are several logics admitting this but to be able to generalize directly our proofs we have to keep the logic as near to S5 as possible. Our proposal is motivated semantically: call ✇ ✒ ✛ ✩ ✟ ① ✟ ✗ ✟ ✭ ✤ a a115 ♥ -probability Kripke model where ✩ ✟ ✗ ✟ ✭ are as above and ① is a symmetric transitive relation, not necessarily reflexive. The modal logic whose models are structures of the form ✛ ✩ ✟ ① ✟ ✗ ✤ , where ① is symmetric and transitive, is known as KB4, a weaker logic than S5 (where axiom T is dropped).

So swichting our base modal logic from S5 to KB4, the reader may go through Sections 2 and 4 generalizing from S5 to KB4 and from regular belief functions to general belief functions. Then define the logics FB ♥ (Ł✂ ✄ ☎ ✤ and FB ♥ (RŁ✂ ✤ modifying the definitions of FB-logics as follows: axioms sub (i) are all KB4-tautologies and sub (ii) all formulas ✑ ✛ ✝ ✤ where ✝ is any normal KB4-tautology. Finally, the completeness Theorem 4 generalizes in the obvious way by replacing FB by FB♥ and deleting all occurrences of the word "regular"). It is important to observe that our generalized fuzzy logic of belief functions can express the regularization of a singular belief function, namely one can check that ✁ ♥ a0 ✒ ✑ ✛ ⑨ ✃ ◆ ✤ ❴ ❐ ✛ ✑ ✛ ⑨ ✃ ◆ ✤ a229 ✑ ✛ a115 a0 ✤ ✤ expresses the regularized belief of a0 .

Finally let us comment how this general approach also covers general belief functions combination by means of Demspter's rule, actually in a simplified way. In such a setting, the (non-normalized) Dempster's combination of two masses ❿ ✄ and ❿ ☎ is defined for any ✹ ✺ ✩ as

where obviously now ✛ ❿ ✄ ✖ ♥ ❿ ☎ ✤ ✛ ✢ ✤ may be positive, even if ❿ ✄ and ❿ ☎ were regular. Then one can just follow the same approach as in Section 5 and define the logics FB♥ ✵ (Ł✂ ✄ ☎ ) and FB ♥ ✵ (RŁ ✂ ✤ as FB ✵ (Ł ✂ ✄ ☎ ) and FB ✵ (RŁ ✂ ✤ respectively but replacing axioms (DR1) and (DR2) just by this one

for each ➟ ✺ ❂ ◆ ✟ ✷ ✷ ✷ ✟ ➠ ➡ ❋ , with the convention that if ➟ ✒ ✢ , then ✾ ➣ ➳ ➙ a253 ➣ is taken as the truth constant ✃ ▲ . Finally one can show that Corollary 2 still remains valid if we replace there normalized Demspter combination ✖ by the non-normalized version ✖ ♥ .

Acknowledgements.

Petr H´ajek acknowledges partial support by the grant No. IAA 1030004 of the Grant Agency of the Academy of Sciences of the Czech Republic. Lluis Godo and Francesc Esteva acknowledges partial support of the bilateral project CSICCNR "Logics for Evidential Theory". The authors also thank the anonymous referees for their useful comments and criticisms.