A Logic for Reasoning about Justified Uncertain Beliefs

1 Introduction

Since the seminal work by Hintikka [1962], modal logic has been a standard approach for reasoning about knowledge and belief of intelligent agents [Fagin et al., 1996]. In the epistemic/doxastic reading of modal logics 1 , the formula □ϕ is interpreted as "ϕ is believable" or "ϕ is knowable". However, without explicit justifications, the reasons why ϕ is believed or known are not represented in the logic. By contrast, justification logics (JL) supply the missing component by adding justification terms to epistemic formulas [Artemov and Nogina, 2005; Artemov, 2008; Artemov and Fitting, 2012; Fitting, 2005]. The first member of the JL family is the logic of proofs (LP) proposed in [Artemov, 2001]. Although the original purpose of LP is to formalize the BrouwerHeyting-Kolmogorov semantics for intuitionistic logic and establish the completeness of intuitionistic logic with respect to this semantics, in a more general setting, LP may be regarded as a device that makes reasoning about knowledge explicit and keeps track of the justifications [Artemov, 2008; Artemov and Nogina, 2005].

1 For the purpose of the paper, the difference between belief and knowledge is not important. Hence, hereafter, we use epistemic reasoning to denote reasoning about any kind of informational attitude for an agent.

Churn-Jung Liau

Institute of Information Science, Academia Sinica, Taipei 115, Taiwan liaucj@iis.sinica.edu.tw

One key issue in epistemic reasoning is the modeling of uncertain beliefs [Halpern, 2003]. While there exist many different uncertainty representation formalisms, the possibility theory-based approach [Zadeh, 1978] is the most appropriate one to be integrated into modal logics, because the necessity measure bears a striking similarity to the epistemic modality. In particular, graded modalities with possibility theory semantics have been successfully applied to the representation and reasoning of uncertain beliefs [Dubois et al., 2013; Esteva et al., 1997; Liau and Lin, 1992; 1996]. However, as in the case of classical epistemic logic, graded modal logics cannot keep track of the reasons of uncertain beliefs. Hence, the objective of the paper is to extend the graded modal logics with explicit justifications. We introduce a possibilistic justification logic (PJL) which is regarded as the explicit version of the quantitative modal logic (QML) proposed in [Liau and Lin, 1992]. We present the syntax and semantics of PJL and investigate its meta-properties, such as soundness, completeness, and realizability.

The remainder of the paper is organized as follows. In Section 2, we review the basic ideas of justification logic and quantitative modal logic. In Section 3, we introduce possibilistic justification logic and investigate its meta-properties. In Section 4, we discuss application of PJL to inconsistencytolerant reasoning and compare PJL with related logical systems. In Section 5, we present the conclusions and indicate future research directions.

2 Preliminaries

2.1 Modal logic and justification logic

We start with the syntax and semantics of classical modal logic [Blackburn et al., 2001]. Let PV denote the set of propositional variables. Then, the well-formed formulas (wffs) of the propositional modal logic are defined as follows:

where p ∈ PV , ⊥ is the logical constant representing falsum , ⊃ is the material implication, and □ is the epistemic modality. Other logical connectives such as ⊤, ¬, ∧, ∨, ≡ and modality ♦ are defined as abbreviations as usual. We use L□ and L to denote the propositional modal language and the underlying propositional language respectively.

The wffs of modal logic are semantically interpreted in a Kripke model (possible world model), which is defined as a triple M = 〈W, R, V 〉, where W is a set of possible worlds, R ⊆ W ×W is a binary accessibility relation on W, and V : PV → 2W assigns to each propositional symbol in PV a subset of W. Given a model M, we can define a forcing relation ⊩M between W and L□ by the semantic rules (we usually omit the subscript M for simplicity). In addition to the standard rules for classical connectives, we have w ⊩ □ϕ iff for any u such that (w, u) ∈ R, u ⊩ ϕ. For a given Kripke model M = 〈W, R, V 〉 and a wff ϕ, we can define the truth set of ϕ with respect to M by

We usually drop the subscript and simply write |ϕ| for the truth set of ϕ when the model M is clear from the context. Let Σ be a set of wffs. Then, we use w ⊩M Σ to denote that w ⊩M ψ for all ψ ∈ Σ. Furthermore, a wff ϕ is a logical consequence of Σ, denoted by Σ |= ϕ, if, for any M and w, w ⊩M Σ implies w ⊩M ϕ. A wff ϕ is valid, denoted by |= ϕ, if it is a logical consequence of the empty set.

