Support + Belief = Decision Trust

Alessandro Aldini University of Urbino Carlo Bo, Italy Agata Ciabattoni TU Wien, Austria Dominik Pichler TU Wien, Austria Mirko Tagliaferri¹¹1Corresponding author. Email: [email protected] University of Urbino Carlo Bo, Italy

Abstract

We present SBTrust, a logical framework designed to formalize decision trust. Our logic integrates a doxastic modality with a novel non-monotonic conditional operator that establishes a positive support relation between statements, and is closely related to a known dyadic deontic modality. For SBTrust, we provide semantics, proof theory and complexity results, as well as motivating examples. Compared to existing approaches, our framework seamlessly accommodates the integration of multiple factors in the emergence of trust.

1 Introduction

Decision trust is defined as the willingness to depend on something (or somebody) with a feeling of relative security, although negative consequences are possible [29, 39]. This notion plays a central role in computer-mediated interactions. For instance, in e-commerce, when there is an abundance of vendors in a marketplace offering nearly identical products, customers use trust to decide whom to buy from [50]. Similarly, in the next generation Internet of Things, smart sensors, edge computing nodes, and cloud computing data centers rely on trust to share services such as data routing and analytics [17]. In spite of their differences, in both scenarios, interactions are governed by trust evaluations that depend on various conditions, e.g., security-based policies, reputation scores, Quality of Service (QoS), and the trustee’s (avail)ability to behave as expected by the trustor.

Those facts drove the development of various formal models for assessing trust, see, e.g., [2, 11, 28]. Yet, each existing model relies on specific conditions for the emergence of trust. The conditions are specifically selected depending on the Trust model in use and then applied to a given domain as fundamental requirements enabling trust. However, this specialized approach fails to work in environments where many conditions contribute to the emergence of trust, see, e.g., the Forbes report [49]. This calls for Trust models that can express multifaceted information combined to evaluate the presence or lack of trust in the environment [51]. To address this need, we introduce SBTrust, a logic that allows reasoning about decision trust relying on varied enabling conditions. In our logic, trusting a formula $\varphi$ means that the trustor is willing to accept the formula as being true, although it might be false. This acceptance-based interpretation of trust is compatible with influential conceptual analyses of the notion of trust that show that trusting a proposition boils down to using the proposition as a premise in one’s reasoning, even though the proposition might be false [19].

Concretely, in SBTrust, Trust is a derived operator whose constituents are a Support connective and a belief operator (hence the logic’s name). Whenever it is both believed that a formula $\varphi$ supports a formula $\psi$ , and that $\varphi$ is true, then $\psi$ is $\varphi$ -trusted. The notion of support, establishing a form of positive influence between two statements, is modeled through a novel dyadic operator $\rightsquigarrow$ , where $\varphi\rightsquigarrow\psi$ is read as: in the most likely $\varphi$ -scenarios $\psi$ holds. The operator $\rightsquigarrow$ yields a non-monotonic conditional sharing properties with the KLM logic $\mathbb{P}$ of preferential reasoning [31], but cautious monotonicity. Furthermore, it encompasses additional properties. We characterize $\rightsquigarrow$ with semantics and proof theory; its axioms and rules turn out to axiomatize the flat (i.e., non-nested) fragment of Åqvist system $\mathbb{F}$ [6] – a foundational preference-based logic for normative reasoning. The notion of belief (what is considered to be true from a subjective standpoint) is modeled through the classical belief operator $B$ , obtained through the normal modal logic $\mathbb{KD}4$ . Hence, our Trust operator ( $T_{\varphi}\psi$ ) is built using those ingredients - $(B(\varphi)\land B(\varphi\rightsquigarrow\psi))\rightarrow T_{\varphi}(\psi)$ .

In the following, through a comparison with the literature, we provide motivations for introducing yet a new logical framework for decision trust. The key ingredient is the support operator $\rightsquigarrow$ , for which we discuss in Sect. 2 the (undesired and) required properties. For our logic we present syntax (Sect. 3), semantics (Sect. 4), and establish the connection between $\rightsquigarrow$ and Åqvist system $\mathbb{F}$ . Soundness, completeness, and complexity (for both the satisfiability and the model checking problem) for SBTrust are established in Sect. 5.

1.1 Decision trust: state of the art

Logical formalisms for decision trust can be classified into one of the following three paradigms [7]:

•

Policy-based models: trust is obtained by implementing hard-security mechanisms based on cryptographic protocols and access control, see, e.g., [46]. Logical frameworks for policy-based mechanisms are defined in, e.g., [1, 9].
•

Reputation-based models: trust is obtained through indications of past interactions that are evaluated by gathering and manipulating performance scores for those interactions, see, e.g., [8]. Logical approaches in this setting are, e.g., [3, 36, 42].
•

Cognitive models: trust derives from the combination of various complex factors, including the agent’s disposition and the importance/utility of a situation [38], or the agent’s expectation and willingness [12]; several logics formalize such cognitive aspects [4, 25, 34, 35, 44].

Although models that fall within one given paradigm are employed in real-world applications, see, e.g., [30], they tend to rely on partial features of trust or assume extremely specific conditions, thus are limited. Policy-based models flatten trust on the use of (cryptographic) protocols and regulations that fail whenever they circularly rely on some trust conditions - the problem of trusting the policy-makers [27]. Reputation-based models flatten trust on scores that often represent only a proxy for trust - the problem of the insufficiency of reputation for trust [11]. Differently from the other paradigms, cognitive models of trust can combine various ingredients that reflect agents’ cognitive states, thus capturing a more nuanced notion of trust. However, those models rely on specific definitions of trust taken from cognitive science (see, e.g., the logical model of [25], which is inspired by the cognitive theory of trust studied in [12]) and specify necessary conditions for trust emergence. This creates a trade-off between the effectiveness in modeling various aspects of trust and the complexity in estimating all its constituting elements in real-world environments. The following example better clarifies the difference between the various paradigms.

Example 1.

As a leading global online retailer, Amazon prioritizes building consumer trust to drive transactions on their platform. To this end, the company enforces various protocols and vendor rules. Imagine a customer assessing whether to trust the proposition “Amazon vendor $V_{i}$ is reliable” ( $\boxed{\mathit{GoodV_{i}}}$ ). In a policy-based model of trust, the customer would only be able to trust $\mathit{GoodV_{i}}$ under the conditions that $V_{i}$ successfully fulfills Amazon’s internal policies (e.g., $V_{i}$ is a registered company). Yet, this approach has various drawbacks: $(i)$ the requirements might be tricked, giving the customer a false sense of security and exposing her to scams; $(ii)$ building trust goes beyond regulations, and customers’ trust seldom rely only on vendors abiding to legal and technical policies; $(iii)$ the problem of trust computing would only be shifted from the vendor $V_{i}$ to Amazon and the policies enforced by it. In a reputation-based model, trust in $\mathit{GoodV_{i}}$ can only depend on $V_{i}$ ’s positive reviews. However, this has two limitations: $(i)$ new vendors lack reviews, hindering their ability to establish trust; $(ii)$ reviews can be manipulated, leading to inaccurate trust assessments (e.g., in 2017, The Shed at Dulwich restaurant became London’s number one restaurant on Tripadvisor, although serving fake food). Using a specific cognitive model of trust, it would be possible to compute trust estimations based on cognitive features of the agents involved (e.g., the intention of the vendor to provide a good service). However, by having to choose a specific cognitive model, the features that can be modelled as trust triggers would be limited to the ones indicated by the model itself. Moreover, cognitive models often neglect to include features typical of the other paradigms, i.e., policies and reputation.

2 Support operator

We introduce the support operator $\rightsquigarrow$ . We compare our modeling approach with other approaches used in the literature on non-monotonic reasoning and motivate the axiomatization we have chosen for our operator. Henceforth, we will shorten the reading of $\varphi\rightsquigarrow\psi$ to: given $\varphi$ , then $\psi$ is most likely.

2.1 Why yet another notion of support

Various notions of support and axiomatizations as a conditional operator have been introduced in the literature; see, e.g. [15] for three potential readings of it as an evidence operator, or [16] for a thorough discussion on a dyadic operator for relevance. What all authors agree upon is that the operator should be non-monotonic, i.e., given $\varphi\rightsquigarrow\psi$ , there is no reason why $\varphi\wedge\xi\rightsquigarrow\psi$ should be the case. This is because additional information ( $\xi$ ) may undermine the previously established supporting statement. We also assume that support is a non-monotonic operator. However, we make assumptions that distinguish our view from the existing ones. Specifically, contraposition ( $(\phi\rightsquigarrow\psi)\rightarrow(\neg\psi\rightsquigarrow\neg\phi)$ ) and right weakening (if $\phi\models\psi$ , then $\chi\rightsquigarrow\phi\models\chi\rightsquigarrow\psi$ ) together give monotonicity for the $\rightsquigarrow$ operator. Differently from [14], to avoid monotonicity, we give up contraposition (as motivated through Example 2) rather than right weakening, which is a reasonable assumption (see Sect. 2.2).

Example 2 (Contraposition and Modus Ponens).

Assume that $\mathit{GoodV_{i}}$ supports that $V_{i}$ ’s products are delivered fast ( $\boxed{\mathit{FastV}_{i}}$ ), i.e., $\mathit{GoodV_{i}}\rightsquigarrow\mathit{FastV}_{i}$ . This should not imply that if the delivery is slow, then it is most likely that the vendor is not a good one ( $\neg\mathit{FastV}_{i}\rightsquigarrow\neg\mathit{GoodV_{i}}$ ), as the delay may depend on other reasons. For analogous reasons, we do not have that $\mathit{GoodV_{i}}$ and $\mathit{GoodV_{i}}\rightsquigarrow\mathit{FastV}_{i}$ imply $\mathit{FastV}_{i}$ , meaning that Modus Ponens for $\rightsquigarrow$ does not hold.

To proceed methodically, we draw upon the axiomatizations of non-monotonic conditionals introduced in [31], commonly referred to as KLM systems, as they serve as cornerstones for non-monotonic reasoning. We start by illustrating with an example why the KLM principle of cautious monotonicity $\mathbf{CM}$ is unsuitable for formalizing our concept of support (see also Remark 2):

\mathbf{CM}\quad((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\chi))\rightarrow((\varphi\land\psi)\rightsquigarrow\chi)

Example 3 (CM).

Let $\boxed{\mathit{Def}CV_{i}}$ denote that customer $C$ receives a defective item from vendor $V_{i}$ , and $\boxed{\mathit{Ref}CV_{i}}$ that $C$ is refunded by $V_{i}$ . In the Amazon marketplace, we have that $\mathit{Def}CV_{i}\rightsquigarrow\mathit{Ref}CV_{i}$ . We also have that given $\mathit{Def}CV_{i}$ then it is most likely that $V_{i}$ is not reliable ( $\mathit{Def}CV_{i}\rightsquigarrow\neg\mathit{Good}V_{i}$ ). However, having $\mathit{Def}CV_{i}\land\mathit{Ref}CV_{i}$ does NOT mean that $\neg\mathit{Good}V_{i}$ is most likely. In fact, receiving a refund eases the customer into considering the vendor a good one, and this invalidates CM. Example 12 will show the failure of this inference in our logic.

2.2 Intuitive properties

We introduce the properties that we envision for the concept of support, illustrating their rationale refining the scenario outlined in Example 1. As will be shown in Theorem 1, many of the properties discussed below are inter-derivable, leading to a more concise axiomatization for $\rightsquigarrow$ .

Henceforth, by axioms, we mean axiom schemata. The naming conventions for the considered properties are taken from the KLM systems [31] and $\mathbb{F}$ [6, 41].

As the support operator $\rightsquigarrow$ applies to boolean formulas we expect all classical tautologies to be provable. Moreover, since any fact intuitively supports itself, the axiomatization of $\rightsquigarrow$ should contain the following axiom:

\mathbf{ID}:\varphi\rightsquigarrow\varphi

The presence of this axiom highlights that $\rightsquigarrow$ does not establish a causal relation, see Remark 1. Moreover we want our support system to not support contradictions. In essence, anything supporting a contradiction must be dismissed. This principle is reflected in the following axiom:

\mathbf{ST}:(\varphi\rightsquigarrow\bot)\to\neg\varphi

Example 4.

