Merging Beliefs and Counterfactuals

1 Introduction

Epistemic logic and the logic of counterfactual conditionals have largely developed independently since the seminal work of Hintikka [Hintikka, 1962] on the logic of knowledge and belief, and of Lewis [Lewis, 1973] and Stalnaker [Stalnaker, 1968] on the logic of counterfactual conditionals. Epistemic logic has been extensively studied in computer science and artificial intelligence (AI) as a framework for modeling agents' uncertainty in distributed and multiagent systems [Meyer and van der Hoek, 1995; Fagin et al., 1995]. By contrast, counterfactuals and their associated logics have recently attracted renewed attention due to their relevance to causal reasoning [Galles and Pearl, 1998; von K¨ugelgen et al., 2023; Aguilera-Ventura et al., 2025; Bochman, 2018] and explainability [Mittelstadt et al., 2019; Mothilal et al., 2020; Sokol and Flach, 2019; Kenny and Keane, 2021], two central topics in AI.

While epistemic logic is primarily concerned with supporting reasoning about agents' beliefs, including first-order beliefs about the environment and higher-order beliefs about other agents' beliefs, the logic of counterfactual conditionals focuses on reasoning about ontic hypothetical necessity and possibility, that is, how the world would/might be if a given condition were satisfied.

The aim of the present work is to merge these two approaches by providing a unified framework for representing and reasoning about agents' beliefs and counterfactuals. This unification is motivated not only by conceptual considerations but also by practical ones. In particular, we seek to enhance the reasoning capabilities of artificial agents. Intelligent agents possess not only beliefs that represent their views of the environment and of other agents' mental states, but also the ability to reason counterfactually. This capacity is crucial for explaining natural events, as well as one's own and others' beliefs, decisions, and actions, and for attributing responsibility to oneself and to others, all of which are especially relevant to machine ethics and human-machine interaction.

At the language level, the integration we propose consists of combining doxastic modalities of the form □i, representing what agent i implicitly believes (i.e., what the agent can deduce from its belief base) with counterfactual conditional modalities in the style of Lewis and Stalnaker, of the form �. To interpret this language, we rely on a computationally grounded semantics, inspired by [Lorini, 2020], in which the accessibility relations over the states of a model are not taken as primitives but are computed from the information contained in the states. In particular, an agent's doxastic accessibility relation, required to model the agent's implicit belief modality, is computed from information about the agent's belief base (i.e., what the agent explicitly believes), whereas the comparative similarity relation between states, needed to interpret the counterfactual conditional modality, is computed from both information about the agents' belief bases and information about the environment.

We show that our framework provides a unified setting for modeling a rich variety of epistemic concepts studied in formal epistemology and for capturing the subtle interplay between beliefs, counterfactuals, and belief change. In particular, we show that our semantics enables belief change operations on belief bases, including forgetting, contraction, revision, and update, to be represented directly as formulas in the language of beliefs and counterfactual conditionals. Furthermore, we show that counterfactual notions of reason, knowledge, and conditional belief can also be naturally expressed within this language. On the computational side, we exploit our semantics to provide a succinct formulation of model checking for the language of beliefs and counterfactual conditionals and establish a PSPACE complexity result.

The paper is organized as follows. In Section 2, we discuss related work. In Section 3, we present our framework, including the semantics and the interpretation of the language of beliefs and counterfactuals. Section 4 presents some formal properties of beliefs, counterfactuals, and their interrelations. In Section 5, we investigate the connection between our framework and the theory of belief change, while in Section 6 we formalize various epistemic concepts. Section 7 addresses model checking and its computational complexity. Proofs are provided in the extended version of this paper available at https://hal.science/hal-05622406.

2 RelatedWork