In JL, in addition to the category of formulas, there is a second category of justifications, which are formal terms built up from constants and variables using various operation symbols. Constants represent justifications for commonly accepted truths--typically axioms, whereas variables denote unspecified justifications. Different JL's allow different operation symbols. However, most of them contain application and sum. Specifically, the justification terms and wffs of the basic JL are formalized as follows:

where p ∈ PV , a is a justification constant, and x is a justification variable. We use LJ to denote the basic JL language. The set of variables appearing in a term t is denoted by V(t) and for a set S of terms, we define V(S) as ⋃t∈S V(t). A term is ground if V(t) = ∅.

JL furnishes an evidence-based foundation for the logic of knowledge with assertions of format t : ϕ, which denotes "t is a justification of ϕ", or more strictly, "t is accepted as a justification of ϕ" [Artemov, 2008]. Semantically, the formula t : ϕ can be regarded as that t is an admissible evidence for ϕ and based on the evidence, ϕ is believed. Thus, the model of JL is the Kripke model of modal logics enriched with an additional evidence component [Artemov, 2008; Fitting, 2005]. This kind of model, called Kripke-Fitting model, is formally defined as a quadruple M = 〈W, R, E, V 〉, where 〈W, R, V 〉 is a Kripke model and E is an admissible evidence function such that E(t, ϕ) ⊆ W for any justification term t and wff ϕ. Intuitively, E(t, ϕ) specifies the set of possible worlds in which t is regarded as admissible evidence for ϕ. In this paper, we consider the minimal justification logic J. For J, it is required that E must satisfy the closure condition with respect to the application and sum operations:

1. Application: E(s, ϕ ⊃ ψ) ∩ E(t, ϕ) ⊆ E(s · t, ψ).
2. Sum: E(s, ϕ) ∪E(t, ϕ) ⊆ E(s + t, ϕ).

The first condition states that an admissible evidence for ϕ ⊃ ψ, which can be regarded as a function that transforms a justification of ϕ to a justification of ψ, can be applied to an admissible evidence for ϕ to obtain an admissible evidence for ψ. The second condition guarantees that adding a piece of new evidence does not defeat the original evidence. That is, s + t is still an admissible evidence for ϕ whenever either s or t is an admissible evidence for ϕ. Note that conflicting evidence is allowed in JL. For example, if s is an admissible evidence for ϕ and t is an admissible evidence for ¬ϕ, then by the second condition above, s + t is an admissible evidence for both ϕ and ¬ϕ. In this case, it means that s and t are in conflict with each other, and we do not exclude such evidence. The forcing relation ⊩M between W and the justification formula t : ϕ then follows the rule:

• w ⊩ t : ϕ iff w ∈ E(t, ϕ) and for any u such that (w, u) ∈ R, u ⊩ ϕ.

2.2 Possibilistic reasoning and modal logic

Possibility theory is developed from fuzzy set theory by Zadeh [1978]. Given a universe W, a possibility distribution on W is a function π : W → [0, 1]. For a given π, we can define possibility and necessity measures Π,N : 2W → [0, 1] respectively as Π(X) = supw∈X π(w) and N(X) = 1 - Π(X), where X is the complement of X with respect to W. Dubois and Prade [1988; 1991] propose the possibilistic logic (PL) based on possibility theory. The wffs of PL based on a propositional language L are of the forms (ϕ Nα) or (ϕ Πα), where ϕ ∈ L and α ∈ (0, 1]. Informally, (ϕ Nα) (resp. (ϕ Πα)) means that the necessity (resp. possibility) of ϕ is at least α. Although PL is useful in reasoning about an agent's uncertain beliefs, it is not suitable for introspective agents, i.e., the agents reasoning about the beliefs of itself. However, by the analogy between necessity (resp. possibility) measure and the modal operator □ (resp. ♦) indicated in [Dubois and Prade, 1988], it is quite easy to extend PL to a graded modal logic that can model uncertain epistemic reasoning [Dubois et al., 2013; Esteva et al., 1997; Liau and Lin, 1992; 1996]. In this paper, we employ the formalism of quantitative modal logic (QML) proposed in [Liau and Lin, 1992; 1996].

To represent nested necessity and possibility measures, QML uses a less cumbersome notation that is compatible with modal operators. In fact, QML can be viewed as a logic with multiple modal operators. Let [α] and [α]+ denote modal operators for any rational α ∈ [0, 1]. Then, the formation rules of QML wffs are as follows:

where p ∈ PV . We also abbreviate ¬[1 - α]¬ϕ and ¬[1 - α]+¬ϕ as 〈α〉+ϕ and 〈α〉ϕ respectively. The intuitive interpretation of [α]ϕ (resp. [α]+ϕ) is that an agent believes ϕ with certainty at least (more than) α. We use LΠ to denote the QML language.

A QML model is a triple M = 〈W, R, V 〉, where W and V are defined as those for modal logic, and R : W×W → [0, 1] is a fuzzy relation on W. For each w ∈ W, a possibility distribution πw can be defined as πw(u) = R(w, u) for all u ∈ W. Let Nw denote the necessity measure corresponding to πw for each w ∈ W. Then, the forcing relation between W and LΠ includes the following two rules:

• w ⊩ [α]ϕ iff Nw(|ϕ|) ≥ α;
• w ⊩ [α]+ϕ iff Nw(|ϕ|) > α.

3 Possibilistic Justification Logic

As JL provides an evidence-based foundation to epistemic logic, we can also combine justification terms with graded modalities in QML to represent uncertain beliefs justified by a piece of evidence. The situations often occur when the evidence is not strong enough to fully support the belief. The resultant logic is called possibilistic justification logic(PJL). The formation rules of PJL wffs are as follows:

where p ∈ PV , α ∈ [0, 1] is a rational number, and t is a justification term formed by the same rules as those in JL. We use LΠJ to denote the PJL language. A rational number α appearing in a wff is called a grade or a degree and we use G(ϕ) to denote the set of grades appearing in a wff ϕ. Also, for a set Σ of wffs, we define G(Σ) as ⋃ϕ∈Σ G(ϕ). Moreover, for any subset F ⊆ [0, 1], we use LΠJ (F ) to denote the fragment of LΠJ in which only grades in F occur.

As the Kripke-Fitting model is an extension of the Kripke model, a PJL model is defined as a quadruple M = 〈W, R, E, V 〉, where 〈W, R, V 〉 is a QML model and the admissible evidence function E is the same as in the KripkeFitting model. The forcing relation ⊩M between W and the uncertain justification formulas t :α ϕ and t :+α ϕ are defined as follows:

• w ⊩ t :α ϕ iff w ∈ E(t, ϕ) and Nw(|ϕ|) ≥ α
• w ⊩ t :+α ϕ iff w ∈ E(t, ϕ) and Nw(|ϕ|) > α

The intuitive interpretation of t :α ϕ is that, according to the evidence t, ϕ is believed with certainty at least α, and t :+α ϕ can be interpreted analogously. The validity of wffs and the notion of logical consequence are defined in the same way as in modal logic. We use |=J Π to denote the validity and logical consequence in PJL.

The validity in PJL can be characterized by the following Hilbert-style axiomatization J Π.

1. Axiom schemata:

• (a) The standard set of axioms for classical propositional logic
• (b) s :α (ϕ ⊃ ψ) ⊃ (t :α ϕ ⊃ s · t :α ψ)
• (c) s :+α (ϕ ⊃ ψ) ⊃ (t :+α ϕ ⊃ s · t :+α ψ)
• (d) s :α ϕ ⊃ s + t :α ϕ and t :α ϕ ⊃ s + t :α ϕ
• (e) s :+α ϕ ⊃ s + t :+α ϕ and t :+α ϕ ⊃ s + t :+α ϕ
• (f) (s :0 ϕ∧ t :α ϕ) ⊃ s :α ϕ (s :0 ϕ∧ t :+α ϕ) ⊃ s :+α ϕ
• (g) t :α ϕ ⊃ t :+β ϕ, if α > β
• (h) t :+α ϕ ⊃ t :α ϕ
• (i) ¬t :+1 ϕ

2. Rules of inference:

• (a) Modus Ponens: from ϕ and ϕ ⊃ ψ, infer ψ;
• (b) Axiom Internalization Rule 2 : from any instance ϕ of the axiom schemata above and any sequence of justification constants c1, c2, . . . , cn, infer cn :1 cn-1 :1 · · · c1 :1 ϕ.