Let $\boxed{\mathit{Compliant}V_{i}}$ mean that vendor $V_{i}$ is compliant with “Amazon Seller Terms and Conditions” and let $V_{i}$ be a vendor with an average rating of 4.5 stars for her main product $j$ ( $\boxed{\mathit{TopRating}V_{i,j}}$ ). Assume that $\mathit{Compliant}V_{i}$ and $\mathit{TopRating}V_{i,j}$ support that $V_{i}$ is a good vendor, i.e., $(\mathit{Compliant}V_{i}\land\mathit{TopRating}V_{i,j})\rightsquigarrow\mathit{Good}V_{i}$ . This implies that being compliant supports the connection between having good reviews and being a good vendor, as expected by Amazon and their customers, i.e., $\mathit{Compliant}V_{i}\rightsquigarrow(\mathit{TopRating}V_{i,j}\rightarrow\mathit{Good}V_{i})$ .

This example leads to the following axiom (first introduced as a rule in [48]):

\mathbf{SH}:((\varphi\land\psi)\rightsquigarrow\chi)\rightarrow(\varphi\rightsquigarrow(\psi\rightarrow\chi))

that expresses the fact that deductions performed under strong assumptions may be useful even if the assumptions are not known facts.

It is quite natural to assume that if a statement supports two other statements, it supports their conjunction, as expressed by the axiom below:

\mathbf{AND}:((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\chi))\rightarrow(\varphi\rightsquigarrow(\psi\land\chi))

Note that due to ST, this axiom can never be used to derive that a non-contradictory statement supports a contradiction. We illustrate this with the following example, involving the lottery paradox [32], a stumbling block for default reasoning systems (see [43]).

Example 5.

The paradox states that in a fair lottery, it is rational to assume that each individual ticket is likely not to win. By allowing to infer from two statements being likely that their conjunction is also likely, one concludes that two tickets are likely not to win. By iterating this reasoning, we can infer that it is likely that no ticket will win, which contradicts the fact that a winning ticket exists. The paradox does not apply to $\rightsquigarrow$ . Indeed, if we assume that every ticket is most likely not to win, $\top\rightsquigarrow\neg T_{i}$ , we can infer $\top\rightsquigarrow\bigwedge\neg T_{i}$ by AND. Being $\bigwedge\neg T_{i}$ a contradiction, using ST we could derive $\neg\top$ , which is impossible.

A support operator should also satisfy the $\mathbf{CUT}$ axiom, as illustrated by Example 6 below

\mathbf{CUT}:((\varphi\rightsquigarrow\psi)\land((\varphi\land\psi)\rightsquigarrow\chi))\rightarrow(\varphi\rightsquigarrow\chi)

Example 6.

Let $\boxed{\mathit{Auth}V_{i}}$ stand for $V_{i}$ is authenticated on the Amazon marketplace. Obviously, an authenticated and compliant vendor is most likely to be a legitimate business ( $\boxed{\mathit{Legit}V_{i}}$ ), i.e., $(\mathit{Auth}V_{i}\land\mathit{Compliant}V_{i})\rightsquigarrow\mathit{Legit}V_{i}$ . Moreover, due to Amazon’s policies, $\mathit{Auth}V_{i}\rightsquigarrow\mathit{Compliant}V_{i}$ . This implies that given $\mathit{Auth}V_{i}$ it is already most likely that $V_{i}$ is legitimate, $\mathit{Auth}V_{i}\rightsquigarrow\mathit{Legit}V_{i}$ .

Example 7.

Let $\boxed{\mathit{Fair}V_{i}}$ mean that $V_{i}$ abides to the “Acting Fairly” policy of the “Amazon’s Code of Conduct”. Consider the case in which we have both $\mathit{Compliant}V_{i}\rightsquigarrow\mathit{Good}V_{i}$ and $\mathit{Fair}V_{i}\rightsquigarrow\mathit{Good}V_{i}$ . These two facts imply that it should be sufficient to satisfy $\mathit{Compliant}V_{i}$ or $\mathit{Fair}V_{i}$ to be considered a good vendor, i.e., $(\mathit{Compliant}V_{i}\lor\mathit{Fair}V_{i})\rightsquigarrow\mathit{Good}V_{i}$ .

This example leads to the axiom:

\mathbf{OR}:((\varphi\rightsquigarrow\psi)\land(\chi\rightsquigarrow\psi))\rightarrow((\varphi\lor\chi)\rightsquigarrow\psi)

Example 8.

Let $\boxed{\mathit{GoodQoS}V_{i,j}}$ mean that vendor $V_{i}$ offers high QoS while selling product $j$ . Consider a situation in which $V_{i}$ sells two distinct products $a$ and $b$ , using the same commercial infrastructure (same logistics, same customer care, and so on). Hence, it would be absurd that $V_{i}$ offers high QoS only for one of the two products, i.e., $\neg(\mathit{GoodQoS}V_{i,a}\leftrightarrow\mathit{GoodQoS}V_{i,b})\rightsquigarrow\bot$ . Hence whatever $\mathit{GoodQoS}V_{i,a}$ supports, it should also be supported by $\mathit{GoodQoS}V_{i,b}$ , and viceversa.

This example leads to the following axiom:

\textbf{LL+}:(\neg(\varphi\mbox{$\leftrightarrow$}\psi)\rightsquigarrow\bot)\rightarrow((\varphi\rightsquigarrow\chi)\leftrightarrow(\psi\rightsquigarrow\chi))

The first rule we consider is motivated by the example:

Example 9.

Let $\boxed{\mathit{GoodPrice}V_{i}}$ mean that $V_{i}$ prices well her products and $\boxed{\mathit{AmazonChoice}_{i,j}}$ that the product $j$ sold by $V_{i}$ is labeled as an “Amazon’s Choice” product. By Amazon’s policy, $(\mathit{GoodPriceV_{i}}\land\mathit{Fast}V_{i}\land\mathit{TopRating}V_{i,j})\rightarrow\mathit{AmazonChoice}_{i,j}$ . Now, assume $\mathit{Good}V_{i}\rightsquigarrow\mathit{GoodPrice}V_{i}$ (a good vendor is most likely to price well her products), $\mathit{Good}V_{i}\rightsquigarrow\mathit{Fast}V_{i}$ (a good vendor is most likely to deliver her products fast), and $\mathit{Good}V_{i}\rightsquigarrow\mathit{TopRating}V_{i,j}$ (a good vendor is most likely to have good reviews). Hence, all of these supports together should imply that $\mathit{Good}V_{i}$ supports $\mathit{AmazonChoice}_{i,j}$ .

The resulting rule is:

\mathbf{RCK}:\frac{(\varphi_{1}\land\dots\land\varphi_{n})\rightarrow\varphi_{n+1}}{((\psi\rightsquigarrow\varphi_{1})\land\dots\land(\psi\rightsquigarrow\varphi_{n}))\rightarrow(\psi\rightsquigarrow\varphi_{n+1})}

of which Right Weakening (RW), see Remark 1, represents the particular case $n=1$ .

Example 10.

Let $V_{i}$ be a vendor selling product $j$ and assume that $\mathit{GoodQoS}V_{i,j}\rightsquigarrow\mathit{Fast}V_{i}$ and $\neg(\mathit{AmazonChoice}_{i,j}\rightsquigarrow\mathit{Def}CV_{i})$ . If these conditions hold, then customer $C$ will have a good purchasing experience. Given that this implication holds, under the same hypothesis, it follows that $C$ having a negative purchasing experience supports a contradiction.

This example leads to the following “ $\mathbb{S}5$ -like” rule:

\mathbf{S5_{F}}:\frac{((\neg)(\varphi_{1}\rightsquigarrow\psi_{1})\land\dots\land(\neg)(\varphi_{n}\rightsquigarrow\psi_{n}))\rightarrow\chi}{((\neg)(\varphi_{1}\rightsquigarrow\psi_{1})\land\dots\land(\neg)(\varphi_{n}\rightsquigarrow\psi_{n}))\rightarrow(\neg\chi\rightsquigarrow\bot)}

where $(\neg)(\varphi_{i}\rightsquigarrow\psi_{i})$ stands for either $(\varphi_{i}\rightsquigarrow\psi_{i})$ or its negated version $\neg(\varphi_{i}\rightsquigarrow\psi_{i})$ . The rule is named because, when considered alongside other axioms and rules, $\mathbf{S5_{F}}$ grants the operator $\rightsquigarrow$ all the properties of an $\mathbb{S}5$ -modality for the shallow fragment (see Theorem 3). As shown in Sect. 5, $\mathbf{S5_{F}}$ lets the operator $\rightsquigarrow$ behave locally like an absolute operator, playing a crucial role in the completeness proof.

Remark 1.

(Most of) The axioms and rules discussed above are present in well-known systems. For instance, the KLM logic $\mathbb{P}$ of preferential reasoning, which interprets the dyadic operator $\varphi~{}|\!\!\!\sim\psi$ as “ $\varphi$ typically implies $\psi$ ”, contains the rule RW (see below) and the axioms ID, CUT, AND and OR. I/O logics [37] and their causal versions [10], whose dyadic operator is interpreted as a dyadic obligation and a causal relation, respectively, share RW, CUT, AND and OR (but notably not ID). Note that KLM and (deontic and causal) I/O logics also contain the rule $\mathbf{LLE}$ below right:

\mathbf{RW}:\frac{\varphi_{1}\rightarrow\varphi_{2}}{(\psi\rightsquigarrow\varphi_{1})\rightarrow(\psi\rightsquigarrow\varphi_{2})}\qquad\qquad\mathbf{LLE}:\frac{\varphi\leftrightarrow\psi}{(\varphi\rightsquigarrow\chi)\leftrightarrow(\psi\rightsquigarrow\chi)}

which is weaker than the axiom $\mathbf{LL+}$ . An important difference between these logics and our $\rightsquigarrow$ operator is the direct interaction of support formulas and propositional formulas due to the rule $\mathbf{S5_{F}}$ .

3 A logical framework for decision trust

We introduce the logic SBTrust for reasoning about decision trust. SBTrust is obtained by combining the $\rightsquigarrow$ operator with a belief operator $B$ . For the former, we use a (subset of) the discussed axioms and rules and for the latter a $\mathbb{KD}4$ modality²²2Alternatively one could use a $\mathbb{KD}45$ modality, which, however, would include as a side effect negative introspection; see [26] for a discussion of why it might be undesirable in scenarios similar to the ones we discuss.

3.1 Syntax and axiomatization

The language $\mathcal{L}$ of SBTrust consists of a countable set of propositional variables (ranging over $p,q,\dots$ ), the connectives $\wedge$ , $\lor$ , $\to$ , $\leftrightarrow$ and $\neg$ of classical logic, the binary support operator $\rightsquigarrow$ , and the unary belief operator $B$ . $\mathcal{L}$ is defined by the following two layers grammar ( $*\in\{\land,\lor,\to,\leftrightarrow\}$ ):

\begin{array}[]{rcl}\varphi&:=&\bot\mid p\mid\varphi*\varphi\mid\neg\varphi\\ \alpha&:=&\varphi\mid\varphi\rightsquigarrow\varphi\mid B(\alpha)\mid\alpha*\alpha\mid\neg\alpha\end{array}

We use $\varphi,\psi,\chi,\delta$ , and $\pi$ only for propositional logic formulas, and $\alpha$ and $\beta$ for general formulas in $\mathcal{L}$ . $\mathcal{L}_{T}$ and $\mathcal{L}_{CL}$ will denote the set of formulas of SBTrust and of classical propositional logic, respectively. We identify theoremhood in SBTrust with derivability in its Hilbert-style system.

Definition 1.

SBTrust is obtained by extending any axiom system for propositional classical logic: (indicating its axioms by) ( $\mathbf{CL}$ ) and the Modus Ponens rule MP, together with:

For the support operator:

The axiom schemata

\begin{array}[]{ll}(\mathbf{ID})&\varphi\rightsquigarrow\varphi\\ (\mathbf{ST})&(\varphi\rightsquigarrow\bot)\rightarrow\neg\varphi\\ (\mathbf{SH})&((\psi\land\chi)\rightsquigarrow\varphi)\rightarrow(\psi\rightsquigarrow(\chi\rightarrow\varphi))\\ (\mathbf{LL+})&(\neg(\varphi\mbox{$\leftrightarrow$}\psi)\rightsquigarrow\bot)\rightarrow((\varphi\rightsquigarrow\chi)\leftrightarrow(\psi\rightsquigarrow\chi))\end{array}