A natural connection between epistemic states and counterfactuals is provided by the notion of conditional belief. Its logic, as well as its relationship with belief revision, has been widely studied in recent years [van Benthem, 2007; Baltag and Smets, 2006]. At the model-theoretic level, an important difference between counterfactual conditionals, at least from a Lewisian perspective, and conditional belief is that the former relies on a notion of (ontic) comparative similarity between states, whereas the latter relies on a notion of subjective plausibility between states. There are two key differences between these two notions. The first concerns the so-called absoluteness property: unlike the comparative similarity relation, which is state-dependent, the plausibility ordering is state-independent, remaining fixed across all states in the model or, more restrictively, within an agent's epistemic state. The second concerns the so-called centering property: whereas the actual state belongs to the set of states that are closest to itself (and, in the case of strong centering, is its unique element), the actual state is not necessarily included in the set of states that are most plausible according to the agent. These differences give rise to distinct logics, as shown in [Friedman and Halpern, 1994]. In the present paper, we start from a language of counterfactual conditionals interpreted using a notion of comparative similarity and augment it with belief modalities. We show that a plausibility-based notion of conditional belief can be naturally expressed in the resulting language.

A close work to ours is [Holliday, 2015], where the notion of a counterfactual belief (CB) model is introduced. A CB model combines a comparative similarity relation for counterfactual reasoning with a doxastic accessibility relation for belief. In contrast to our computationally grounded semantics, where comparative similarity reflects differences in agents' belief bases, thereby interrelating the counterfactual and epistemic dimensions, the two dimensions in a CB model are treated independently. A further difference is that Holliday employs CB models to interpret a range of epistemic and doxastic modalities, including Nozick's counterfactual notion of knowledge (which we consider in Section 6), without introducing an explicit counterfactual conditional modality. By contrast, we integrate counterfactual conditional modalities with doxastic modalities and use the resulting language to express a variety of doxastic and epistemic concepts.

The framework presented in Section 3 extends the beliefbase approach to epistemic logic introduced in [Lorini, 2020], both at the semantic and at the language level, by incorporating counterfactual conditionals.

3 Logical Framework

In this section, we present our framework. We begin by introducing the semantics and then turn to the language. In our semantics, a state specifies the truth of ontic facts describing the environment, as well as the agents' explicit beliefs, that is, the information stored in their belief bases. From the information associated with a state, we derive an agent's doxastic accessibility relation, which represents the states the agent considers possible, as well as a comparative similarity relation for reasoning about counterfactual situations. We use this semantics to interpret a language of implicit belief and counterfactual conditionals. The implicit belief modality captures what an agent can deduce from its explicit beliefs.

3.1 Semantics

Assume a countably infinite set of atomic propositions P0 = {p, q, . . .} and a finite set of agents A = {1, . . . , n}. We define the language L0 for explicit belief, as follows:

where p ranges over P0 and i ranges over A. The formula △iα reads "agent i has the explicit belief that α".

We define the set of atomic formulas as follows:

The following definition introduces the notion of state.

Definition 1 (State). A state is a finite set of atomic formulas from P. We denote by S the set of states. Elements of S are denoted by S, S′ , . . .

The truth conditions for the formulas of L0 are defined with respect to states, as follows.

Definition 2 (L0-truth conditions). Let S ∈ S. Then,

As the previous definition highlights, the language L0 can seen as a propositional language built from the set of atomic formulas P and a state S is nothing but a propositional valuation for the propositional language L0.

We define the agent i's belief base at a state S, as the set of i's explicit beliefs at S.

Definition 3 (Belief base). Let i ∈ A and S ∈ S. Then,

The following definition introduces an agent's doxastic accessibility relation. It is computed from its belief base.

Definition 4 (Doxastic accessibility relation). Let i ∈ A and S, S′ ∈ S. Then, SRiS′ iff ∀α ∈ Bi(S), S′ |= α.

According to the previous definition, at state S the agent i considers the state S′ possible if S′ satisfies all facts that i explicitly believes at S. The second component of our semantics is the comparative similarity relation between states.

Definition 5 (Comparative similarity relation). Let S, S′ , S′′ ∈ S. State S′ is at least as similar to state S as state S′′ is, denoted by S′′ ⪯sim S S′ , if (S∆S′ ) ⊆ (S∆S′′ ), where ∆ stands for symmetric difference. We write S′′ ≺sim S S′ if S′′ ⪯sim S S′ and S′ ̸⪯sim S S′′ .