Let Σ be a subset of PJL wffs. Then, an axiomatic proof (or derivation) from Σ is a finite sequence of wffs, each of which is an instance of an axiom schema, an element of Σ, or follows from earlier items by one of the rules of inference; and a wff ϕ is derivable from Σ, denoted by Σ ⊢J Π ϕ, if ϕ is the last line of a proof from Σ. Moreover, ϕ is an axiomatic theorem of the system J Π, denoted by ⊢J Π ϕ, if it is derivable from the empty set. A set Σ is inconsistent if Σ ⊢J Π ⊥, otherwise, Σ is consistent.

The axiom internalization rule behaves like the necessitation rule in modal logic or QML. For the soundness of the rule, we impose a further restriction on the admissible evidence function:

• for any instance ϕ of the axiom schemata above and any sequence of justification constants c1, c2, . . . , cn(n ≥ 1), E(cn, cn-1 :1 · · · c1 :1 ϕ) =W.

Note that the premises of the axiom internalization rule are restricted to instances of axioms instead of any theorems. The main reason of such restriction is that in JL or PJL, justification terms can track the derivation of a theorem. Because justification constants represent atomic derivations which cannot be analyzed further, an axiom that holds without resorting to any deduction process can be simply justified by any justification constant. However, a theorem that is not an axiom must be derived through a complex deduction process whose structure is reflected by justification terms of the theorem. Thus, justification constants are not necessarily applicable to any theorem. Despite the restriction on the axiom internalization rule, internalization of any proof is possible via the following result.

Theorem 1 (Internalization) The system J Π enjoys internalization. That is, for any wff ϕ1, . . . , ϕn, ψ ∈ LΠJ , if

then for any terms t1, . . . , tn, rational numbers α1 . . . , αn ∈ [0, 1], and I ⊆ {1, 2, . . . , n}, there exists a term t such that V(t) ⊆ V({t1, . . . , tn}) and

where α = min1≤i≤n αi. Furthermore, if mini∈I αi > α, then the conclusion of the derivation above can be strengthened to t :+α ψ.

Proof. The theorem can be easily proved by induction on the length of the derivation {ϕ1, . . . , ϕn} ⊢J Π ψ.

A special case of the internalization theorem shows that any proof of an axiomatic theorem can be internalized.

Corollary 1 For any wff ϕ ∈ LΠJ , if ⊢J Π ϕ then there exists a ground term t such that ⊢J Π t :1 ϕ.

2 The rule corresponds to using total constant specification [Artemov, 2008]. For brevity, we do not introduce the notion of constant specification in this paper.

The system J Π is sound and complete with respect to PJL models. Nevertheless, because of the failure of the compactness theorem, the strong completeness of the system is restricted. For example, let Σ = {c :1- 1n ϕ | n > 1}. Then, c :1 ϕ is a logical consequence of Σ. However, because any finite subset of Σ ∪ {¬c :1 ϕ} is obviously satisfiable and any deduction must be finitary, c :1 ϕ is not derivable from Σ. Let us consider a set of wffs Σ ∪ {ϕ} ⊆ LΠJ such that G(Σ ∪ {ϕ}) is finite and let F = {α, 1 - α | α ∈ G(Σ ∪ {ϕ})} ∪ {0, 1} . Then, we can define the worldalternative functions AL,AL+ : 2LΠJ (F) × F → 2LΠJ (F) as follows:

Informally, AL(Γ, α) (resp. AL+(Γ, α)) contains all wffs ϕ such that N(|ϕ|) ≥ α (resp. N(|ϕ|) > α) is implied by formulas in Γ. To establish completeness, we use the standard canonical model construction. A model M = 〈W, R, E, V 〉 is called a canonical model for LΠJ (F) if

• W is the set of all maximal consistent subsets of LΠJ (F). We use Γ,∆, etc. to denote elements of W.
• R satisfies the following two conditions for all Γ, Γ′ ∈ W and α ∈ F :
• if α > 0, thenAL(Γ, α) ⊆ Γ′ iff R(Γ, Γ′ ) > 1-α; - AL+(Γ, α) ⊆ Γ′ iff R(Γ, Γ′ ) ≥ 1-α.
• E(t, ϕ) = {Γ ∈W | ∃α(t :α ϕ ∈ Γ or t :+α ϕ ∈ Γ)}.
• V (p) = {Γ ∈ W | p ∈ Γ}.

The following lemma shows that canonical models indeed exist.

Lemma 1 There exists R satisfying the two conditions for the accessibility relation of a canonical model.