together with the rules $\mathbf{RCK}$ and $\mathbf{S5_{F}}$ (whose applications must ensure the resulting formulas to be within the language ${\mathcal{L}}$ ).

For the belief operator:

The following axiom schemata

\begin{array}[]{ll}(\mathbf{KB})&B(\alpha\rightarrow\beta)\rightarrow(B(\alpha)\rightarrow B(\beta))\\ (\mathbf{DB})&B(\alpha)\rightarrow\neg B(\neg\alpha)\\ (\mathbf{4B})&B(\alpha)\rightarrow B(B(\alpha))\\ \end{array}

and the Necessitation rule for $B$ ( $\bf NB$ ).

Trust arises as a combination of support and belief.

Definition 2.

$T_{\varphi}\psi:=B(\varphi)\land B(\varphi\rightsquigarrow\psi)$ .

The notion of derivation is the usual one (some care is required to maintain the restrictions on our language), as well as the notion of derivability for a formula $\alpha$ from a set of assumptions $\Phi$ , which we denote as $\Phi\vdash\alpha$ . We write $\vdash\alpha$ iff $\emptyset\vdash\alpha$ . Clearly, in SBTrust, the deduction theorem holds. We now prove that all the axioms and rules stated in Sect. 2.2 are derivable in SBTrust.

Theorem 1.

The rules RW and LLE, as well as the axioms AND, CUT, and OR are derivable in the system for $\rightsquigarrow$ .

Proof.

Trivial for RW, LLE and AND. The CUT axiom follows by $\mathbf{RCK}$ applied to formulas obtained by SH and CL. Axiom OR: by applying LLE to $(\varphi\land(\varphi\lor\chi))\mbox{$\leftrightarrow$}\varphi$ we get $(\varphi\rightsquigarrow\psi)\mbox{$\leftrightarrow$}((\varphi\land(\varphi\lor\chi))\rightsquigarrow\psi$ ); similarly, we get also $(\chi\rightsquigarrow\psi)\mbox{$\leftrightarrow$}((\chi\land(\chi\lor\varphi))\rightsquigarrow\psi$ ). The claim follows by two applications of SH, followed by CL, RCK, ID, AND and RW. Full proof in appendix. ∎

Remark 2.

Another reason for rejecting CM is that, in conjunction with CUT and RW, it permits to derive REC: $((\varphi\rightsquigarrow\psi)\land(\psi\rightsquigarrow\varphi))\rightarrow((\varphi\rightsquigarrow\chi)\leftrightarrow(\psi\rightsquigarrow\chi))$ (derivation can be found in the appendix). REC is too strong for a support operator since two statements that support each other do not necessarily support the same statements. For instance, the proposition $\mathit{GoodV_{i}}$ and the statement ” $V_{i}$ always responds quickly to a customer’s question” may support each other but do not support the same statements; the latter may support that $V_{i}$ uses an AI tool to answer while the former does not.

A strong connection holds between $\rightsquigarrow$ and $\mathbb{F}$ , the dyadic deontic logic introduced in [6] and axiomatized in [41] as follows ( $\bigcirc(\psi/\varphi)$ stands for “ $\psi$ is obligatory under the condition $\varphi$ ”):

•

Axioms:

\begin{array}[]{rl}\mathbf{CL}&\textrm{All truth-functional tautologies}\\ \mathbf{K_{\Box}}&\Box(\varphi\rightarrow\psi)\rightarrow\Box\varphi\rightarrow\Box\psi\\ \mathbf{T}&\Box\varphi\rightarrow\varphi\\ \mathbf{5}&\lozenge\varphi\rightarrow\Box\lozenge\varphi\\ \mathbf{COK}&\bigcirc(\psi\rightarrow\chi/\varphi)\rightarrow(\bigcirc(\psi/\varphi)\rightarrow\bigcirc(\chi/\varphi))\\ \mathbf{Abs}&\bigcirc(\varphi/\psi)\rightarrow\Box\!\bigcirc\!(\varphi/\psi)\\ \mathbf{Nec}&\Box\varphi\rightarrow\bigcirc(\varphi/\psi)\\ \mathbf{Ext}&\Box(\varphi\leftrightarrow\psi)\rightarrow(\bigcirc(\chi/\varphi)\leftrightarrow\bigcirc(\chi/\psi))\\ \mathbf{ID}&\bigcirc(\varphi/\varphi)\\ \mathbf{SH}&\bigcirc(\varphi/\psi\land\chi)\rightarrow\bigcirc(\chi\rightarrow\varphi/\psi)\\ \mathbf{D^{*}}&\lozenge\psi\rightarrow(\bigcirc(\varphi/\psi)\rightarrow\neg\!\bigcirc\!(\neg\varphi/\psi))\end{array}

•

Rules: modus ponens MP and necessitation for $\Box$ .

The flat fragment (i.e., $\Box$ and $\bigcirc$ apply only to formulas of $\mathcal{L}_{CL}$ ) of the language of $\mathbb{F}$ can be translated into our language as follows:

Definition 3.

Let $\chi$ be any formula in the flat fragment of $\mathbb{F}$ . The translation $\chi^{*}$ using $\rightsquigarrow$ is ( $\varphi,\psi\in\mathcal{L}_{CL}$ ):

\begin{array}[]{rclp{1cm}rcl}\varphi^{*}&\mapsto&\varphi&&(\Box\varphi)^{*}&\mapsto&\neg\varphi\rightsquigarrow\bot\\ (\lozenge\varphi)^{*}&\mapsto&\neg(\varphi\rightsquigarrow\bot)&&(\bigcirc(\psi/\varphi))^{*}&\mapsto&\varphi\rightsquigarrow\psi\end{array}

We show that with the exception of $\mathbf{5}$ and $\mathbf{Abs}$ , all axioms and rules of $\mathbb{F}$ (within the flat fragment) are derivable in the axiomatization for $\rightsquigarrow$ . This establishes a first link between $\mathbb{F}$ and $\rightsquigarrow$ .

Theorem 2.

The translation ^∗ of all axioms and rules of $\mathbb{F}$ – but $\mathbf{5}$ and $\mathbf{Abs}$ – are derivable in the axiomatization for $\rightsquigarrow$ .

Proof.

The claim for axioms $\mathbf{T}$ , $\mathbf{Ext}$ , $\mathbf{ID}$ , and $\mathbf{SH}$ directly follows from the translation. For the remaining axioms: The translation ^∗ of D^∗ is $\neg(\varphi\rightsquigarrow\bot)\to\neg((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\neg\psi))$ . Its contraposition $((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\neg\psi))\rightarrow(\varphi\rightsquigarrow\bot)$ is an instance of AND. The translation of $\mathbf{K_{\Box}}$ can be derived by two applications of $\mathbf{ST}$ , the axioms $\mathbf{CL}$ and the rule $\mathbf{S5_{F}}$ . COK follows by $\mathbf{AND}$ , $\mathbf{RW}$ and $\mathbf{CL}$ . Nec follows by $\mathbf{ST}+\mathbf{CL}$ , together with the rules $\mathbf{S5_{F}}$ and $\mathbf{SH}+\mathbf{CL}$ . The Necessitation rule for $\Box$ follows by modus ponens using $\mathbf{RCK}$ and $\mathbf{ID}$ . Full proofs in appendix. ∎

Remark 3.

The translation of axioms Abs and $\mathbf{5}$ from $\mathbb{F}$ results in formulas containing nested applications of the support operator. In Sect. 4, we will see that the axioms and rules for $\rightsquigarrow$ axiomatize the shallow fragment of $\mathbb{F}$ . In this regard, the rule $\mathbf{S5_{F}}$ , which does not correspond to any rule known in the literature, does not follow from the remaining axioms and rules for $\rightsquigarrow$ , and it is needed to derive (some) flat formulas which hold in $\mathbb{F}$ .

Example 11.

Let us see SBTrust at work. Assume that a customer $C$ believes the two formulas supported by $\mathit{Def}CV_{i}$ discussed in Example 3. If $C$ receives a defective item from vendor $V_{1}$ ( $\mathit{Def}CV_{1}$ ), from $B(\mathit{Def}CV_{1})$ and $B(\mathit{Def}CV_{1}\rightsquigarrow\neg\mathit{Good}V_{1})$ we derive $T_{\mathit{Def}CV_{1}}(\neg\mathit{Good}V_{1})$ . Similarly, it also holds that $T_{\mathit{Def}CV_{1}}(\mathit{Ref}CV_{1})$ . Now, assume that $C$ does indeed receive the refund, thus $B(\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1})$ .

We can show that it is not the case that $C$ trusts $V_{1}$ , $\neg T_{\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1}}(\mathit{Good}V_{1})$ . We use the following abbreviations to write a concise derivation: Let $d:=\mathit{Def}CV_{1}$ , $r:=\mathit{Ref}CV_{1}$ , and $g:=\mathit{Good}V_{1}$ , and, by hypothesis, $T_{d}(\neg g)\land T_{d}(r)$ , i.e., $B(d)\land B(d\rightsquigarrow\neg g)\land B(d\rightsquigarrow r)$ . Hence:

\begin{array}[]{llr}(1)&(d\land(d\rightsquigarrow\neg g))\rightarrow\neg(d\rightsquigarrow g)&(\mathbf{ST}\!+\!\mathbf{D^{*}})\\ (2)&((d\rightsquigarrow r)\land\neg(d\rightsquigarrow g))\rightarrow\neg((d\land r)\rightsquigarrow g)&(\mathbf{CUT}\!+\!\mathbf{CL})\\ (3)&(d\land(d\rightsquigarrow\neg g)\land(d\rightsquigarrow r))\rightarrow\neg((d\land r)\rightsquigarrow g)&(1\land 2)\\ \end{array}

Then, applying rule $\bf NB$ to (3) and using the hypothesis together with axiom $\bf KB$ , we derive $B(\neg((d\land r)\rightsquigarrow g))$ . This formula, by axiom $\bf DB$ , finally implies $\neg T_{d\land r}(g)$ . Note that the lack of axiom CM impedes to derive $T_{\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1}}(\neg\mathit{Good}V_{1})$ , as shown in Example 12.

4 Semantics

For evaluating a formula of the form $\varphi\rightsquigarrow\psi$ , we intuitively consider only the most likely $\varphi$ -scenarios and check whether $\psi$ holds in those scenarios. This approach is inspired by preference-based logics [22], in which a conditional statement “If $\varphi$ then $\psi$ ” is interpreted as among the “best” possible scenarios in which $\varphi$ is true, $\psi$ is true as well. Hence the semantics for SBTrust is built on preference-based models [47] (for the support statements) and standard relational models (for the belief operator).

Also used in KLM logics and in Åqvist system $\mathbb{F}$ , preference-based models are triples $\langle S,\succeq,V\rangle$ , where $S$ denotes a set of states, $V$ a valuation function, and the preference relation $\succeq\subseteq S\times S$ orders the states in $S$ . In our context, $w\succeq v$ means that the state $w$ is at least as likely as $v$ ( $\mathbb{F}$ uses a better than interpretation, while the KLM logic $\mathbb{P}$ uses a preferred to interpretation). Although similar to $\mathbb{F}$ and $\mathbb{P}$ , our approach differs from those for two important aspects. First, in our semantics, we include a component for belief formulas. Second, instead of having a unique preference frame, in a Trust frame, the set of states $S$ is partitioned into multiple preference frames $\langle S_{i},\succeq_{i}\rangle$ ; this allows us to consider different support systems within the same model. Note that, without partitioning, the unique given support system would necessarily have to be believed. In our interpretation, a statement $\varphi\rightsquigarrow\psi$ is true in a state $w\in S_{i}$ if among all the $\varphi$ -states in $S_{i}$ ( $||\varphi||_{i}$ ) the most likely $\varphi$ -states in $S_{i}$ ( $\mathit{most}(||\varphi||_{i})$ ) satisfy $\psi$ ; $\mathit{most}(||\varphi||_{i})$ consists of the maximal elements in the set of all $\varphi$ -states of $S_{i}$ according to $\succeq_{i}$ .