According to the previous definition, state S′ is at least as similar to state S as state S′′ is if S′′ differs from S at least as much as S′ differs from S. In other words, the similarity between two states is fully determined by the set of atomic formulas whose truth values are the same in the two states. Note that ⪯sim S is a partial preorder and, moreover, satisfies the following strong centering property:

We conclude this section by defining the notion of model as a state supplemented with a set of states also called context or universe. The latter includes all states that are compatible with the agents' common ground [Stalnaker, 2002].

Definition 6 (Model). A model is a pair (S,U) with S ∈ U ⊆ S. The class of models is denoted by M.

It is possible to specify both a context and a model succinctly by restricting states to be defined from a finite vocabulary, together with an integrity constraint in L0.

Definition 7 (Context and model specification). A context specification is a pair (Γ, α), where Γ is finite set of atomic formulas from P and α ∈ L0 is an integrity constraint.

A model specification is a triple (S, Γ, α), where (Γ, α) is a context specification and S ∈ S(Γ,α), with

The set S(Γ,α) is the context induced by the integrity constraint α and the the finite vocabulary Γ.

3.2 Language

In this section, we introduce a language for implicit belief and counterfactual conditionals on the top of the language L0 defined above. It is noted L and defined, as follows:

where α ranges over L0 and i ranges over Agt. The other Boolean constructions ⊤, ⊥, ∨, → and ↔ are defined from α, ¬ and ∧ in the standard way. The formula □iφ is read "agent i implicitly believes that φ" in the sense that "φ is deducible

from agent i's explicit beliefs". Its dual, ♢iφ def = ¬□i¬φ, is read as "according to agent i, it is possible that φ". The conditional φ � ψ is read "if φ were true, ψ would be true". Its dual φ�ψ def = ¬(φ�¬ψ) is read "if φ were true, ψ

might be true".

Given a formula φ ∈ L, we denote by P(φ) the set of atomic formulas occurring in φ (including nesting occurences under △i). The definition generalizes to a set of formulas X ⊆ L in a straightforward way: P(X) = ⋃φ∈X P(φ).

Formulas in the language L are interpreted relative to a model as follows. (Boolean cases are omitted since they are defined in the usual way.)

Definition 8 (L-truth conditions). Let (S,U) ∈M. Then,

where Closest(φ,S,U) = {S′ ∈ U | (S′ ,U) |= φ and ∄S′′ ∈ U such that (S′′ , U) |= φ and S ′ ≺sim S S′′}.

In the previous definition, Closest(φ,S,U) is the set of φ-states in U that are the closest (or most similar) ones to the state S. We call Closest(φ,S,U) the φ-neighborhood of state S within U. In agreement with Lewis' interpretation of counterfactual conditionals, at model (S,U) it is the case that "if φ were true, ψ would be true" if every state in the φ-neighborhood of state S within U satisfies ψ. The implicit belief modality □i is interpreted through the doxastic relation Ri: the agent i implicitly believes that φ if φ is true at all states in U that agent i considers possible.

For notational convenience we sometimes write S |= φ instead of (S, S) |= φ. Given a formula φ of the language L, we say that φ is valid (denoted |= φ) if (S, U) |= φ for every (S,U) ∈M. The following example illustrates the language L and its semantic interpretation.

Example 1. We consider an example involving two agents, A = {1, 2}, representing two robots in a building. It is common knowledge among the robots that: (i) if the fire alarm rings (al ), then everyone will explicitly believe this, and if someone explicitly believes that the fire alarm rings, then the alarm indeed rings; (ii) if there is a fire in the building, then the building must be evacuated (ev ). Furthermore, each robot explicitly believes that if the fire alarm rings, then there is a fire in the building (fi). We assume that this information resides at the level of the robots' private belief bases and is not common knowledge, since the fire alarm is defective (even though the robot are unaware of this), so the alarm may ring even in the absence of a fire. Finally, robot 2 privately and wrongly believes that robot 1 does not explicitly believe that if the fire alarm rings, then there is a fire in the building. We are in a situation in which there is a fire in the building, the alarm correctly rings and there is need to evacuate the building. Our scenario is represented by the following actual state:

together with the following integrity constraint representing the agents' common ground:

We assume the vocabulary from which the context is built includes all relevant atomic formulas occurring in the state S0 and in the integrity constraint α0. That is, we consider the model specification (S0, Γ0, α0) such that Γ0 = P(S0 ∪ {α0}). It is routine to verify that for every agent i ∈ {1, 2}:

This means that at the actual state each robot can infer from its belief base that the building should be evacuated. Moreover, if the alarm did not ring, the robot would not be able to infer that the building should be evacuated. Finally, if a robot did not believe that the alarm rings, it would not be able to infer that the building should be evacuated. We also have:

This means that robot 2 can deduce from its belief base that robot 1 does not explicitly believe that the alarm ringing implies a fire in the building, and that, if it did believe so, it would infer that the building must be evacuated.

4 Properties

A central property of counterfactuals is the so-called limit closure: if a formula φ is possible, there should exist a closest state to the actual one in which it holds. As the following theorem shows, our semantics satisfies this property.

Theorem 1. Let (S,U) be a model. Then, for any φ ∈ L, if there is S′ ∈ U s.t. (S′ , U) |= φ then Closest(φ,S,U) ̸= ∅.

The following proposition lists some validities that illustrate interesting properties of counterfactuals and beliefs, as well as their interaction.

Theorem 2. Let φ, ψ ∈ L, α ∈ L0 and p ∈ P0. We have the following validities:

Validity (2), together with property (3), constitutes the two fundamental principles of the normal modal logic K for the implicit belief modality. Validity (4) captures the interaction between explicit and implicit belief: explicitly believing α entails implicitly believing α.

Validities (5), (6), and (7) are standard properties of counterfactual conditionals. In particular, validity (5) expresses the reflexivity property: all closest φ-states to the actual state must satisfy φ. This follows directly from the semantic interpretation of counterfactuals provided in Definition 8.

Validity (6) corresponds to the so-called strong centering property, namely property (1) in Section 3.1. Finally, validity (7) follows from the fact that the relation ⪯sim S is a partial preorder.

The validities (8), (9), (10), and (11) illustrate the interaction between counterfactual conditionals, propositional atoms, and agents' explicit beliefs. Specifically, they show that the comparative similarity used to interpret counterfactual conditionals (Definition 5) depends entirely on information about atomic propositions and agents' explicit beliefs at the state level. They capture a form of monotonicity under the accumulation of true atomic formulas and their negations. Note that the following formula is not valid:

If ⪯sim S were a total preorder, then the earlier formula (12) would be valid. This formula is an axiom of Lewis' V-logics and corresponds to several well-known axioms and postulates in other areas, e.g., the final postulate in AGM theory [Alchourr´on et al., 1985] and rational monotonicity (RM) in non-monotonic reasoning [Kraus et al., 1990]. Since ⪯sim S is not total, RM does not hold in our setting.

5 Belief Change Operations

In our framework, we can capture the subtle interplay between counterfactual conditionals and beliefs, on the one hand, and belief change, on the other. Specifically, we can express standard implementations of belief change operations, including forgetting, contraction, revision, and update, by combining counterfactual conditionals and belief modalities of the language L in various ways.

We focus on the belief base approach to belief change, where a belief base is represented as a finite set of formulas representing an agent's explicit beliefs, and the set of the agent's implicit beliefs is given by its classical deductive closure, denoted by the operator Cn ( · ) [Hansson, 1999]. In our framework, we can work with the formulas from L0, thereby accomodating higher-order explicit beliefs as well. The notions of forgetting, contraction, and revision can be defined in this setting in different ways. We start with the simplest notion of forgetting. 1