Proof. The result relies on that F is finite. Let us assume that the elements of F are enumerated decreasingly as 1 = α1 > α2 > · · · > αk = 0. Then, for any Γ ∈ W, we have AL+(Γ, α1) = ∅ and for any 1 ≤ i < k,

Hence, for any Γ, Γ′ ∈ W, R(Γ, Γ′ ) can be defined in the following way:

1. if AL+(Γ, αi) ⊆ Γ′ ̸⊇ AL(Γ, αi) for some 1 ≤ i < k, then R(Γ, Γ′ ) = 1 - αi
2. if AL(Γ, αi) ⊆ Γ′ ̸⊇ AL+(Γ, αi+1) for some 1 ≤ i < k, then R(Γ, Γ′ ) = 1 - α for some α ∈ (αi, αi+1)
3. if AL+(Γ, αk) ⊆ Γ′ , then R(Γ, Γ′ ) = 1.

Then, it is easily verified that R satisfies the requirements. The key fact for canonical models is the following Truth Lemma.

Lemma 2 Let M = 〈W, R, E, V 〉 be a canonical model for LΠJ (F). Then, for any ϕ ∈ LΠJ (F) and Γ ∈ W, Γ ⊩M ϕ iff ϕ ∈ Γ.

Proof. The lemma can be proved by induction on the complexity of ϕ. The atomic cases are covered by the definition of V and the cases for Boolean connectives and logical constants are standard. The only interesting cases are ϕ = t :α ψ or ϕ = t :+α ψ. We consider the former case and the latter one is proved analogously.

(⇐): let us consider two cases:

1. If t :α ψ ∈ Γ for some α > 0, then by definition Γ ∈ E(t, ψ) and ψ ∈ AL(Γ, α). Hence, ψ ∈ Γ′ for any Γ′ such that R(Γ, Γ′ ) > 1 - α by the first condition of R. By the induction hypothesis, this means that ΠΓ(|¬ψ|) ≤ 1 - α and NΓ(|ψ|) ≥ α, which leads to Γ ⊩ t :α ψ.
2. If t :0 ψ ∈ Γ (i.e. α = 0), then Γ ∈ E(t, ψ) is sufficient to show that Γ ⊩ t :0 ψ because NΓ(|ψ|) ≥ 0 holds trivially.

(⇒): there are also two cases:

1. If t :0 ψ ̸∈ Γ, then by axioms (g) and (h), Γ ̸∈ E(t, ψ). Hence, Γ ̸⊩ t :0 ψ.
2. If t :α ψ ̸∈ Γ for some α > 0, then we must consider whether t :0 ψ ∈ Γ. In the case that t :0 ψ ̸∈ Γ, we have seen that Γ ̸∈ E(t, ψ) and hence Γ ̸⊩ t :α ψ. Thus, let us assume that t :0 ψ ∈ Γ. We first show that AL(Γ, α) ∪ {¬ψ} is consistent. If this is not the case, then by axioms (b), (c), (g), (h) and the modus ponens rule, we can find a term s such that s :α ψ ∈ Γ and by axiom (f), t :α ψ ∈ Γ, which is contradictory with the assumption. Therefore, there exists a maximal consistent Γ′ such that ¬ψ ∈ Γ′ and R(Γ, Γ′ ) > 1 - α, which means that ΠΓ(|¬ψ|) > 1 - α and NΓ(|ψ|) < α by the induction hypothesis. Consequently, Γ ̸⊩ t :α ψ.

To prove the completeness, let us assume that ϕ is not derivable from Σ. Then, Σ ∪ {¬ϕ} is consistent and can be extended to a maximal consistent subset of LΠJ (F). Hence, by the Truth Lemma, we can find a possible world in a canonical model that satisfies Σ∪ {¬ϕ}. That is, ϕ is not a logical consequence of Σ. Because the soundness of the system can be proved in a standard way, we have the following theorem.

Theorem 2 (Soundness and Completeness) For any Σ ∪ {ϕ} ⊆ LΠJ such that G(Σ ∪ {ϕ}) is finite, we have Σ ⊢J Π ϕ iff Σ |=J Π ϕ.

Obviously, the logic J Π is a conservative extension of the logic J. In other words, we can embed the language LJ into LΠJ by using a straightforward translation mapping τ : LJ → LΠJ that maps each propositional variable into itself, respects the Boolean connectives, and satisfies the following condition:

Then, we have the following result.

Theorem 3 (Conservative extension) For any wff ϕ ∈ LJ , we have |=J ϕ iff |=J Π τ(ϕ).