In line with systems $\mathbb{F}$ and $\mathbb{P}$ , our semantics include a limitedness condition: $||\varphi||_{i}\not=\emptyset\Rightarrow\mathit{most}(||\varphi||_{i})\not=\emptyset$ . Limitedness allows us to express when a formula $\varphi$ is impossible in a partition $S_{i}$ using $\varphi\rightsquigarrow\bot$ . Hence, limitedness restricts SBTrust to support only non-contradictory options (with the exception of $\bot\rightsquigarrow\bot$ ). Consequently, an agent will never place trust in a blatant contradiction.³³3This is different from trusting contradicting statements separately, which is still possible in SBTrust. The definitions in this section characterize the frames and models on which our logic is based on.

Definition 4 (Trust frame).

Let $\mathcal{F}:=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R\rangle$ where

•

$\langle S,R\rangle$ is a serial and transitive Kripke frame;
•

$(S_{i})_{i\in I}$ is a partition⁴⁴4 $\bigcup_{i\in I}S_{i}=S$ and $\forall i,j\in I:~{}S_{i}\cap S_{j}=\emptyset$ . of $S$ ;
•

For each $i\in I$ : $\langle S_{i},(\succeq_{i})\rangle$ is a preference frame (therefore $\succeq_{i}\subseteq S_{i}\times S_{i}$ ).

Definition 5 (Trust model and truth conditions).

Let $\mathcal{M}:=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R,V\rangle$ where

•

$\mathcal{F}:=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R\rangle$ is a Trust frame;
•

$V:Prop\mapsto 2^{S}$ is a Valuation function;
•

For each $i\in I$ , $\langle S_{i},(\succeq_{i}),V\rangle$ fulfills the limitedness condition: for every propositional formula $\varphi$

$||\varphi||_{i}\not=\emptyset\Rightarrow\mathit{most}(||\varphi||_{i})\not=\emptyset$
•

$\mathcal{M},s\models p$ iff $s\in V(p)$ ;
•

$\mathcal{M},s\models\neg\alpha$ iff $\mathcal{M},s\not\models\alpha$ ;
•

$\mathcal{M},s\models\alpha\land\beta$ iff $\mathcal{M},s\models\alpha$ and $\mathcal{M},s\models\beta$ ;
•

$\mathcal{M},s\models\varphi\rightsquigarrow\psi$ iff $\mathit{most}(||\varphi||_{i})\subseteq||\psi||_{i}$ for $s\in S_{i}$ ;
•

$\mathcal{M},s\models B(\varphi)$ iff $\forall v:(sRv\rightarrow\mathcal{M},v\models\varphi)$

where $||\varphi||_{i}:=\{v\in S_{i}:\mathcal{M},v\models\varphi\}$ and
$\mathit{most}(||\varphi||_{i}):=\{s\in||\varphi||_{i}:\forall v[(v\in||\varphi||_{i}\land v\succeq_{i}s)\rightarrow s\succeq_{i}v]\}$ .

Remark 4.

Three observations: $(i)$ The semantics for formulas containing $\lor,\rightarrow$ and $\leftrightarrow$ are defined through $\neg$ and $\land$ as usual. $(ii)$ We do not assume any property on the relations $\succeq_{i}$ to keep the model as general as possible. $(iii)$ $\mathcal{M},w\models\varphi\rightsquigarrow\psi$ holds if $w$ is part of a set of states in which $\varphi$ supports $\psi$ is true. An agent may or may not believe $\varphi\rightsquigarrow\psi$ , independently from the fact that $\varphi\rightsquigarrow\psi$ holds or not. This gives us the possibility to capture an agent’s misinformation.

The two notions of a formula $\alpha$ being a semantical consequence of a set of formulas $\Phi$ (in symbols: $\Phi\models\alpha$ ) and $\alpha$ being valid (in symbols: $\models\alpha$ ) are defined as usual.

Example 12 (Ctd Ex. 11).

We use our semantics to show that $T_{\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1}}(\neg\mathit{Good}V_{1})$ (i.e., the customer trusts that $V_{1}$ is not a good vendor on the basis of having received a defective item and a refund) does not follow from $T_{\mathit{Def}CV_{1}}(\mathit{Ref}CV_{1})$ and $T_{\mathit{Def}CV_{1}}(\neg\mathit{Good}V_{1})$ . Consider the Trust model $\mathcal{M}:=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R,V\rangle$ , with $I=\{1\}$ , $S_{1}:=\{s,w,v\}$ , $s\succeq_{1}w$ and $w\succeq_{1}v$ for support, $vRs,wRw,sRs$ for belief, and $V(\mathit{Def}CV_{1}):=S$ , $V(\mathit{Ref}CV_{1}):=\{s,v\}$ , $V(\mathit{Good}V_{1}):=\{v\}$ . A graphical representation of $\mathcal{M}$ is below; $d:=\mathit{Def}CV_{1}$ , $r:=\mathit{Ref}CV_{1}$ , $g:=\mathit{Good}V_{1}$ , and solid and dashed arrows represent the preference relation $\succeq_{1}$ and the accessibility relation $R$ , respectively.

Let $v$ be the current state. In $v$ the customer $C$ believes $\mathit{Def}CV_{1}$ and $\mathit{Ref}CV_{1}$ (i.e. $B(\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1})$ ). Since $\mathit{most}(||\mathit{Def}CV_{1}||_{1})=\{s\}\subseteq\{w,s\}=||\neg\mathit{Good}V_{1}||_{1}$ , we have that $\mathcal{M},s\models\mathit{Def}CV_{1}\rightsquigarrow\neg\mathit{Good}V_{1}$ . Hence, $\mathcal{M},v\models B(\mathit{Def}CV_{1}\rightsquigarrow\neg\mathit{Good}V_{1})$ and $\mathcal{M},v\models T_{\mathit{Def}CV_{1}}(\neg\mathit{Good}V_{1})$ . Similarly, $\mathit{most}(||\mathit{Def}CV_{1}||_{1})=\{s\}\subseteq\{v,s\}=||\mathit{Ref}CV_{1}||_{1}$ , we also have that $\mathcal{M},s\models\mathit{Def}CV_{1}\rightsquigarrow\mathit{Ref}CV_{1}$ . Hence, $\mathcal{M},v\models B(\mathit{Def}CV_{1}\rightsquigarrow\mathit{Ref}CV_{1})$ and $\mathcal{M},v\models T_{\mathit{Def}CV_{1}}(\mathit{Ref}CV_{1})$ . Now, since $\mathit{most}(||\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1}||_{1})=\{v,s\}\not\subseteq\{w,s\}=||\neg\mathit{Good}V_{1}||_{1}$ , we have that $\mathcal{M},s\not\models(\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1})\rightsquigarrow\neg\mathit{Good}V_{1}$ . Hence, $\mathcal{M},v\models\neg B((\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1})\rightsquigarrow\neg\mathit{Good}V_{1})$ . Finally, we have $\mathcal{M},v\models\neg T_{(\mathit{Def}CV_{1}\land\mathit{Ref}CV_{1})}(\neg\mathit{Good}V_{1})$ .

We now examine the relation between $\mathbb{F}$ and $\rightsquigarrow$ . Theorem 2 has already highlighted a syntactic connection (from $\mathbb{F}$ to $\rightsquigarrow$ via the translation ^∗ in Def. 3). Here, by using their semantics, we uncover a stronger tie. Recall that $\mathbb{F}$ is sound and complete w.r.t. all preference models $\langle S,\succeq,V\rangle$ which fulfil the limitedness condition, see [41]. We denote by $\models^{\mathbb{F}}$ the semantical consequence relation in $\mathbb{F}$ .

Theorem 3.

For any set of formulas $\Gamma$ and formula $\alpha$ in the language of $\mathbb{F}$ that do not contain nested modal operators, we have: $\Gamma\models^{\mathbb{F}}\alpha\Leftrightarrow\Gamma^{*}\models\alpha^{*}$ .

Proof.

Both directions proceed by contraposition.

$(\Rightarrow)$ We show that given a Trust model invalidating the semantical consequence for support we can find a preference model invalidating the semantical consequence for $\mathbb{F}$ . Assume that $\Gamma^{*}\not\models\alpha^{*}$ . Hence, there exists a Trust model $\mathcal{M}=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R,V\rangle$ and a state $s\in S_{i}$ such that $\forall\beta^{*}\in\Gamma:\mathcal{M},s\models\beta^{*}$ and $\mathcal{M},s\not\models\alpha^{*}$ . We cut down the Trust model into a preference model as follows $\mathcal{M^{\prime}}:=\langle S_{i},\succeq_{i},V\rangle$ . By definition, $\mathcal{M}^{\prime}$ is a preference model fulfilling the limitedness condition.⁵⁵5In [41], the limitedness condition is stated for every formula of $\mathbb{F}$ . Since the truth sets of obligations and modalities are those of $\top$ or $\bot$ , our limitedness condition is equivalent to the one given in $\mathbb{F}$ . Observe that no formula in $\Gamma^{*}\cup\{\alpha^{*}\}$ contains the operator $B$ . Hence, the evaluation of the formulas in $\Gamma^{*}\cup\{\alpha^{*}\}$ at the state $s\in S_{i}$ coincides with the evaluation of the formulas in $\Gamma\cup\{\alpha\}$ in $\mathcal{M}$ . This lets us conclude $\forall\beta\in\Gamma:\mathcal{M}^{\prime},s\models\beta$ and $\mathcal{M}^{\prime},s\not\models\alpha$ .

$(\Leftarrow)$ Given a preference model invalidating $\Gamma\models^{\mathbb{F}}\alpha$ , we provide a Trust model invalidating $\Gamma^{*}\models\alpha^{*}$ . Assume to have the preference model $\mathcal{M}=\langle S,\succeq,V\rangle$ , fulfilling the limitedness condition and a state $s\in S$ such that $\forall\gamma\in\Gamma:\mathcal{M},s\models\gamma$ and $\mathcal{M},s\not\models\alpha$ . We extend it into a Trust model with only one element in the partition, as follows $\mathcal{M^{\prime}}:=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},V,R\rangle$ , with $I:=\{1\}$ , $S_{1}:=S$ , $\succeq_{1}:=\succeq$ and $R:=S\times S$ . By definition, $\mathcal{M}^{\prime}$ is a Trust model. Again no formula in $\Gamma^{*}\cup\{\alpha^{*}\}$ contains the operator $B$ . Hence the evaluation of the formulas in $\Gamma^{*}\cup\{\alpha^{*}\}$ at the state $s\in S$ coincides with the evaluation of the formulas in $\Gamma\cup\{\alpha\}$ in $\mathcal{M}$ . This lets us conclude $\forall\beta^{*}\in\Gamma^{*}:\mathcal{M}^{\prime},s\models\beta^{*}$ and $\mathcal{M}^{\prime},s\not\models\alpha^{*}$ . ∎

By the Soundness and Completeness of SBTrust w.r.t. Trust models, proved in the next section, it follows that the axioms and rules of $\rightsquigarrow$ axiomatize the flat fragment of $\mathbb{F}$ .

5 Soundness, completeness and complexity of SBTrust

We start with the soundness of SBTrust w.r.t. Trust models.

Theorem 4 (Soundness).

Given $\Phi\subseteq\mathcal{L}_{T}$ and $\alpha\in\mathcal{L}_{T}$ it holds that: $\Phi\vdash\alpha\Rightarrow\Phi\models\alpha$ .

Proof.

Proceed, as usual, by induction of the length of the derivation. We distinguish cases according to the last rule applied, showing the details of the cases for the axiom LL+ and the rule $\mathbf{S5_{F}}$ .

LL+: Given a Trust model $\mathcal{M}=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R,V\rangle$ and a state $s\in S_{i}$ such that $\mathcal{M},s\models\neg(\varphi\mbox{$\leftrightarrow$}\psi)\rightsquigarrow\bot$ , then we get $\mathit{most}(||\neg(\varphi\mbox{$\leftrightarrow$}\psi)||_{i})\subseteq\emptyset$ . Given the limitedness assumption, this is equivalent to $||\neg(\varphi\mbox{$\leftrightarrow$}\psi)||_{i}=\emptyset$ and furthermore to $||\varphi\mbox{$\leftrightarrow$}\psi||_{i}=S_{i}$ . Hence, $\varphi$ and $\psi$ are equivalent in every state of $S_{i}$ . Therefore the sets $\mathit{most}(||\varphi||_{i})$ and $\mathit{most}(||\psi||_{i})$ coincide, i.e., $\mathcal{M},s\models(\varphi\rightsquigarrow\chi)\mbox{$\leftrightarrow$}(\psi\rightsquigarrow\chi)$ .