Definition 9 (Forgetting). Let X ⊆ L0 and α ∈ L0. The deductive closure of X after forgetting α is defined as:

As the following theorem highlights, forgetting is expressible in the language L, assuming that the model includes all states. (We remind that S |= φ stands for (S, S) |= φ). Specifically, α2 is in the deductive closure of an agent's belief base after forgetting α1 if and only if, if the agent did not explicitly believe α1, it would be able to infer α2.

1 Here, forgetting is understood as the removal of a formula from the belief base [Lorini, 2020], rather than as contraction of the vocabulary [Lin and Reiter, 1994; Delgrande and Wang, 2015].

Belief contraction is a more involved operation, which requires that a formula is not only removed from the belief base, but also cannot be deduced from it. At its core is the following notion of an α-remainder, borrowed from formal models of theory change [Alchourr´on et al., 1985] and belief base change [Hansson, 1993].

Definition 10 (α-remainder). Let X ⊆ L0, α ∈ L0 and X′ ⊆ X. We say that X′ is a α-remainder of X if α ̸∈ Cn(X ′ ), and for all X′′ ⊆ X, if X′ ⊂ X′′ then α ∈ Cn(X′′ ). We denote by X⊥α the set of all α-remainders of X.

According to the previous definition, an α-remainder of a set of L0-formulas X is a maximal subset of X from which α is not deducible. One standard definition for contraction, defined via α-remainders, is full meet base contraction (also known as simple base contraction) [Ginsberg, 1986].

Definition 11 (Full meet base contraction). Let X ⊆ L0 and α ∈ L0. The full meet contraction of X by α is defined as:

Full meet contraction can be expressed in a similar way to forgetting through a counterfactual, this time with the antecedent involving the implicit belief modality rather than the explicit belief one.

Full meet base revision (also known as simple base revision [Nebel, 1989]) is then defined via the well-known Levi identity [Levi, 1977]. This is equivalent to the definitions in [Fagin et al., 1983; Ginsberg, 1986].

Definition 12 (Full meet revision). Let X ⊆ L0 and α ∈ L0. The full meet revision of X by α is defined as:

As the following theorem highlights, α2 is in the deductive closure of an agent's belief base after full meet revision with α1 if and only if, if the agent explicitly believed α1 without falling into a contradiction, it would be able to infer α2.

Another important notion in the theory of belief change is belief update. It is fundamentally different from belief revision in that it is intended to reflect changes in a dynamic world, rather than accommodating new information about a static one. The standard approach to belief update, due to Katsuno and Mendelzon [Katsuno and Mendelzon, 1991], uses a different representation of an agent's beliefs, namely Winslett's Possible Models Approach [Winslett, 1988], which represents beliefs as the set of models considered possible by the agent (in our case, a subset of states from S). Updating by the fact α replaces each state S with the set of states satisfying α that are closest to S, using symmetric difference as the distance measure.

Definition 13 (Katsuno-Mendelzon update). Let X ⊆ L0 and α ∈ L0. Moreover, let S(X) = {S ∈ S | ∀α′ ∈ X, S |= α′ } and S(α) = {S ∈ S | S |= α}. The set of possible states after updating the base X with α is defined as:

The set of deducible formulas after updating X with α is:

Since our framework is based on the same notion of distance, the fact that α2 is in the deductive closure of an agent's belief base after its update with α1 can be represented as the agent's implicit belief that, if α1 were true, α2 would be true.

6 Epistemic Concepts

In this section, we highlight the expressive power of the language L and the semantics under which it is interpreted by using it to define a range of epistemic concepts that are widely studied in epistemology. A novel and interesting aspect of our approach, from the standpoint of expressiveness, is that it naturally captures counterfactual relations, including counterfactual dependence, both between the environment and the agents' epistemic states and among the agents' epistemic states themselves.

We start our conceptual analysis by the defining the classical notion of counterfactual dependence between two facts:

According to the previous definition, ψ counterfactually depends on φ, denoted by Dep(ψ, φ), if both formulas are true and, moreover, if φ were false, then ψ would be false as well.