Proof. Because all axioms and inference rules of J are instances of axioms and inference rules of J Π under the translation, |=J ϕ implies |=J Π τ(ϕ) by the soundness and completeness of both systems. On the other hand, if ̸|=J ϕ, then there exists a Kripke-Fitting model M = 〈W, R, E, V 〉 and a possible world w such that w ̸⊩ ϕ. However, a KripkeFitting model can be regarded as a special case of PJL model and w ⊩ ϕ in a Kripke-Fitting model iff w ⊩ τ (ϕ) in the corresponding PJL model. Therefore, |=J Π τ(ϕ) implies |=J ϕ.

It is well-known that JL can be regarded as an explicit epistemic logic. Thus, the connection between these two logics is that the epistemic formula □ϕ can be informally interpreted as "there exists some justification x such that x : ϕ". This observation leads to the notion of forgetful projection from LJ to L□ which replaces each occurrence of t : ϕ by □ϕ. The forgetful projection always maps valid formulas of JL to valid formula of epistemic logic; and the converse also holds: any valid formulas of epistemic logic is a forgetful projection of some valid formula of JL [Artemov, 2008; Artemov and Fitting, 2012; Fitting, 2013]. This kind of correspondence theorem also generalizes to PJL and QML. A forgetful projection from LΠJ to LΠ replaces each occurrence of t :α ϕ with [α]ϕ for any α > 0, each occurrence of t :0 ϕ with ⊤, and each occurrence of t :+α ϕ with [α]+ϕ for any α ≥ 0. For each wff ϕ ∈ LΠJ , let ϕ0 denote its forgetful projection and for any subset Σ ⊆ LΠJ , let Σ0 = {ϕ0 | ϕ ∈ Σ}. Then, we have the following result.

Theorem 4 (Correspondence theorem) Let J Π denote the set of all PJL theorems and let KΠ + denote the set of all QML theorems in which the modality [0] does not appear. Then, (J Π)0 = KΠ + .

Proof. (Sketch) The easy part is to show that (J Π)0 ⊆ KΠ + because the forgetful projection of the system J Π is derivable from the basic QML system. The hard part is to prove a Realization Theorem which essentially claims that, for any theorem ϕ in KΠ + , there is some way of replacing [α] and [α]+ symbols with justification terms t :α and t :+α respectively to produce a theorem of J Π. There are essentially two methods of establishing realization theorems: the constructive syntactic method due to Artemov [2001] that makes use of cut-free sequent systems for modal logics and the non-constructive semantic method due to Fitting [2005; 2013]. We will use the semantic method in our proof. In the proof, negative occurrences of modalities become justification variables and positive occurrences of modalities become justification terms that may involve those variables. The modality [0] must be specially treated because [0]ϕ is a QML theorem but t :0 ϕ is not. Note that each QML wff can be equivalently transformed into one wff without any occurrence of the [0] modality by replacing each outermost occurrence of [0]ϕ with ⊤.

4 Discussion and RelatedWork

4.1 Discussion

As QML is a modal formulation of PL, it inherits the advantage of PL to allow inconsistency-tolerant reasoning [Dubois et al., 1994]. More specifically, let Σ denote a knowledge base (i.e. a set of wffs) in QML. Then, the inconsistency level of Σ, denoted by Inc(Σ), is the maximum number α such that Σ ⊢ [α]⊥. A deduction of [α]ϕ is nontrivial only when

α > Inc(Σ). In other words, the derivation of a QML formula [α]ϕ from Σ is trivial if [α]⊥ is also derivable from Σ. In this way, QML allows a knowledge base to be inconsistent to some extent; and uncertain beliefs with necessity measures above the inconsistency level are still acceptable. However, instead of simply discarding a large part of information, the occurrence of inconsistency sometimes yields the requirement to update the knowledge base. By adding justification terms to the formulas, it is possible to track the origin of inconsistency which can be used in the update process. The following example illustrates this point.