$\mathbf{S5_{F}}$ : Given a Trust model $\mathcal{M}=\langle S,(S_{i})_{i\in I},(\succeq_{i})_{i\in I},R,V\rangle$ , we assume $((\neg)(\varphi_{1}\rightsquigarrow\psi_{1})\land\dots\land(\neg)(\varphi_{n}\rightsquigarrow\psi_{n}))\rightarrow\chi$ to be true in every state of $\mathcal{M}$ . Given a state $s\in S_{i}$ such that $\mathcal{M},s\models((\neg)(\varphi_{1}\rightsquigarrow\psi_{1})\land\dots\land(\neg)(\varphi_{n}\rightsquigarrow\psi_{n}))$ holds, it follows that $\forall w\in S_{i}$ $\mathcal{M},w\models((\neg)(\varphi_{1}\rightsquigarrow\psi_{1})\land\dots\land(\neg)(\varphi_{n}\rightsquigarrow\psi_{n}))$ because by virtue of the semantics of $\rightsquigarrow$ , all the states of a given partition class satisfy the same (negated) support formulas. Therefore, we have that $\forall w\in S_{i}$ $\mathcal{M},w\models\chi$ , which means $||\neg\chi||_{i}=\emptyset$ and finally $\mathcal{M},s\models\neg\chi\rightsquigarrow\bot$ . ∎

Completeness is shown via the canonical model construction, adapted to our framework from the technique outlined in [22]. The needed modifications are the following. First, we have to ensure that SBTrust allows us to derive all the axioms and rules required for the construction to proceed. Furthermore, unlike the models considered in [22], Trust models incorporate multiple preference frames, the belief operator $B$ , and include the limitedness condition.

The modifications are implemented as follows. The required axioms and rules for their proof to go through are those of $\mathbb{F}$ without $\mathbf{D^{*}}$ (which corresponds to limitedness). In Sect. 3.1 we have shown that with the exception of 5 and Abs the axioms of $\mathbb{F}$ are derivable in SBTrust. We prove that we can derive all the necessary properties of the canonical model even in the absence of axioms 5 and Abs, by relying on other rules of SBTrust, primarily on $\bf S5_{F}$ . The multiple preference frames are handled by partitioning the maximal consistent sets used in the canonical model construction into equivalence classes containing the same support formulas. The addition of belief is easy: We equip the canonical model with the accessibility relation in the usual Kripke fashion. Incorporating the limitedness condition poses the challenge of guaranteeing that, in every preference model of our canonical model, each non-empty set $||\varphi||_{i}$ contains a maximal element according to the preference relation. We address this by using the axiom ST.

Definition 6.

A set $\Gamma\subseteq\mathcal{L}_{T}$ is called a maximal consistent set (MCS for short) if (a) $\Gamma\not\vdash\bot$ , and (b) For every $\alpha\in\mathcal{L}_{T}$ either $\alpha\in\Gamma$ or $\neg\alpha\in\Gamma$ .

Although not all the states in a model validate the same support formulas, we still need to make sure that all the states inside the same preference frame $S_{i}$ do. For that reason, we partition the maximal consistent sets into equivalence classes, containing the same support formulas. We also define a set $\rightsquigarrow_{\varphi}(\Gamma)$ containing all formulas which are supported in a MCS $\Gamma$ by a formula $\varphi$ .

Definition 7.

Given $\Gamma,\Delta\subseteq\mathcal{L}_{T}$ and $\varphi\in\mathcal{L}_{CL}$ we define:

•

$\Gamma^{\rightsquigarrow}:=\{\chi\rightsquigarrow\psi\in\Gamma\}\qquad\qquad\hskip 11.0pt$ (We write $\Gamma\leftrightsquigarrow\Delta$ if $\Gamma^{\rightsquigarrow}=\Delta^{\rightsquigarrow}$ ).
•

$\rightsquigarrow_{\varphi}(\Gamma):=\{\psi:\varphi\rightsquigarrow\psi\in\Gamma\}\qquad$ (We call $\Delta$ $\varphi$ -likely for $\Gamma$ if $\rightsquigarrow_{\varphi}(\Gamma)\subseteq\Delta$ ).

Fact 1.

$\leftrightsquigarrow$ is an equivalence relation on the set of all MCSs. We write $[\Gamma]_{\leftrightsquigarrow}$ for the equivalence class containing $\Gamma$ .

Each equivalence class serves as a basis for a preference frame in our canonical model. The maximal consistent sets, which are $\varphi$ -likely for $\Gamma$ are our candidates for the most likely $\varphi$ states in the preference frame based on the equivalence class $[\Gamma]_{\leftrightsquigarrow}$ , as they contain all formulas supported by $\varphi$ .

Before moving forward, we need a result that will be used repeatedly. It asserts that if $\psi$ is not supported by $\varphi$ in $\Gamma,$ then we can construct a MCS $\Delta$ with the same support formulas as $\Gamma$ , and including the negation of $\psi$ as well as all the propositions supported by $\varphi$ .

Lemma 1.

Given a MCS $\Gamma$ and a propositional formula $\psi$ with $\psi\not\in\rightsquigarrow_{\varphi}(\Gamma)$ , then there exists $\Delta\in[\Gamma]_{\leftrightsquigarrow}$ such that $\{\neg\psi\}\cup\rightsquigarrow_{\varphi}(\Gamma)\subseteq\Delta$ .

Proof.

We show the consistency of the set $A:=\{\neg\psi\}\cup\rightsquigarrow_{\varphi}(\Gamma)\cup\Gamma^{\rightsquigarrow}\cup\{\neg(\chi\rightsquigarrow\gamma):\chi\rightsquigarrow\gamma\not\in\Gamma\}.$ If this holds, we can extend the set to an MCS $\Delta$ which, by construction, is contained in $[\Gamma]_{\leftrightsquigarrow}$ . We prove the consistency of $A$ by contradiction. Assume $A\vdash\bot$ . Hence, we can find

\varphi_{1},...,\varphi_{n}\in\rightsquigarrow_{\varphi}(\Gamma),\pi_{1}\rightsquigarrow\psi_{1},...,\pi_{m}\rightsquigarrow\psi_{m}\in\Gamma^{\rightsquigarrow}

and $\neg(\chi_{1}\rightsquigarrow\gamma_{1}),...,\neg(\chi_{k}\rightsquigarrow\gamma_{k})\in\Gamma$ such that $\alpha\land\varphi_{1}\land...\land\varphi_{n}\land\neg\psi\vdash\bot$ with

\alpha:=\pi_{1}\rightsquigarrow\psi_{1}\land...\land\pi_{m}\rightsquigarrow\psi_{m}\land\neg(\chi_{1}\rightsquigarrow\gamma_{1})\land...\land\neg(\chi_{k}\rightsquigarrow\gamma_{k}).

The $\mathbf{CL}$ axioms and the deduction theorem yield $\vdash\alpha\rightarrow((\varphi_{1}\land\dots\land\varphi_{n})\rightarrow\psi).$ From $\mathbf{S5_{F}}$ we get

\vdash\alpha\rightarrow(\neg((\varphi_{1}\land...\land\varphi_{n})\rightarrow\psi)\rightsquigarrow\bot)

and then $\vdash\alpha\rightarrow(\varphi\rightsquigarrow((\varphi_{1}\land...\land\varphi_{n})\rightarrow\psi))$ with the help of Nec. This leads to $\psi\in\rightsquigarrow_{\varphi}(\Gamma)$ because of RW, a contradiction to our assumption. ∎

We define the states and preference relations $\succeq_{\Gamma}$ for our canonical model (the index $\Gamma$ is a representative of an equivalence class of the equivalence relation $\leftrightsquigarrow$ ). The states are $(\Delta,\varphi,i)$ where $\Delta$ is a MCS in the equivalence class $[\Gamma]_{\leftrightsquigarrow}$ , $i\in\{0,1,2\}$ , and $\varphi$ is a propositional formula. $\varphi$ and $i$ are used to pinpoint the maximal $\varphi$ -states according to the relation $\succeq_{\Gamma}$ and to ensure that the maximal elements of $\succeq_{\Gamma}$ coincide with the states satisfying the supported formulas within $\Gamma$ , see Cor. 2.

For a MCS $\Gamma$ we use the following notation:

S_{\Gamma}:=[\Gamma]_{\leftrightsquigarrow}\times\mathcal{L}_{CL}\times\{0,1,2\}\quad\mbox{ and }\quad[\delta]_{\Gamma}:=\{(\Delta,\varphi,i)\in S_{\Gamma}:\delta\in\Delta\}.

Definition 8.

The preference relation $\succeq_{\Gamma}\subseteq S_{\Gamma}\times S_{\Gamma}$ is defined as follows:

$(\Delta,\varphi,i)\succeq_{\Gamma}(\Omega,\psi,j)$ holds if and only if at least one of the following conditions holds:

•

$\Delta$ is $\varphi$ -likely for $\Gamma$ and $\varphi\in\Omega$
•

( $i=1$ and $j=0$ ) or ( $i=2$ and $j=1$ ) or ( $i=0$ and $j=2$ )

After having defined our preference relations we show that the maximal elements in $[\delta]_{\Gamma}$ are $\delta\text{-likely for }\Gamma$ . This is what we are aiming for as we want all the elements in $\mathit{max}([\delta]_{\Gamma})$ to fulfil every formula supported by $\delta$ in $\Gamma$ . Furthermore, if an MCS $\Delta\in S_{\Gamma}$ is $\delta\text{-likely for }\Gamma$ then $(\Delta,\delta,i)$ is a maximal element in $[\delta]_{\Gamma}$ . These results will be the core of our completeness proof since they can be used to show that a support formula is true in a state of $S_{\Gamma}$ if and only if the formula appears in $\Gamma$ . To prove this, we start proving the following technical lemma that establishes a connection between an $(\Delta,\varphi,i)$ appearing in $\mathit{max}([\delta]_{\Gamma})$ and the MCS $\Gamma$ .

Lemma 2.

Given $(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma})$ then:

\begin{array}[]{ll}(a)&\Delta\textit{\ is\ }\varphi\textit{-likely\ for\ }\Gamma;\\ (b)&\neg(\delta\rightarrow\varphi)\rightsquigarrow\bot\in\Gamma.\end{array}

Proof.

We assume $i=0$ . The other cases being similar.

(a) Given $(\Delta,\varphi,0)\in\mathit{max}([\delta]_{\Gamma})$ , we have $(\Delta,\varphi,1)\succeq_{\Gamma}(\Delta,\varphi,0)$ by construction of $\succeq_{\Gamma}$ . This implies $(\Delta,\varphi,0)\succeq_{\Gamma}(\Delta,\varphi,1)$ by maximality. The latter only holds if $\Delta$ is $\varphi$ -likely for $\Gamma$ , and $\varphi\in\Delta$ since no other condition applies.

(b) Assume that there exists a MCS $\Omega\in S_{\Gamma}$ such that $\delta\in\Omega$ but $\varphi\not\in\Omega$ . For $\Omega$ we then have $(\Delta,\varphi,0)\not\succeq_{\Gamma}(\Omega,\delta,1)$ , but $(\Omega,\delta,1)\succeq_{\Gamma}(\Delta,\varphi,0)$ which is a contradiction to $(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma})$ . Hence, we can infer that such an MCS $\Omega\in S_{\Gamma}$ does not exist, which means $[\delta]_{\Gamma}\subseteq[\varphi]_{\Gamma}$ . In other words, every MCS in $S_{\Gamma}$ contains the formula $\delta\rightarrow\varphi$ . More specific each MCS $\Pi$ with $\Pi\in[\Gamma]_{\leftrightsquigarrow}$ contains the formula $\delta\rightarrow\varphi$ , which means $[\Gamma]^{\rightsquigarrow}\cup\{\neg(\delta\rightarrow\varphi)\}$ is inconsistent. This lets us infer $[\Gamma]^{\rightsquigarrow}\vdash\delta\rightarrow\varphi$ , hence we can find finitely many support formulas in $\Gamma^{\rightsquigarrow}$ such that $(\varphi_{1}\rightsquigarrow\psi_{1}\land\dots\land\varphi_{n}\rightsquigarrow\psi_{n})\vdash\delta\rightarrow\varphi$ . By applying the deduction theorem and $\mathbf{S5_{F}}$ we get $\vdash(\varphi_{1}\rightsquigarrow\psi_{1}\land\dots\land\varphi_{n}\rightsquigarrow\psi_{n})\rightarrow(\neg(\delta\rightarrow\varphi)\rightsquigarrow\bot)$ and finally $\neg(\delta\rightarrow\varphi)\rightsquigarrow\bot\in\Gamma$ . ∎