Counterfactual dependence allows us to define two counterfactual notions of epistemic reason: explicit counterfactual reasons and implicit counterfactual reasons. These two notions are based on two assumptions: (i) an agent's reason for believing a certain fact is mental (or internal to the agent) insofar as it consists in another belief of the agent that supports the first belief, and (ii) the support relation between a belief and the reason on which that belief is based is counterfactual in nature. In epistemology, this relation is known as the basing relation. Different theories analyze it in different ways: causally, counterfactually, dispositionally, or doxastically (see [Carter and Bondy, 2019; Korcz, 2024] for a general overview of competing theories of the basing relation). Following the taxonomy of epistemic reasons proposed in [Sylvan, 2016a; 2016b], we adopt a mentalist (internalist) view of epistemic reasons and a counterfactual interpretation of the basing relation. 2

2 Another important distinction in the theory of epistemic reasons is that between normative reasons (i.e., reasons why an agent ought to believe something) and operative reasons (i.e., reasons why an agent holds a belief) [Sylvan, 2016b]. We remain agnostic about this distinction, since in the case of logic-based artificial agents, which are our focus, the normative and descriptive views coincide: the beliefs an agent ought to have (by applying the normative principles of deductive rationality) coincide with the beliefs the agent holds.

An explicit counterfactual reason is an agent's explicit belief on which one of its implicit beliefs counterfactually depends. That is, the agent explicitly believes α, and can deduce φ from its explicit beliefs, but it would not be able to deduce φ if it did not explicitly believe α. In this sense, explicitly believing α is a necessary condition for the agent to infer that φ is true. In formal terms:

where EReasi(α, ψ) means that the explicitly belief that α is an explicit counterfactual reason for agent i to deduce ψ.

To define an implicit counterfactual reason, we simply replace an explicit belief with an implicit one:

where IReasi(φ,ψ) means that the implicit belief that φ is an implicit counterfactual reason for agent i to deduce ψ. The difference between an explicit and an implicit reason is that, in the former, what the agent can deduce counterfactually depends on its explicit beliefs, whereas in the latter, it depends on something else the agent can deduce. We now return to our example to illustrate the previous definitions.

Example 2 (cont.). The following holds:

This means that, for each robot, the ringing of the alarm provides an explicit reason to conclude that the building must be evacuated, whereas the fact that there is a fire in the building provides an implicit reason for reaching the same conclusion.

As the following theorem shows, under the conditions that the model includes all states and beliefs are about formulas of the language L0, the existence of an explicit counterfactual reason coincides with the fact that the agent would no longer be able to deduce the supported proposition if it were to forget the reason. Thus, under these conditions, counterfactual dependence of the supported belief on its explicit reason can be characterized in purely internal terms, namely, only in terms of operations on the agent's belief base. 3

Nozick's counterfactual definition of knowledge [Nozick, 1981] emphasizes that, for a true belief to count as knowledge, there must be a counterfactual dependence between the true proposition and the agent's belief in it. That is:

Here Kiφ denotes that agent i knows that φ, according to Nozick's counterfactual theory of knowledge. 4

3 The idea that the basing relation should be internal to the agent is discussed in [Korcz, 2000] as a solution to deviant causal chains and to cases where one belief causes another accidentally, rather than through inference, as described in [Audi, 1986; Plantinga, 1993].

4 Nozick includes a second condition in his definition, namely that if φ were true, the agent would believe φ, that is, φ �□iφ. In our framework, this condition is redundant since, by the strong centering property satisfied by our counterfactual conditionals, it is implied by φ ∧ □iφ, which is part of the definition of Kiφ. He includes this second condition as he presupposes weak centering.

The condition ¬φ � ¬□iφ in the definition of Kiφ is known as the sensitivity condition: agent i's belief that φ is sensitive to the truth of φ. This condition ensures that the agent does not hold a true belief in φ merely by accident.

Example 3 (cont.). We have:

Thus, we have: (S0, S(Γ0,α0)) |= ¬K1ev ∧ K1△2al .