Example 1 Let us use ϕ1, ϕ2, ϕ3, and ψ to denote "Tweety is a penguin", "Tweety is a bird", "Tweety lives in Zoologischer Garten Berlin", and "Tweety can fly" respectively; and let us assume that our knowledge base is Σ = {c :1 ϕ1, s :1 (ϕ1 ⊃ ϕ2), d1 :0.9 (ϕ1 ⊃ ¬ψ), d2 :0.8 (ϕ2 ⊃ ψ), n :0.8 ϕ3} where c, s, d1, d2, n are justification constants denoting a reliable observation, a strict rule, a quite reliable default rule, a less reliable default rule and a partially reliable information source respectively. Then, by axioms (b), (g), and (h), we can derive (d1 · c) · (d2 · (s · c)) :0.8 ⊥ (recalling that ¬ψ is an abbreviation of ψ ⊃ ⊥) which keeps track of sources of the inconsistency. By using inconsistency-tolerant reasoning, (d1 · c) :0.9 ¬ψ is a nontrivial consequence of Σ, whereas (d2 · (s · c)) :0.8 ψ and n :0.8 ϕ3 are both blocked because of the triviality. Although inconsistency-tolerant reasoning allows us to maintain highly certain information in the knowledge base, it is sometimes not good enough to simply discard less certain information. For example, it seems that n :0.8 ϕ3 is unrelated to the inconsistent information in Σ, but the derivation of n :0.8 ϕ3 is still blocked. In such case, the justification term (d1 · c) · (d2 · (s · c)) for ⊥ will provide a clue to deal with the problem.

By checking the term, we find that it is possible to modify the strength of the least reliable evidence d2 to improve the consistency degree of the knowledge base. The most straightforward method is to remove d2 :0.8 (ϕ2 ⊃ ψ) from Σ. Then, the inconsistency degree of Σ will be reduced to 0. However, the complete removal of d2 :0.8 (ϕ2 ⊃ ψ) seems not very reasonable according to our commonsense. Hence, an alternative way is to change d2 :0.8 (ϕ2 ⊃ ψ) to d2 :0.7 (ϕ2 ⊃ ψ) because the defeating example Tweety may show that the strength of the default rule was set too high. Yet another approach is to keep the default rule unchanged but seek further evidence to increase the reliability of ϕ3. This approach, despite not increasing the consistency of Σ, may suggest that some information independent of the inconsistent part of the knowledge base deserves further investigation. This usually occurs in the context of scientific inquiry.

In the Kripke-Fitting semantics of JL, the truth of a wff t : ϕ in a possible world w depends on two conditions: (1) t is an admissible evidence for ϕ in w and (2) ϕ is believed. However, in the JL language, we cannot describe these two conditions separately. In particular, we cannot assert that t is an admissible evidence for ϕ by using JL formulas. By contrast, the wff t :0 ϕ precisely describes this fact because w ⊩ t :0 ϕ iff w ∈ E(t, ϕ). Indeed, the formula is used in axiom (f) to formalize an implicit assumption in JL. That is, all admissible evidences for the same proposition are treated equally in the sense that if s and t are both admissible evidences for ϕ, then s : ϕ is true iff t : ϕ is true. An implication of the assumption in PJL is that multiple justifications of the same proposition will converge to the strongest justification among them. Indeed, by using axiom (f), we can derive that, if s :α ϕ and t :β ϕ are true, then s :max(α,β) ϕ and t :max(α,β) ϕ are both true. Hence, if there exist multiple justifications for uncertain beliefs on ϕ, then the strongest justified uncertain belief will be chosen and all other justifications are regarded as supporting the uncertain belief to the same extent. The assumption is sometimes regarded as too restrictive. A possibility of lifting the restriction is to associate with each term t an accessibility relation Rt instead of using a single relation R in the PJL model. It may well be worth exploring the impact of the less restrictive semantics.

Mkrtychev semantics is a predecessor of Kripke-Fitting semantics [Mkrtychev, 1997]. Mkrtychev models essentially coincide with single-world Kripke-Fitting models. In such models, the truth value of t : ϕ is determined only by the admissible evidence function E. Interestingly, the information about Kripke structure in Kripke-Fitting models can be completely encoded by the admissible evidence function and consequently, the system J is also complete with respect to Mkrtychev semantics [Artemov, 2008]. However, this is no longer true for PJL. For example, let us consider a set of PJL wffs Σ = {s :0.9 p, ¬s :+0.9 p, t :0.7 q, ¬t :+0.7 q}. Then, Σ is obviously satisfiable in PJL semantics. However, any models of Σ must contain at least two possible worlds to accommodate different necessity values on p and q.

4.2 Related works

In the last decades, the research on JL and its applications to formal epistemology, mathematics, computer science, and AI has been highly active [Artemov and Fitting, 2012]. However, it is only very recently that the integration of uncertainty reasoning with JL started to be an important topic in the discipline. Consequently, only a few works have been done along this direction. The most remarkable example is the logic JU for uncertain justifications proposed in [Milnikel, 2014]. Syntactically, the wffs of JU are defined by