Corollary 1.

Given $(\Delta,\varphi,i)\in S_{\Gamma}$ then

\begin{array}[]{ll}(a)&(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma})\text{\ implies\ }\Delta\text{\ is\ }\delta\text{-likely\ for\ }\Gamma;\\ (b)&\Delta\text{\ being\ }\delta\text{-likely\ for\ }\Gamma\text{\ implies\ }(\Delta,\delta,i)\in\mathit{max}([\delta]_{\Gamma}).\end{array}

Proof.

(a) By $(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma})$ and Lemma 2 we derive $\neg(\delta\rightarrow\varphi)\rightsquigarrow\bot\in\Gamma$ . Using the derivable axiom $\mathbf{K_{\Box}}$ and Necessitation for $\Box$ (see Theorem 2) we get $\neg(\delta\leftrightarrow(\delta\land\varphi))\rightsquigarrow\bot\in\Gamma$ (using the classical tautology $(\delta\rightarrow\varphi)\rightarrow(\delta\leftrightarrow(\delta\land\varphi))$ ). Let us take an arbitrary $\gamma\in\rightsquigarrow_{\delta}(\Gamma)$ , this means $\delta\rightsquigarrow\gamma\in\Gamma$ . Since $\neg(\delta\leftrightarrow(\delta\land\varphi))\rightsquigarrow\bot\in\Delta$ we can apply LL+ to derive $(\delta\land\varphi)\rightsquigarrow\gamma\in\Delta$ . Furthermore, by applying SH, we get $\varphi\rightsquigarrow\delta\rightarrow\gamma\in\Delta$ . By Lemma 2 we know that $\Delta\text{ is }\varphi\text{-likely for }\Gamma$ , which means $\rightsquigarrow_{\varphi}(\Gamma)\subseteq\Delta$ and therefore $\delta\rightarrow\gamma\in\Delta$ . By assumption, we have $\delta\in\Delta$ , which lets us conclude $\gamma\in\Delta$ . Since $\gamma$ was arbitrary we get $\rightsquigarrow_{\delta}(\Gamma)\subseteq\Delta$ .

(b) Since $\Delta$ is $\delta$ -likely for $\Gamma$ by axiom ID we have $\delta\in\rightsquigarrow_{\delta}(\Gamma)\subseteq\Delta$ and therefore $\Delta\in[\delta]_{\Gamma}$ . If we take an arbitrary MCS $\Omega\in S_{\Gamma}$ with $\Omega\in[\delta]_{\Gamma}$ and an arbitrary propositional formula $\pi$ we end up with $(\Delta,\delta,i)\succeq_{\Gamma}(\Omega,\pi,j)$ since the first point in the definition of $\succeq_{\Gamma}$ is fulfilled. ∎

We can finally show that our construction works as intended, namely that every formula $\psi$ supported by a formula $\delta$ according to a MCS $\Gamma$ is contained in all the maximal $\delta$ states in the equivalence set of $\Gamma$ .

Corollary 2.

Given a MCS $\Gamma$ and two propositional formulas $\delta$ and $\psi$ , it holds that

\delta\rightsquigarrow\psi\in\Gamma\text{ if and only if }\;\forall\,(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma}):\psi\in\Delta

Proof.

$(\Rightarrow)$ Given $(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma})$ we can derive that $\Delta\text{ is }\delta\text{-likely for }\Gamma$ via Corollary 1. By assumption we get $\psi\in\rightsquigarrow_{\delta}(\Gamma)\subseteq\Delta$ .

$(\Leftarrow)$ By contraposition. Assume $\psi\not\in\rightsquigarrow_{\delta}(\Gamma)$ . By Lemma 1 we infer that there exists a MCS $\Delta\in[\Gamma]_{\leftrightsquigarrow}$ such that $\{\neg\psi\}\cup\rightsquigarrow_{\delta}(\Gamma)\subseteq\Delta$ . By construction $\Delta$ is $\delta\text{-likely for }\Gamma$ . Corollary 1 gives us $(\Delta,\varphi,i)\in\mathit{max}([\delta]_{\Gamma})$ . Since $\neg\psi\in\Delta$ we get $\psi\not\in\Delta$ by consistency. ∎

Now, we proceed to define the canonical model. To begin, let us fix $I$ as a set consisting of one representative of each equivalent class of $\leftrightsquigarrow$ .

Definition 9 (Canonical model).

Let $\mathcal{M}^{Can}:=\langle S,(S_{\Gamma})_{\Gamma\in I},(\succeq_{\Gamma})_{\Gamma\in I},R,V\rangle$ where:

•

$S:=\bigcup_{\Gamma\in I}S_{\Gamma}$ ;
•

$V(p):=\{(\Delta,\varphi,i)\in S:p\in\Delta\}$ ;
•

$\succeq_{\Gamma}\subseteq S_{\Gamma}\times S_{\Gamma}$ is defined as in Definition 8;
•

$R\subseteq S\times S$ is defined as $(\Delta,\varphi,i)R(\Omega,\psi,j)$ if for all $\alpha\in\mathcal{L}_{T}:~{}(B(\alpha)\in\Delta\Rightarrow\alpha\in\Omega)$ .

We now begin the final steps of our completeness proof. First, we present the truth lemma, which states that a formula is true at a state in the canonical model if and only if the formula is an element of the maximal consistent set of this state. Following this, we demonstrate that $\mathcal{M}^{Can}$ is a Trust model.

Lemma 3 (Truth lemma).

$\mathcal{M}^{Can},(\Delta,\pi,i)\models\alpha$ iff $\alpha\in\Delta$ .

Proof.

Proceeds, as usual, by structural induction on the formula $\alpha$ . See appendix. ∎

Lemma 4.

$\mathcal{M}^{Can}$ in Definition 9 is a Trust model.

Proof.

First, we prove that for each $\Gamma\in I$ $\langle S_{\Gamma},(\succeq_{\Gamma}),V\rangle$ fulfils the limitedness condition. Let $\varphi\in\mathcal{L}_{CL}$ and $\Gamma\in I$ with $[\varphi]_{\Gamma}\not=\emptyset$ . Hence there exists a MCS $\Delta\in[\Gamma]_{\leftrightsquigarrow}$ with $\varphi\in\Delta$ . ST tells us that $\neg(\varphi\rightsquigarrow\bot)\in\Delta$ . This implies $\varphi\rightsquigarrow\bot\not\in\Delta$ and finally $\bot\not\in\rightsquigarrow_{\varphi}(\Gamma)$ . Given that the set $\rightsquigarrow_{\varphi}(\Gamma)$ is closed under consequences because of RW, we can conclude that it is consistent. By Lemma 1, we can now extend $\rightsquigarrow_{\varphi}(\Gamma)$ to a MCS $\Pi\in[\Gamma]_{\leftrightsquigarrow}$ . By construction $\Pi$ is $\varphi\text{-likely for }\Gamma$ . Using part (b) of Corollary 1 we obtain $(\Pi,\varphi,i)\in\mathit{max}([\varphi]_{\Gamma})$ , which makes $\mathit{max}([\varphi]_{\Gamma})$ non-empty. We use Lemma 3 to conclude $||\varphi||_{\Gamma}\not=\emptyset\Rightarrow\mathit{most}(||\varphi||_{\Gamma})\not=\emptyset$ . Since $\varphi$ and $\Gamma$ were arbitrary we are done.

Furthermore, we need to show that the relation $R$ is transitive and serial. We will, from now on, write $\Delta R\Omega$ for $(\Delta,\varphi,i)R(\Omega,\psi,j)$ since $R$ only depends on the sets. Transitivity: Assume $\Delta R\Omega$ and $\Omega R\Pi$ . From $B(\alpha)\in\Delta$ by 4B we derive $B(B(\alpha))\in\Delta$ . By assumption $\Delta R\Omega$ and the construction in Definition 9 $B(\alpha)\in\Omega$ ; the same argument applies for $\Omega R\Pi$ to derive $\alpha\in\Pi$ . Since $\alpha$ was arbitrary, we can conclude $\Delta R\Pi$ . Seriality: Given a MCS $\Delta$ we get $B(\top)\in\Delta$ via the rule of necessitation for $B$ . This implies $B(\bot)\not\in\Delta$ because of the axiom DB and the consistency of $\Delta$ . Now we take a look at the set $A:=\{\alpha:B(\alpha)\in\Delta\}$ . Because of the axiom $\mathbf{KB}$ , we know that $A$ is closed under consequences, and since $\bot\not\in A$ , we also know $A$ to be consistent. We can, therefore, extend it to a maximal consistent set $\Pi$ . By definition $\Delta R\Pi$ , which makes $R$ serial. ∎

With these two lemmas, we are now ready to prove the completeness of SBTrust. This will be done in the usual manner by showing that for every non-derivable formula, there exists a state in our canonical model where it does not hold.

Theorem 5 (Completeness).

Given $\Phi\subseteq\mathcal{L}_{T}$ and $\alpha\in\mathcal{L}_{T}$ it holds that: $\Phi\models\alpha\Rightarrow\Phi\vdash\alpha$ .

Proof.

By contraposition. From $\Phi\not\vdash\alpha$ follows that $\Phi\cup\{\neg\alpha\}$ is consistent and can therefore be extended to a MCS $\Delta$ . By Lemma 3 every formula in $\Delta$ holds in the canonical model in a state of the form $(\Delta,\gamma,i)$ . Hence $\forall\beta\in\Phi:(\Delta,\gamma,i)\models\beta$ and $(\Delta,\gamma,i)\not\models\alpha$ , which gives us $\Phi\not\models\alpha$ by Lemma 4. ∎

We now discuss the complexity results for SBTrust. We split the problem into two parts: $(i)$ we reduce SBTrust by ignoring its support part and focusing on the Boolean and belief parts, and then $(ii)$ we reinstate the support part, completing the proof.

Definition 10 (SBTrust-reduction).

The SBTrust-reduction is obtained by reducing $\mathcal{L}_{T}$ to $\mathcal{L}_{T}^{\prime}$ and transforming a model $\mathcal{M}:=\langle S,\_,\_,R,V\rangle$ into a model $\mathcal{M}^{\prime}:=\langle S,R,V^{\prime}\rangle$ in the following way:

•

$\varphi$ formulas of $\mathcal{L}_{T}$ remain unchanged in $\mathcal{L}_{T}^{\prime}$ ;
•

All $\alpha\in\mathcal{L}_{T}$ of the form $\varphi\rightsquigarrow\varphi$ , are mapped to novel propositional variables taken from a set $\mathit{Prop}^{\prime}$ , where $\mathit{Prop}^{\prime}\bigcap\mathit{Prop}=\emptyset$ ;
•

All the other $\alpha$ formulas are adjusted accordingly;
•

$V^{\prime}$ extends $V$ to also include in its domain $\mathit{Prop}^{\prime}$ , according to the following rule: if $\mathcal{M},s\models\varphi\rightsquigarrow\psi$ and $p^{\prime}$ is the propositional variable corresponding to $\varphi\rightsquigarrow\psi$ , then $s\in V^{\prime}(p^{\prime})$ .

Theorem 6.

The decision problem for SBTrust is PSPACE-complete.

Proof.

First note that the decision problem for a SBTrust-reduction is PSPACE-complete. This follows from the fact that $\mathcal{L}_{T}^{\prime}$ is a set of $\mathbb{KD}4$ formulas and the $\mathcal{M}^{\prime}$ s are serial and transitive relational models. Therefore the results given in [24, 33, 40] hold also for $\mathcal{L}_{T}^{\prime}$ formulas and, in turn, for the SBTrust-reduction. Now, take the conjunction of all support formulas corresponding to the propositional variables of $\mathit{Prop}^{\prime}$ that appear in $\mathcal{L}_{T}^{\prime}$ and are mapped to true. To prove the theorem, we have to show that the problem of deciding those support formulas’ satisfiability is within PSPACE. Refining a result in [18], [45] shows that the satisfiability problem for the (full) logic $\mathbb{F}$ is NP-complete. The result follows by Theorem 3. ∎

Finally, we state the complexity of the model checking problem for SBTrust, i.e., the problem of deciding whether a formula $\alpha$ is satisfied by a state $s\in S$ of a model $\mathcal{M}$ .

