Trust and Belief, Interrelation Besik Dundua1 and Levan Uridia2 1 DCC-FC & LIACC, University of Porto, Portugal bdundua@dcc.fc.up.pt 2 Universidad Rey Juan Carlos de Madrid, Spain uridia@ia.urjc.es Abstract. We introduce the modal system B2T which is a multi-modal language designed to talk about trust and belief of two agents. The belief operators are based on modal system KS. This gives the main difference with already known system BA introduced by Churn-Jung Liau [2] and also carries its own intuitive meaning. As a main result we prove that B2T is sound and complete with respect to the given semantics, which is a mixture of the Kripke and neighborhood semantics. 1 Introduction In a notion derived from Plato’s dialogue Theaetetus, philosophy has tradition- ally defined knowledge as justified true belief. The relationship between belief and knowledge is that a belief is a knowledge if the belief is true, and if the believer has a justification for believing it is true. Dropping out the part about justification we can express this connection in a standard modal language by well known translation Sp (splitting translation from S5 to KS), The main clause of which states: Sp(Kp) = Bp ∧ p. Mainly because of this connection together with some doxastic properties of the axiom system, the modal logic KS could be adopted as a good concurrent to the classical doxastic logic KD45. First introduced in the 1980s by Segerberg as a modal logic of some other time [8], KS was rediscovered as a modal logic of inequality [5], [7] and recently it was investigated as a doxastic logic which carries quite adequate properties for mod- elling beliefs of agents [1]. In this paper we consider only those agents whose doxastic properties are formalized in the modal logic KS. Different types of trust have been proposed and studied in the disciplines like philosophy, economics, computer science, etc. In this paper we focus on the interrelation of trust and belief in the two agents case. On the one hand, we follow the ideas introduced in [2], but on the other hand, we simplify the language in a sense that we leave only two types of modalities: i as a belief operator of agent i and Ti,j for trust of agent-i in agent-j. So the logic B2T we introduce is especially designed to talk about belief and trust and their interrelation. As for belief operators, as we already mentioned, they satisfy the axioms of KS and this makes the main difference with the logic BA discussed in [2]. The paper is organized in the following way: In section 2 we recall the logic KS, provide basic definitions and some known facts. In section 3 we introduce 35 the logic B2T and also give its semantics on Kripke’s structures. In the same section we prove the main result of the paper which states that the logic B2T is sound and complete with respect to the given semantics. 2 The Modal Logic KS In 1976 Krister Segerberg [8] explicitly formulated a modal logic KS in which the diamond modality ♦ is interpreted as ”somewhere else”. In this section we define the system KS and its Kripke semantics. 2.1 Syntax Definition 2.11 The normal modal logic KS is defined in a standard modal language with infinite set of propositional letters p, q, r, .. and connectives ∧, , ¬, • The axioms are all classical tautologies plus three axioms containing modal operators. Namely: (p → q) → p → q, p ∧ p → p, p → ♦p, where ♦p ≡ ¬¬p. • The rules of inference are: Modus-ponens, Substitution and Necessitation. Observe that doxastic interpretation of the last axiom states that If p is true then agent believes that it is not the case that he believes the negation of p. It is an easy task to show that if we add axiom p → p to the KS we will get the classical epistemic system S5. Following Smullyan [9] this means that if the KS-reasoner is accurate (never believes any false proposition) then his beliefs coincide with his knowledge. 2.2 Kripke semantics Kripke semantics for the modal logic KS is provided by weakly-transitive and symmetric Kripke frames. Below we give the definition of weakly-transitive re- lation. Definition 2.21 We will say that a relation R ⊆ W × W is weakly-transitive if (∀x, y, z)(xRy ∧ yRz ∧ x 6= z ⇒ xRz). Obviously every transitive relation is weakly-transitive also. Moreover it is immediate to notice that weakly-transitive relations differ from transitive ones just by the occurrence of irreflexive points in clusters. As you can see the frame on the picture is weak transitive, but not transitive. 36 The picture represents the diagrammatic view of Kripke structure, where irreflexive x y points are colored by grey and reflexive ones are uncolored. Arrows represent the relation between two distinct points. So as we can pic. 1 see yRx and xRy, but we do not have yRy, which contradicts transitivity, but not weak transitivity as y = y. In the study of modal logic the class of rooted frames plays a central role. Recall that a frame (W, R) is rooted if it contains a point w ∈ W , which can see all other points in W . That is R(w) ⊇ W − {w}, where R(w) is the set of all successors of w. The class of all rooted, weakly-transitive and symmetric frames can be characterized by the property which we call weak - cluster. Definition 2.22 We will say that a relation R ⊆ W × W is weak-cluster if (∀x, y)(x 6= y ⇒ xRy). It is easy to see that every weak-cluster is just a cluster where we allow irreflexive points. We will see the detailed characterization of finite weak-clusters in the next section. The following proposition makes the link between weak- clusters and rooted, weakly-transitive, symmetric frames. Proposition 2.23 A frame (W, R) is rooted, weakly-transitive and symmetric iff it is weak-cluster. Proof. It is immediate that every weak-cluster is rooted, weakly-transitive and symmetric frame. For the other direction let (W, R) be rooted, weakly-transitive and symmetric frame. Let w ∈ W be the root. Take arbitrary two distinct points x, y ∈ W . As w is the root, we have: wRx and wRy. Because of symmetry we get xRw. Now as R is weakly-transitive, from xRy ∧ yRw and x 6= y we get xRy. Hence R is a weak-cluster. For the sake of completeness we will just briefly state the main definitions, like: Kripke model, satisfaction and validity of modal formulas. These definitions are standard and can be found in any modal logic book. Definition 2.24 The pair (W, R), with W an arbitrary set (set of possible worlds) and R ⊆ W × W is called a Kripke frame. If we additionally have a third component V : P rop × W → {0, 1}, then we say that we have a Kripke model M = (W, R, V ) (Here P rop denotes the set of all propositional letters). The satisfaction and validity of a modal formula are defined inductively. We just state the base and modal cases here. 37 Definition 2.25 For a given Kripke model M = (W, R, V ) the satisfaction of a formula at a point w ∈ W is defined inductively as follows: w p iff V (p, w) = 1, the boolean cases are standard, w φ iff (∀v)(wRv ⇒ v φ). We will say that a formula φ is valid in a model (W, R, V ) if for every point w ∈ W we have w φ. We will say that a formula φ is valid in a frame (W, R) if it is valid in every model (W, R, V ) based on a frame (W, R). We will say that a formula φ is valid in a class of frames C if φ is valid in every frame (W, R) ∈ C. So far we defined the modal logic KS syntactically and we gave the definition of weak-cluster relation. The following theorem links these two notions: Theorem 2.26 [4] The modal logic KS is sound and complete w.r.t. the class of all finite, irreflexive weak-cluster relations. Mainly because of the theorem 2.26 the modal logic KS is called the modal logic of inequality. As the reader can easily check the interpretation of box in irreflexive weak-clusters boils down to the following: w φ iff (∀v)(w 6= v ⇒ v φ). 3 Trust In this section we extend the language for multi-agent case and in addition we add modalities for trust. We restrict the language for the case with two agents as far as the other cases (for finite agents) follow as an easy generalizations of two agent case. We take the ideas from [2] and introduce modal logic which has enough expressive power to talk about trust and belief. We do not consider the same language as in [2], but just its fragment, since we are only interested in interrelation between trust and belief. We give the semantics for this logic and as a main result of the paper we prove the completeness of the described logic with respect to the semantics. Main crucial difference from [2] lies in the fact that the doxastic properties of agents follow KS axioms not KD45 axioms as is classically adopted. 3.1 Syntax The language consists of infinite set of propositional letters p, q, r, ..., connectives ∨, ∧, ¬, →, and modalities 1 , 2 T1,2 , T2,1 Axioms:Each i satisfies KS axioms, ` T1,2 p ↔ 1 T1,2 p, ` T2,1 p ↔ 2 T2,1 p. Rules of inference are: Modus ponens and substitution for each modality, necessitation for i where i ∈ {1, 2} and the following rule `Ti,j`p↔q p↔Ti,j q for each 38 Ti,j with i, j ∈ {1, 2} and i 6= j. The desired interpretation of Ti,j p carries the following idea: Agent-i trusts agent-j about the claim p. In these settings the last two axioms have very in- tuitive meaning, mainly: Agent-i trusts agent-j about the claim p iff Agent-i believes that he trusts agent-j about p. Hence trust does not contradict one’s beliefs. These are the only (very natural) restrictions we have on the interrelation between trust and belief. 3.2 Semantics Kripke semantics is provided by bi-relational Kripke frames together with two neighborhood functions. More formally Definition 3.21 A B2T -frame F is a tuple (W, R1 , R2 , u1,2 , u2,1 ), where: W is a set of possible worlds, R1 , R2 ⊆ W × W are weakly transitive and symmetric relations, u1 : W → P P (W ), u2 : W → P P (W ) are functions T (neighborhood maps), such that the following equalities take place: ui,j (w) = v∈Ri (w) ui,j (v), for every i, j ∈ {1, 2} where i 6= j. B2T -model is a pair M = (F, V ), where F is a B2T -frame and V : P rop → P(W ) is a valuation. Definition 3.22 A satisfaction of a formula in a given B2T -model M = (F, V ) and a point w ∈ W is defined inductively as follows: w p iff w ∈ V (p), w ¬α iff w 6 α, w α ∧ β iff w α and w β, w i α iff (∀w0 )(wRi w0 ⇒ w0 α), w Ti,j α iff |α| ∈ ui,j (w). Here |α| denotes the set {v|v φ}. A formula is valid in in a given B2T -model if it is true at every point of the model. A formula is valid in a B2T -frame if it is valid in every model based on the frame. A formula is valid in a class of B2T -frames if it is valid in every frame in the class. Theorem 3.23 The logic B2T is sound and complete with respect to the class of all B2T -frames. Proof. The soundness easily follows by direct check as for completeness, the proof is standard and therefore we just give a sketch. Let W be the set of all maximally consistent subsets of formulas in a logic B2T . Let us define the relations R1 and R2 on W in the following way: For every 39 Γ, Γ 0 ∈ W we define Γ Ri Γ 0 iff (∀α)(i α ∈ Γ ⇒ α ∈ Γ 0 ), where i ∈ {1, 2}. The following lemma is proved in [4] when proving completeness of the logic KS. It also directly follows from Sahlqvist theorem and the observation that KS-axioms characterize the class of all weakly-transitive and symmetric frames. Lemma 1. [4] Each Ri is weakly-transitive and symmetric. So far we defined a set W with two weakly-transitive and symmetric relations R1 , R2 on it. Now we define functions u1,2 and u2,1 in the following way: ui,j (Γ ) = {{Γ 0 |φ ∈ Γ 0 }|Ti,j φ ∈ Γ }. It immediately follows that T ui,j are functions defined from W to P P (W ). Before we show that ui,j (Γ ) = Γ 0 ∈Ri (Γ ) ui,j (Γ 0 ), for every i, j ∈ {1, 2}, where i 6= j and every Γ ∈ W , let us define the valuation and prove the truth lemma. The valuation V is defined in the following way: V (Γ ) = {p|p ∈ Γ }. Lemma 2 (Truth). For every formula α ∈ B2T and every point Γ ∈ W of the canonical model, the following equivalence holds: Γ α iff α ∈ Γ. Proof. The proof goes by induction on the length of formula. Base case follows immediately from the definition of valuation. Assume for all α ∈ B2T with length less then k holds: Γ α iff α ∈ Γ. Let us prove the claim for α with length equal to k. If α is conjunction or negation of two formulas then the result easily follows from the definition of satisfaction relation and the properties of maximal consistent sets, so we skip the proofs. Assume α = i β and assume Γ α. Take a set B = {γ|i γ ∈ Γ }∪{¬β}. The sub claim is that B is inconsistent. Assume not, then there exists Γ 0 ∈ W such that Γ 0 ⊇ B. This by definition of the relation Ri means that Γ Ri Γ 0 . Now as ¬β ∈ Γ 0 , by inductive assumption we get Γ 0 ¬β. Hence we get a contradiction with our assumption that Γ i β. So B is inconsistent. This means that there exists γ1 , γ2 , ...γn ∈ B such that ` γ1 ∧ γ2 ∧ .. ∧ γn → β. Applying necessitation rule for i we get ` i γ1 ∧ .. ∧ i γn → i β so Γ ` i β, hence we get that i β ∈ Γ . We just showed the left-to-right direction of our claim for α = i β. For the right-to-left implication assume that i β ∈ Γ . By definition of Ri for every Γ 0 with Γ Ri Γ 0 we have β ∈ Γ 0 . From this by inductive assumption it follows that Γ 0 ` β. So we imply that Γ i β. Now assume α = Ti,j φ. Assume Γ Ti,j φ. By definition this means that |φ| ∈ ui,j (Γ ). Hence there exists β such that {Γ 00 |β ∈ Γ 00 } = |φ| with Ti,j β ∈ Γ . This means that we have ` β ↔ φ in B2T . Hence by the rule for trust modality we have ` Ti,j β ↔ Ti,j φ. But the last implies that Ti,j φ ∈ Γ . Conversely assume that Ti,j φ ∈ Γ this implies that {Γ 00 |φ ∈ Γ 00 } ∈ ui,j (Γ ). Now by inductive assumption we know that Γ 00 φ iff φ ∈ Γ 00 hence |φ| ∈ ui,j (Γ ). Hence Γ Ti,j φ. 40 Now let us show that the model we constructed falls into the class of B2T - models. The only thing left to show is the following equality: \ ui,j (Γ ) = ui,j (Γ 0 ). Γ 0 ∈Ri (Γ ) Assume X ∈ ui,j (Γ ). This means that X is of the form {Γ 00 |φ ∈ Γ 00 } for some φ with Ti,j φ ∈ Γ . Because of the B2T axioms and because Γ is maximally consistent set, we imply that i Ti,j φ ∈ Γ . From this we imply that Ti,j φ ∈ Γ 0 for every Γ 0 ∈ Ri (Γ ). Now by definition of ui,j this means that {Γ 00 |φ ∈ Γ 00 } ∈ ui,j (Γ 0 )Tand as Γ 0 was arbitrary member of Ri (Γ ), we get that X = {Γ 00 |φ ∈ Γ 00 } ∈ Γ 0 ∈Ri (Γ ) ui,j (Γ 0 ). Conversely assume some set X ⊆ W belongs to Γ 0 ∈Ri (Γ ) ui,j (Γ 0 ). By defini- T tion this means that there exists a formula φ such that Ti,j φ ∈ Γ 0 ∈Ri (Γ ) Γ 0 and T X = {Γ 00 |φ ∈ Γ 00 }. Now as far as (∀Γ 0 )(Γ Ri Γ 0 ⇒ Ti,j φ ∈ Γ 0 ) by truth lemma we get that (∀Γ 0 )(Γ Ri Γ 0 ⇒ Γ 0 Ti,j φ). Hence Γ i Ti,j φ. Now applying axioms for trust modality we get that Γ Ti,j φ and hence X ∈ ui,j (Γ ). This completes the proof. 4 Conclusions As a conclusion we mention that the logic described is very much alike to the fragment of BIT defined in [2] and techniques used are also much similar. The only motivation for considering B2T and hence moving from ”KD45-reasoner” to ”KS-reasoner” lies in the future perspective to generalize the semantics of the logic and impose topology instead of neighborhood maps. It is well known that KS has much closer connection with topology then KD45. As a future work we use the system PρLog [3] to implement a reasoner for reasoning questions in the B2T . 5 Acknowledgments This research has been partially funded by LIACC through Programa de Fi- nanciamento Plurianual of the Fundao para a Cincia e Tecnologia (FCT), by the FCT fellowship (ref. SFRH/BD/62058/2009), by the MCICINN projects TIN2006-15455-CO3 and CSD2007-00022. References 1. P. Blackburn, J.F.A.K. van Benthem, Frank Wolter. Handbook of Modal Logic. 2002. 2. Churn-Jung Liau. Belief, information acquisition, and trust in multi-agent systems - A modal logic formulation. Journal of Artificial Intelligence, 149, 3160, 2003. 41 3. J. Coelho, B. Dundua, M. Florido, and T. Kutsia. A rule-based approach to xml processing and web reasoning. In P. Hitzler and T. Lukasiewicz, editors, RR, volume 6333 of Lecture Notes in Computer Science, pages 164172. Springer, 2010. 4. L. Esakia. Weak transitivity-restitution. Logical Studies 2001, vol 8, 244-255. 5. V. Goranko. Modal definability in enriched language. Notre Dame Journal of For- mal Logic, 31, 81-105, 1990. 6. P.R. Halmos. Algebraic Logic. Chelsea Publishing Company, New York, 1962. 7. M. de Rijke. The Modal Logic of Inequality. J. Symbolic Logic, 57, 566-587, 1992. 8. K. Segerberg. ”Somewhere else” and ”some other time”. In: Wright and wrong: mini-essay in honor of G.H.Wright, Publ. the group in logic and methodology of Real Finland, 61-64, 1976. 9. R. M. Smullyan. What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles. 42