This means that, on the one hand, robot 1 holds a true belief that the building should be evacuated, but this belief does not amount to knowledge because the sensitivity condition is not satisfied. In this sense, robot 1's true belief is accidental. On the other hand, robot 1 knows that robot 2 explicitly believes that the alarm is ringing, since it believes this correctly and, moreover, it would not hold this belief if robot 2 did not explicitly believe that the alarm is ringing.

The last concept we consider in this section is conditional belief, where an agent believes that ψ conditional on φ, denoted by Bi(ψ | φ), means that if the agent believed φ, it would deduce that ψ holds. As emphasized in Section 2, this concept has been widely employed in epistemic logic and formal epistemology [van Benthem, 2007; Baltag and Smets, 2006; Spohn, 2013]. While following the Lewisian tradition a counterfactual conditional is interpreted through a notion of comparative similarity, the interpretation of a conditional belief relies on a plausibility ordering over possible states. What we are going to show is that in our framework conditional belief can be reduced to a combination of implicit belief and counterfactual conditional, once an appropriate notion of plausibility is provided.

Following [Lorini, 2025, Def. 7] we compute an agent i's plausibility ordering over states from its belief base.

Definition 14 (Plausibility ordering). Let i ∈ Agt and S, S′ , S′′ ∈ S. Then, S′′ ⪯plaus i,S S′ iff Sati(S, S′′ ) ⊆ Sati(S, S′ ), where Sati(S, S′ ) = {α ∈ Bi(S) : S′ |= α}. We write S′′ ≺plaus i,S S′ if S′′ ⪯plaus i,S S′ and S′ ̸⪯plaus i,S S′′ .

The fact S′′ ⪯plaus i,S S′ should be interpreted as "at state S agent i considers state S′ at least as plausible as state S′′ ". According to the previous definition, this means that all explicit beliefs of agent i at state S that are satisfied by state S′′ are also satisfied by state S′ . Clearly, the relation ⪯plaus i,S thus defined is a partial preorder. However, unlike the comparative similarity relation ⪯sim S , it does not satisfy either the strong or the weak centering property, that is, the analogue of property (1) from Section 3.1, nor its weak variant in which strict ordering is replaced by weak ordering.

Let us define the dyadic conditional belief modality as the following abbreviation using counterfacual conditional:

According to the previous definition, a conditional belief coincides with a belief about material implication in all closest states to the actual one at which the condition is considered possible by the agent.

As the following theorem highlights, when the model includes all states, the previous abbreviation captures the standard notion of conditional belief as defined in epistemic logic, according to which believing that ψ conditional on φ means that ψ is true at all most plausible states satisfying the condition φ.

Theorem 8. Let S ∈ S. Then

where Best(i,φ,S) = {S ′ ∈ S: S′ |= φ and ∄S′′ ∈ S s.t. S′ ≺plaus i,S S′′ and S′′ |= φ}.

7 Model Checking

In Definition 7 we introduced the notion of a model specification. We use this notion to formulate the following succinct model checking problem.

Succinct Model Checking Problem

input: model specification (S, Γ, α), φ ∈ L;

output: true if (S, S(Γ,α)) |= φ; false otherwise.

In this section, we study the computational complexity of this problem and study its connection with model checking w.r.t. the universal context S.

Succinct model checking for (S, Γ, α) and φ can be done directly by definition, in polynomial space w.r.t. the size of the input (a detailed algorithm is provided in the supplementary material): (i) if φ is an atom, check φ ∈ S; (ii) if φ has a Boolean connective at the top, recursively check its immediate subformula(s); (iii) if φ = □iφ′ , check that (S′ , S(Γ,α)) |= φ′ for every subset S′ of Γ satisfying all formulas in {α} ∪ {α′ : △iα′ ∈ S}; (iv) if φ = φ1 � φ2, check that for every subset S′ of Γ, either S′ ̸|= α or (S′ , S(Γ,α)) |= φ2, or (S′ , S(Γ,α)) ̸|= φ1, or there exists a subset S′′ ⊆ Γ with (S′′ , S(Γ,α)) |= φ1 and S∆S′′ ⊂ S∆S′ . Although (iii)-(iv) also perform model checking on formulas in {α}∪{α′ : △iα′ ∈ S} that are not subformulas of φ, these are all in L0 and require only linear time for model checking. Apart from these formulas, the recursion depth is bounded by the size of φ, so the procedure uses polynomial space, resulting in a PSPACE upper bound. A matching lower bound follows from the known reduction of TQBF to model checking of similarity-based counterfactuals [Aguilera-Ventura et al., 2025].