Theorem 7.

Given a model $\mathcal{M}:=\langle S,\_,\_,R,V\rangle$ and a formula $\alpha\in\mathcal{L}_{T}$ , let $n$ be the number of states $s\in S$ and $r$ the number of pairs $sRv$ determined by the accessibility relation $R$ . Let $k$ be the number of support formulas, $k^{\prime}$ the number of belief modalities, plus the number of atomic propositions in $\alpha$ , plus the number of connectives in the formula. Then, the complexity of the model checking decision problem is $O(k\cdot n^{2}+(k+k^{\prime})\cdot(n+r))$ .

Proof.

We use the splitting methodology: first considering only the modal part of the formula $\alpha$ , and afterwards the support part. For the first stage, apply a SBTrust-reduction to $\mathcal{M}$ and $\alpha$ . This takes at most $k+k^{\prime}$ -steps (the propositional formulas are left unchanged and each support formula is substituted with a novel propositional formula). After the reduction, what is left is a model checking problem for a modal formula within a pointed Kripke relational model. As is well-known, the complexity of this problem is $O((n+r)\cdot(k+k^{\prime}))$ , see, e.g., [23]. For the second stage, translate back the novel propositional formulas to their respective $k$ support formulas. Take the partition $S_{i}$ which contains the state $s$ in which we must evaluate the formula. To evaluate a support formula $\varphi\rightsquigarrow\psi$ , we need to compute the two sets $\mathit{most}(||\varphi||_{i})$ and $||\psi||_{i}$ . The latter is straightforward (since each state was already labeled during the first stage). The former requires at most $n^{2}$ -steps (we are assuming the worst case in which $||\varphi||_{i}=S_{i}=S$ ): compare each state in $S_{i}$ with all other states in $S_{i}$ , keeping track of the states that are preferred to other states. This must be done for all $k$ support formulas, thus, the complexity of the whole procedure is $O(k\cdot n^{2})$ . This gives us the whole complexity of the model checking problem, which is $O(k\cdot n^{2}+(k+k^{\prime})\cdot(n+r))$ . ∎

6 Conclusions and Future Works

We have introduced SBTrust, a logical framework for reasoning about decision trust based on two pillar concepts, namely belief and support. For the latter, we defined a novel non-monotonic conditional operator, which axiomatizes the flat fragment of the logic $\mathbb{F}$ and is based on preference-semantics.

Because of the generality of the concepts above and the way in which they are combined to formalize trust, SBTrust can integrate elements from the different approaches mentioned in Sect. 1.1 within a unified framework. More precisely, we do not need to indicate specific necessary cognitive conditions for the emergence of trust. Instead, we provide a way to get trust out of the support that exists between different formulas, which can capture the influence of different factors on trust. We also maintain a reference to cognitive features by integrating the belief modality.

Following up the discussion initiated in Example 1, we now illustrate how SBTrust can be used to combine different elements that contribute to establishing trust.

Example 13.

Assume that to trust $\mathit{Good}V_{i}$ , customer $C$ seeks to fulfil three conditions: i) a cognitive-based one; ii) a reputation-based one; iii) a policy-based one. The cognitive-based condition could be captured by the notion of occurrence Trust (denoted by formula $\mathit{OccT}V_{i}$ ) given in [25], which depends on multiple cognitive features of the agents involved such as the goals of $C$ , the ability and intentions of $V_{i}$ , and the effects of the actions of $V_{i}$ on the goals of $C$ . The reputation-based condition could be represented, e.g., by the proposition $\mathit{TopRating}V_{i,j}$ , while the policy-based condition by proposition $\mathit{Auth}V_{i}$ . Then, the formula $T_{\Gamma}(\mathit{GoodV_{i}})$ will indicate that customer $C$ trusts $V_{i}$ as a good vendor for reason $\Gamma$ , where $\Gamma$ stands for $(\mathit{OccT}V_{i}\land\mathit{TopRating}V_{i,j}\land\mathit{Auth}V_{i})$ .

As emphasized by this example, in SBTrust, we have the flexibility to express several different conditions that specific models cannot capture alone. This flexibility comes, however, at the expense of reduced deductive power.

While our framework is primarily designed to capture decision trust, we claim that it could be versatile enough to encompass other notions of trust. In particular, as discussed in [21], many alternative definitions of trust in heterogeneous domains, such as reliability trust [20] in the setting of economy, are based on the use of explicit supportive information. In addition, it is interesting to note that our approach has strong similarities with the approach followed in argumentation-based formalizations of trust [5, 52]. In the future, we intend to explore further potential applications of SBTrust and of the support operator. From the technical point of view, we plan to study the derived operator $T$ in isolation and identify its properties independently of support and belief. Moreover, we intend to extend SBTrust by: $(i)$ allowing nesting of the operators, using beliefs within support statements; $(ii)$ providing a proof calculus, along the line of that in [13], equipped with a prover; $(iii)$ moving towards a quantitative, dynamic, and multi-agent setting.

References

[1] Martín Abadi. Logic in access control (tutorial notes). In Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri, editors, Foundations of Security Analysis and Design V: FOSAD 2007/2008/2009 Tutorial Lectures, pages 145–165. Springer Berlin Heidelberg, 2009.
[2] A. Aldini and M. Tagliaferri. A taxonomy of computational models for trust computing in decision-making procedures. In Audun Jøsang, editor, European Conference on Information Warfare and Security, pages 571–578, 2018.
[3] Alessandro Aldini, Gianluca Curzi, Pierluigi Graziani, and Mirko Tagliaferri. A probabilistic modal logic for context-aware trust based on evidence. International Journal of Approximate Reasoning, 169, 2024.
[4] Alessandro Aldini and Mirko Tagliaferri. Logics to reason formally about trust computation and manipulation. In Andrea Saracino and Paolo Mori, editors, Emerging Technologies for Authorization and Authentication, pages 1–15. Springer, 2020.
[5] Leila Amgoud and Robert Demolombe. An argumentation-based approach for reasoning about trust in information sources. Argument & Computation, 5(2-3):191–215, 2014.
[6] L. Åqvist. Deontic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic: Volume II, pages 605–714. Springer, Dordrecht, 1984.
[7] Donovan Artz and Yolanda Gil. A survey of trust in computer science and the semantic web. Journal of Web Semantics, 5(2):58–71, 2007. Software Engineering and the Semantic Web.
[8] Abdessamad Benlahbib and El Habib Nfaoui. AmazonRep: A reputation system to support Amazon’s customers purchase decision making process based on mining product reviews. In 2020 Fourth International Conference On Intelligent Computing in Data Sciences (ICDS), pages 1–8, 2020.
[9] Bruno Blanchet. Security protocol verification: Symbolic and computational models. In Pierpaolo Degano and Joshua D. Guttman, editors, Principles of Security and Trust, pages 3–29. Springer, 2012.
[10] Alexander Bochman. A logic for causal reasoning. In Georg Gottlob and Toby Walsh, editors, Proceedings of IJCAI-03, pages 141–146. Morgan Kaufmann, 2003.
[11] Diego De Siqueira Braga, Marco Niemann, Bernd Hellingrath, and Fernando Buarque De Lima Neto. Survey on computational trust and reputation models. ACM Comput. Surv., 51(5), nov 2018.
[12] C. Castelfranchi and R. Falcone. Trust Theory: A Socio-Cognitive and Computational Model. John Wiley and Sons, 2010.
[13] Agata Ciabattoni and Dmitry Rozplokhas. Streamlining input/output logics with sequent calculi. In Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isberner, editors, Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, pages 146–155, 2023.
[14] Vincenzo Crupi and Andrea Iacona. The evidential conditional. Erkenntnis, 87:2897–2921, 2022.
[15] Vincenzo Crupi and Andrea Iacona. Three ways of being non-material. Studia Logica, 110:47–93, 2022.
[16] James P. Delgrande and Francis Jeffry Pelletier. A formal analysis of relevance. Erkenntnis (1975-), 49(2):137–173, 1998.
[17] Lidia Fotia, Flávia Delicato, and Giancarlo Fortino. Trust in edge-based internet of things architectures: State of the art and research challenges. ACM Comput. Surv., 55(9), 2023.
[18] Nir Friedman and Joseph Y. Halpern. On the complexity of conditional logics. In Jon Doyle, Erik Sandewall, and Pietro Torasso, editors, Proceedings of KR’94, pages 202–213. Morgan Kaufmann, 1994.
[19] Karen Frost-Arnold. The cognitive attitude of rational trust. Synthese, 191(9):1957–1974, 2014.
[20] Diego Gambetta. Can we trust trust? In Diego Gambetta, editor, Trust: Making and Breaking Cooperative Relations, pages 213–237. Blackwell, 1988.
[21] Diego Gambetta, editor. Trust: Making and Breaking Cooperative Relations. Blackwell, 1988.
[22] Davide Grossi, Wiebe van der Hoek, and Louwe B Kuijer. Reasoning about general preference relations. Artificial Intelligence, 313:103793, 2022.
[23] Joseph Y. Halpern. Reasoning about Knowledge. The MIT Press, 2003.
[24] Joseph Y. Halpern and Yoram Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54(3):319–379, 1992.
[25] Andreas Herzig, Emiliano Lorini, Jomi F. Hübner, and Laurent Vercouter. A logic of trust and reputation. Logic Journal of the IGPL, 18(1):214–244, 12 2009.
[26] Lloyd Humberstone. Philosophical Applications of Modal Logic. College Publications, 2016.
[27] Christian Damsgaard Jensen. The importance of trust in computer security. In Jianying Zhou, Nurit Gal-Oz, Jie Zhang, and Ehud Gudes, editors, Trust Management VIII, pages 1–12. Springer, 2014.
[28] Audun Jøsang. Trust and reputation systems. In Alessandro Aldini and Roberto Gorrieri, editors, Foundations of Security Analysis and Design IV, pages 209–245. Springer, 2007.
[29] Audun Jøsang, Roslan Ismail, and Colin Boyd. A survey of trust and reputation systems for online service provision. Decision Support Systems, 43(2):618–644, 2007. Emerging Issues in Collaborative Commerce.
[30] Sepandar D Kamvar, Mario T Schlosser, and Hector Garcia-Molina. The eigentrust algorithm for reputation management in p2p networks. In Proceedings of the 12th International Conference on World Wide Web, pages 640–651, 2003.
[31] Sarit Kraus, Daniel Lehmann, and Menachem Magidor. Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell., 44(1):167–207, 1990.
[32] Henry Ely Kyburg. Probability and the logic of rational belief. Wesleyan University Press, 1961.
[33] Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6:467–480, 1977.
[34] Christopher Leturc and Grégory Bonnet. A normal modal logic for trust in the sincerity. In International Foundation for Autonomous Agents and Multiagent Systems, AAMAS ’18, page 175–183, 2018.
[35] Fenrong Liu and Emiliano Lorini. Reasoning about belief, evidence and trust in a multi-agent setting. In Bo An, Ana L. C. Bazzan, João Leite, Serena Villata, and Leendert W. N. van der Torre, editors, PRIMA 2017: Principles and Practice of Multi-Agent Systems, volume 10621 of LNCS, pages 71–89. Springer, 2017.
[36] Yining Liu, Keqiu Li, Yingwei Jin, Yong Zhang, and Wenyu Qu. A novel reputation computation model based on subjective logic for mobile ad hoc networks. Future Generation Computer Systems, 27(5):547–554, 2011.
[37] David Makinson and Leendert van der Torre. Input/output logics. J. of Philosophical Logic, 29(4):383–408, 2000.
[38] Stephen Marsh. Formalising Trust as a Computational Concept. University of Stirling, 1994.
[39] D. Harrison McKnight, Norman L. Chervany, and Hubert Horatio Humphrey. The meanings of trust. In University of Minnesota MIS Research Center Working Paper series, 2000.
[40] Linh Anh Nguyen. On the complexity of fragments of modal logics. In Advances in Modal Logic, 2004.
[41] Xavier Parent. Completeness of Åqvist’s systems E and F. The Review of Symbolic Logic, 8(1):164–177, 2015.
[42] I. Pinyol, J. Sabater-Mir, P. Dellunde, and M. Paolucci. Reputation-based decisions for logic-based cognitive agents. Autonomous Agents and Multi-Agent Systems, 24:175–216, 2012.
[43] David Poole. What the lottery paradox tells us about default reasoning. In Ronald J. Brachman, Hector J. Levesque, and Raymond Reiter, editors, Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR’89). Toronto, Canada, May 15-18 1989, pages 333–340. Morgan Kaufmann, 1989.
[44] G. Primiero. A logic of negative trust. Journal of Applied Non-Classical Logics, 30(3):193–222, 2020.
[45] Dmitry Rozplokhas. LEGO-like small-model constructions for Åqvist’s logics. Proceedings of AIML 2024, 2024.
[46] K. E. Seamons, M. Winslett, L. Yu, R. Jarvis, A. Hess, J. Jacobson, B. Smith, and T. Yu. Negotiating trust on the web. IEEE Internet Computing, 6(06):30–37, nov 2002.
[47] Yoav Shoham. A semantical approach to non-monotonic logics. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987), pages 275–279. IEEE Computer Society Press, 1987.
[48] Yoav Shoham. Reasoning about Change. The MIT Press, 1988.
[49] Anthony Smith. What Amazon key teaches us about trust in customer relationships. Forbes., November, 2017.
[50] Marzieh Soleimani. Buyers’ trust and mistrust in e-commerce platforms: a synthesizing literature review. Inf. Syst. E-bus. Manag., 20(1):57–78, March 2022.
[51] Mirko Tagliaferri and Alessandro Aldini. From belief to trust: A quantitative framework based on modal logic. Journal of Logic and Computation, 32(6):1017–1047, 03 2022.
[52] Serena Villata, Guido Boella, Dov M. Gabbay, and Leendert van der Torre. A socio-cognitive model of trust using argumentation theory. International Journal of Approximate Reasoning, 54(4):541–559, 2013. Eleventh European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2011).