However, its wff t :α ϕ is interpreted quite differently. In a JU model 〈W,R,E, V 〉, the accessibility relation R is crisp but E is defined as a ternary function such that for any term t, possible world w, and wff ϕ, E(w, t, ϕ) = [0, β) or [0, β] for some rational number β ∈ [0, 1]; and w ⊩ t :α ϕ holds if α ∈ E(w, t, ϕ) and for any u such that (w, u) ∈ R, u ⊩ ϕ. Informally, this means that the same wff t :α ϕ represents the uncertain justification of belief and the justification of uncertain belief in JU and PJL respectively. A consequence of the semantic difference is that the forgetful projection of PJL is QML, whereas the forgetful projection of JU should be classical modal logic 3 .

3 Although forgetful projection is not explicitly defined in [Milnikel, 2014], we think the claim is reasonable because by removing the admissible evidence function, a JU model is simply a classical Kripke model.

The logic JU is further extended to fuzzy justification logics in [Ghari, 2014b]. Instead of using classical twovalued logic, the proposed fuzzy justification logics BLJ and RPLJ are based on Hajek's fuzzy basic logic BL and rational Pavelka logic RPL respectively [H´ajek, 1998], where BL has a classical syntax with conjunction (&) and implication (→) as primitive connectives and RPL is an extension of BL that allows rational truth constants α for α ∈ [0, 1]. Hence, in BLJ and RPLJ, a justification formula also has the classical syntax. However, for a BLJ or RPLJ model 〈W,R,E, V 〉, although the accessibility relation R is still crisp, V is now defined as a fuzzy valuation such that V (w, p) ∈ [0, 1] for any possible world w and propositional variable p, besides E(w, t, ϕ) ∈ [0, 1] for any term t, possible world w, and wff ϕ. Then, V is extended to all wffs according to the many-valued interpretation. In particular, V (w, t : ϕ) = E(w, t, ϕ) ⊗ infu:(w,u)∈R V (u, p), where ⊗ is a t-norm that interprets the many-valued conjunction. Therefore, in BLJ and RPLJ, t : ϕ can represent the uncertain justification of belief on vague propositions and their forgetful projections will be the respective fuzzy modal logics.

In addition to possibility theory-based representation, the combination of probabilistic reasoning and JL has been also proposed recently [Kokkinis et al., 2014]. However, instead of considering probabilistic justification of belief or justification of probabilistic belief, the proposed logic PJ aims at reasoning about the probability of justification statements. Hence, the wffs of PJ are Boolean combinations of formulas of the form P≥αϕ where ϕ ∈ LJ and interpreted by probability measures over the space of LJ models. By contrast, it is possible to develop a logic for reasoning about justified probabilistic beliefs using our approach by interpreting t :α ϕ in a structure where the fuzzy accessibility relation is replaced by probability measures over possible worlds.

5 Conclusion

In this paper, we present an extension of JL to PJL in the same way that QML extends classical modal logic. As JL is regarded as an explicit modal logic, PJL can be regarded as an explicit version of QML. Because QML is a modal formulation of PL, it can represent and reason with uncertain beliefs and partial inconsistency. On the other hand, the justification terms in JL can track the derivation process of a deduction and record the structure of a proof. Thus, by combining the advantages of QML and JL, PJL can track the derivation of uncertain belief and locate the source of inconsistency if the belief is partially inconsistent.

Although we only present the basic system of PJL in this paper, it should be clear that PJL is a promising approach for integrating uncertainty formalisms into justification reasoning. As the starting point of a fruitful project, we can see several possible directions for further research including the extension of the basic system with axioms about beliefs like D, 4, 5; the decidability and complexity of the PJL; a constructive proof of the Realization Theorem based on sequent systems [Goetschi and Kuznets, 2012]; multiagent PJL; probabilistic justification logic based on probability modalities [van der Hoek, 1997]; the applications of PJL

to truth maintenance systems [de Kleer, 1993], formal argumentation [Ferretti et al., 2014; Letia and Groza, 2012], and belief fusion [Ghari, 2014a].

Acknowledgments

This work was partially supported by the Ministry of Science and Technology of Taiwan under Grants 103-2410-H-346007-MY2 and NSC 103-2221-E-001-032. We wish to thank the anonymous referees for their constructive suggestions.