Theorem 9. Succinct model checking is PSPACE-complete.

Model checking w.r.t. the universal context S is trickier. While in standard classical and modal logics the vocabulary can always be restricted to the atoms occurring in the input formula, this does not hold in our framework, since additional atoms of the form△iα may impose additional constraints on occurring atoms, changing the satisfiability of the subformulas in the accessible states. For example, for φ = □i¬□ip, (∅, S(Γ,⊤)) |= φ for Γ = {p}, since ∅RiS and S Ri ∅ for all S ∈ S(Γ,⊤); however, ∅ |= φ because □ip is satisfied, e.g., in the state {△ip}. Thus, in the general case, model checking w.r.t. the universal context requires considering non-trivial extensions of the set of atoms occurring in the input, and we conjecture that this problem belongs to a higher complexity class than the succinct model checking problem defined above. At the same time, we can isolate a fragment of the language that avoids such problematic instances but still contains many interesting formulas (including representations in Section 5). For this, we need to forbid changes of polarity in modal subformulas (such as the occurrence of a modality with existential polarity inside a modality with universal polarity, as in the example above). More precisely, we define a two-layered grammar of formulas in normal form with the connectives ∧ and ∨ and without negations. The first layer L↓ is given by the following grammar, allowing only universal modalities and only formulas from L0 in the antecedent of the counterfactual:

where α ranges over L0 and i ranges over A. The second layer L↑ is given by the following grammar, allowing only formulas from L↓ under the □i modality and the negation of formulas fromL↓ in the antecedent of the counterfactual:

where α ranges over L0, i ranges over A, and φ↓ ranges over L↓. Thus, L↑ allows epistemic modalities in the antecedent of a counterfactual, but only with existential polarity and only if no other epistemic modalities occur above. Notice that all the representation theorems in Section 5 comply with the fragment L↑ (as (¬□i⊥∧△iα1) � (□iα2) can be equivalently rewritten as (¬(□i⊥∨¬△iα1)) � (□iα2)). For L↑, model checking w.r.t. the universal context can be reduced to succinct model checking.

Theorem10. S |= φ↑ iff (S, S(Γ,⊤)) |= φ↑ , for φ↑ ∈ L↑ and Γ = S ∪ P(φ↑ ).

8 Conclusion

We have presented a logical framework integrating beliefs and counterfactuals, and demonstrated its flexibility and expressiveness by using it to capture a wide range of belief change operations and epistemic concepts studied in epistemic logic and formal epistemology. On the computational side, we have provided a succinct formulation of model checking in our framework and proved its PSPACEcompleteness. Moreover, we have identified a non-trivial fragment of our language for which model checking can be formulated more generally, without relying on a notion of finite vocabulary.

Future work will be devoted to studying the proof-theoretic aspects of our framework. In particular, we plan to come up with an axiomatization for the set of validities of the language L. We also plan to extend the language L with epistemic group modalities, including common belief and distributed belief. Indeed, we plan to generalize to the collective level our analysis of the interplay between epistemic states and counterfactuals. On the practical side, we plan to come up with an implementation of the model checking algorithm used for proving the PSPACE upper bound, or a variant of it relying on a polysize reduction into TQBF.

Acknowledgements

This work is supported the ANR PRCE project DesiRes (ANR-25-CE23-7498-01) and the European Union's Horizon 2020 research and innovation programme under grant agreement No 101034440.