Appendix A Technical appendix: proofs of results

Theorem 1.

The rules RW and LLE, as well as the axioms AND, CUT, and OR are derivable in the system for $\rightsquigarrow$ .

Trivial for RW and LLE.

Axiom AND:

\begin{array}[]{llr}(1)&(\psi\land\chi)\rightarrow(\psi\land\chi)&(\mathbf{CL})\\ (2)&((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\chi))\rightarrow(\varphi\rightsquigarrow(\psi\land\chi))&(\mathbf{RCK})\\ \end{array}

Axiom CUT:

\begin{array}[]{llr}(1)&(\varphi\rightsquigarrow\psi)\land((\varphi\land\psi)\rightsquigarrow\chi)&\textit{Hyp.}\\ (2)&(\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow(\psi\rightarrow\chi))&(\textbf{SH})\\ (3)&(\psi\land(\psi\rightarrow\chi))\rightarrow\chi&(\mathbf{CL})\\ (4)&\varphi\rightsquigarrow\chi&(\mathbf{RCK})+(2\land 3)\end{array}

Axiom OR:

Starting from $(\varphi\land(\varphi\lor\chi))\mbox{$\leftrightarrow$}\varphi$ (CL) and applying LLE we get $(\varphi\rightsquigarrow\psi)\mbox{$\leftrightarrow$}((\varphi\land(\varphi\lor\chi))\rightsquigarrow\psi$ ); similarly, we can get also $(\chi\rightsquigarrow\psi)\mbox{$\leftrightarrow$}((\chi\land(\chi\lor\varphi))\rightsquigarrow\psi$ ). Now, let us assume by hypothesis $(\varphi\rightsquigarrow\psi)\land(\chi\rightsquigarrow\psi)$ :

\begin{array}[]{llr}(1)&(\varphi\lor\chi)\rightsquigarrow(\varphi\rightarrow\psi)&\textit{Hyp.}+(\mathbf{SH})\\ (2)&(\varphi\lor\chi)\rightsquigarrow(\chi\rightarrow\psi)&\textit{Hyp.}+(\mathbf{SH})\\ (3)&((\varphi\rightarrow\psi)\land(\chi\rightarrow\psi))\rightarrow((\varphi\lor\chi)\rightarrow\psi)&(\mathbf{CL})\\ (4)&(\varphi\lor\chi)\rightsquigarrow((\varphi\lor\chi)\rightarrow\psi)&(\mathbf{RCK})+(1\land 2)\\ (5)&(\varphi\lor\chi)\rightsquigarrow((\varphi\lor\chi)\land((\varphi\lor\chi)\rightarrow\psi))&(\mathbf{ID})+(\mathbf{AND})\\ (6)&(\varphi\lor\chi)\rightsquigarrow\psi&(\mathbf{RW})\\ \end{array}

∎

Remark 2.

We show that CM in conjunction with CUT and the rule RW permits to derive REC:

$((\varphi\rightsquigarrow\psi)\land(\psi\rightsquigarrow\varphi))\rightarrow((\varphi\rightsquigarrow\chi)\leftrightarrow(\psi\rightsquigarrow\chi))$

\begin{array}[]{llr}(1)&((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\chi))\rightarrow((\varphi\land\psi)\rightsquigarrow\chi)&(\mathbf{CM})\\ (2)&((\psi\rightsquigarrow\varphi)\land((\varphi\land\psi)\rightsquigarrow\chi))\rightarrow(\psi\rightsquigarrow\chi)&(\mathbf{CUT})\\ (3)&((\varphi\rightsquigarrow\psi)\land(\psi\rightsquigarrow\varphi)\land(\varphi\rightsquigarrow\chi))\rightarrow(\psi\rightsquigarrow\chi)&(1\land 2)\\ \end{array}

$(3)$ is equivalent to $((\varphi\rightsquigarrow\psi)\land(\psi\rightsquigarrow\varphi))\rightarrow((\varphi\rightsquigarrow\chi)\rightarrow(\psi\rightsquigarrow\chi))$ . By again using CM and CUT we can also derive $((\varphi\rightsquigarrow\psi)\land(\psi\rightsquigarrow\varphi))\rightarrow((\psi\rightsquigarrow\chi)\rightarrow(\varphi\rightsquigarrow\chi))$ which in total gives as REC.

∎

Theorem 2.

All axioms and rules of $\mathbb{F}$ – but $\mathbf{5}$ and $\mathbf{Abs}$ – are derivable in the axiomatization for $\rightsquigarrow$ .

The claim for axioms $\mathbf{T}$ , $\mathbf{Ext}$ , $\mathbf{ID}$ , and $\mathbf{SH}$ directly follows from the translation. For the remaining axioms: The translation of axiom D^∗ in terms of $\rightsquigarrow$ is $\neg(\varphi\rightsquigarrow\bot)\to\neg((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\neg\psi))$ . Its contraposition $((\varphi\rightsquigarrow\psi)\land(\varphi\rightsquigarrow\neg\psi))\rightarrow(\varphi\rightsquigarrow\bot)$ is an instance of AND.

Case $\mathbf{K_{\Box}}$ :

\begin{array}[]{llr}(1)&(\neg(\varphi\rightarrow\psi)\rightsquigarrow\bot)\rightarrow(\varphi\rightarrow\psi)&(\mathbf{ST})\\ (2)&(\neg\varphi\rightsquigarrow\bot)\rightarrow\varphi&(\mathbf{ST})\\ (3)&((\neg(\varphi\rightarrow\psi)\rightsquigarrow\bot)\land(\neg\varphi\rightsquigarrow\bot))\rightarrow\psi&(\mathbf{CL})+(1\land 2)\\ (4)&((\neg(\varphi\rightarrow\psi)\rightsquigarrow\bot)\land(\neg\varphi\rightsquigarrow\bot))\rightarrow(\neg\psi\rightsquigarrow\bot)&(\mathbf{S5_{F}})\\ (5)&(\neg(\varphi\rightarrow\psi)\rightsquigarrow\bot)\rightarrow((\neg\varphi\rightsquigarrow\bot)\rightarrow(\neg\psi\rightsquigarrow\bot))&(\mathbf{CL})\end{array}

Case COK:

\begin{array}[]{llr}(1)&((\varphi\rightsquigarrow(\psi\rightarrow\chi))\land(\varphi\rightsquigarrow\psi))\rightarrow(\varphi\rightsquigarrow((\psi\rightarrow\chi)\land\psi))&(\mathbf{AND})\\ (2)&((\varphi\rightsquigarrow(\psi\rightarrow\chi))\land(\varphi\rightsquigarrow\psi))\rightarrow(\varphi\rightsquigarrow\chi))&(\mathbf{RW})\\ (3)&(\varphi\rightsquigarrow(\psi\rightarrow\chi))\rightarrow((\varphi\rightsquigarrow\psi)\rightarrow(\varphi\rightsquigarrow\chi))&(\mathbf{CL})\end{array}

Case Nec:

\begin{array}[]{llr}(1)&(\neg\varphi\rightsquigarrow\bot)\rightarrow(\varphi\lor\neg\psi)&(\mathbf{ST})+(\mathbf{CL})\\ (2)&(\neg\varphi\rightsquigarrow\bot)\rightarrow((\neg\varphi\land\psi)\rightsquigarrow\bot)&(\mathbf{S5_{F}})+(\mathbf{LL+})\\ (3)&(\neg\varphi\rightsquigarrow\bot)\rightarrow(\psi\rightsquigarrow\varphi)&(\mathbf{SH})+(\mathbf{CL})\end{array}

Case Necessitation for $\Box$ , if we assume that the formula $\varphi$ is provable, then we can derive $\neg\varphi\rightsquigarrow\bot$ via the following:

\begin{array}[]{llr}(1)&\neg\varphi\rightarrow\bot&\textit{Hyp.}+(\mathbf{CL})\\ (2)&(\neg\varphi\rightsquigarrow\neg\varphi)\rightarrow(\neg\varphi\rightsquigarrow\bot)&(\mathbf{RCK})\\ (3)&\neg\varphi\rightsquigarrow\neg\varphi&(\mathbf{ID})\\ (4)&\neg\varphi\rightsquigarrow\bot&(2\land 3)\\[-5.69054pt] \end{array}

∎

Lemma 3 (Truth lemma).

$\mathcal{M}^{Can},(\Delta,\pi,i)\models\alpha$ iff $\alpha\in\Delta$ .

This proof proceeds by structural induction on the formula $\alpha$ .

If $\alpha\in\mathcal{L}_{CL}$ the claim follows directly from $\mathbf{CL}$ . Assuming the induction hypothesis for every formula in $\mathcal{L}_{CL}$ lets us derive $\forall\varphi\in\mathcal{L}_{CL}$ $||\varphi||_{\Gamma}=[\varphi]_{\Gamma}$ and $\mathit{most}(||\varphi||_{\Gamma})=\mathit{max}([\varphi]_{\Gamma})$ .

Let $\alpha$ be of the form $\varphi\rightsquigarrow\psi$ . We start with the case $\alpha\in\Delta$ . Take $\Gamma$ with $\Delta\in[\Gamma]_{\leftrightsquigarrow}$ . Given an arbitrary $(\Omega,\gamma,j)\in S_{\Gamma}$ with $(\Omega,\gamma,j)\in\mathit{max}(||\varphi||_{\Gamma})$ we get $(\Omega,\gamma,j)\in\mathit{max}([\varphi]_{\Gamma})$ by the induction hypothesis. Because $\psi\in\rightsquigarrow_{\varphi}(\Gamma)$ Corollary 2 implies that $\psi\in\Omega$ . Again by using the induction hypothesis we conclude $(\Omega,\gamma,j)\models\psi$ which means $(\Delta,\pi,i)\models\varphi\rightsquigarrow\psi$ .

For the other direction, we assume $\alpha\not\in\Delta$ . In this case, we have to find a maximal $\varphi$ state which does not satisfy $\psi$ . The assumption $\psi\not\in\rightsquigarrow_{\varphi}(\Delta)$ lets us derive $\psi\not\in\rightsquigarrow_{\varphi}(\Gamma)$ . By the use of Corollary 2, we obtain a $(\Pi,\chi,i)\in\mathit{max}([\varphi]_{\Gamma})$ with $\psi\not\in\Pi$ . By induction hypothesis we get $(\Pi,\chi,i)\in\mathit{max}(||\varphi||_{\Gamma})$ and $(\Pi,\chi,i)\models\neg\psi$ . This means $(\Delta,\pi,i)\not\models\varphi\rightsquigarrow\psi$ .

Let $\alpha$ be of the form $B(\varphi)$ . Then both directions of the claim follow directly from the induction hypothesis and the construction of $R$ in Definition 9. ∎