Asymptotic Conditional Probability in Modal Logic: A Probabilistic Reconstruction of Nonmonotonic Logic

1 Introduction

Asymptotic Probabilities inModal Logic. Asymptotic (or limit) probabilities of classical logic formulas have been investigated in various contexts [Glebskii et al., 1969; Fagin, 1976; Compton, 1988; Kolaitis and Vardi, 1990; Le Bars, 1998]. Halpern and Kapron have analyzed asymptotic probability in modal logic [Halpern and Kapron, 1994], where, instead of relational structures, Kripke structures are considered, and where the size of a structure is measured in terms of the number of its worlds. Among various results, 1 they have shown that every modal formula is either almost surely true or almost surely false in finite Kripke structures. Thus, there is a 0-1 law for modal logic K, analogous to the 0-1 law for function-free first-order logic [Fagin, 1976; Glebskii et al., 1969].

To give a simple example, if p is a propositional letter of a considered finite alphabet A, then the modal formula 2 Mp is almost surely true (w.r.t. modal logic K). In fact, it can be seen that if n→∞, then the cardinality of the set An of Kripke structures for A of size ≤ n satisfying Mp (i.e., where at least one world satisfying p is reachable from Institut f¨ ur Informationssysteme Technische Universit¨ at Wien gottlob@dbai.tuwien.ac.at each world) grows much faster than the cardinality of the set Bn of Kripke structures which do not satisfy Mp, and thus limn→∞ |An|/|Cn| = 1 where Cn is the set of all Kripke structures with n worlds over the considered alphabet.

1 Some of the results of [Halpern and Kapron, 1994] have been corrected in [Le Bars, 2002], but those referred-to in the present paper are perfectly correct in [Halpern and Kapron, 1994].

2 We here use K as the symbol for the necessity (= knowledge) operator and M (≡ ¬K¬) for the possibility operator.

Assigning asymptotic probabilities to modal formulas provides an interesting nonstandard semantics to modal logics and has important connections to philosophy and to artificial intelligence:

PHILOSOPHY: It has been observed [Halpern and Kapron, 1994; Gottlob, 1999] that the modal formulas that are almost surely true in all Kripke models are exactly those formulas which are valid in Carnap's modal logic, exposed in his wellknown foundational treatise Meaning and Necessity [Carnap, 1947]. Carnap argued that precisely these formulas are those to be considered logically true (L-true). The same logic has since be considered by various philosophers and logicians [Gottlob, 1999].

ARTIFICIAL INTELLIGENCE: Various nonmonotonic modal logics have been defined in the literature. Examples are autoepistemic logic [Moore, 1985], nonmonotonic logics K, S4, etc. [Marek and Truszczy´nski, 1993], the logic MBNF [Lifschitz, 1994] and the logic of minimal knowledge S5G [Halpern andMoses, 1985]. In these logics, the modal operator K is interpreted as an epistemic operator of knowledge or of belief. As observed in [Gottlob, 1999], the formulas that can be derived from an empty set of premises in all these logics precisely coincide with those formulas which are almost surely true in all Kripke structures. This set of formulas is furthermore identical to the stable set [Stalnaker, 1993] based on the empty set of formulas, thus, in a sense, to the "absolute" stable set, containing only those formulas that are epistemic consequences of the empty theory, i.e., that can be assumed in the case of total factual ignorance (for a definition of stable sets, see Section 4). We thus retain that in nonmonotonic and epistemic logics, in absence of further knowledge, a modal formula is considered true if and only if this formula is almost surely valid.

Reasoning and Asymptotic Conditional Truth. While almost sure validity provides an appealing probabilistic semantics of truth in the case of total factual ignorance, this does not yet allow us to reason on the basis of premises, which is the the most important goal of all logical formalisms, and, in particular, of nonmonotonic and epistemic logics. In the setting of limit probabilities, the inference ϕ |= ψ of a (possibly modal) formula ψ from a knowledge base (theory) ϕ would most intuitively correspond to the statement that the conditional probability P(ψ | ϕ) is asymptotically equal to 1. Assuming a uniform probability distribution of Kripke structures, this means that for the sets An and Bn of Kripke models of size n satisfying ψ ∧ ϕ and ϕ, respectively, the limit limn→∞ |An|/|Bn| exists and is equal to 1.

There is, in general, no 0-1 law for conditional probabilities in our setting, which immediately follows from previous results (see e.g. [Grove et al., 1996b]) and from the fact that modal logic corresponds to a fragment of functionfree first-order logic. The existence and determination of conditional probabilities in first and higher order logics has been the subject of several studies [Grove et al., 1996b; 1996a]. However, to our best knowledge, conditional probabilities for modal logics have never been studied.

Observe that reasoning via conditional limit probabilities as explained above clearly constitutes a form of nonmonotonic reasoning. For example, if p is a propositional letter, then |=lim Mp but K¬p ̸|=lim Mp, thus, adding a premise may invalidate a consequence (here |=lim denotes inference of almost sure formulas under conditional limit probabilities). The nonmonotonic behaviour of conditional inference has been pointed out in the context of FO and higher order classical logic (see e.g. [Grove et al., 1996b]). We deem the context of modal logic particularly interesting, because most nonmonotonic logics that have been defined are modal logics. It would thus be very interesting to know how the nonmonotonic modal logic obtained from conditional limit probabilities of Kripke structures relates to well-known and well-studied nonmonotonic modal logics.

Nonmonotonic Modal Logics. For every "classical" monotonic system of modal logic S, a nonmonotonic version NM-S is obtained by the following definition: A set E of modal formulas is an NM-S-expansion of a knowledge base ϕ iff E = CnS(ϕ ∪ {¬Kγ|γ ∈ LK(A) - E}), where CnS is the consequence operator according to modal logic S and LK(A) is the underlying modal language, i.e., the set of all possible modal formulas over the alphabet of propositions A3 . In particular, Moore's autoepistemic logic corresponds to NM-KD45. For more background, consult [Marek and Truszczy´nski, 1993].

It was often criticized that the above fixed-point equation is somewhat too liberal, because it allows a theory to have expansions that are not sufficiently "grounded" in the premises and contain positive knowledge that a rational agent should never conclude from the premises. For this reason, ground nonmonotonic modal logics have been defined by restricting the introspection of the agent to non-modal sentences. The notion of groundedness has a rather intuitive motivation: in fact, it corresponds to discarding any reasoning based on epistemic assumptions, which, for example, would enable the agent to conclude that something is true in the world, by assuming to know it. The fixed-point equation defining a SGexpansion of ϕ is: E = CnS(ϕ ∪ {¬Kγ | γ ∈ L(A)-E}), where L(A) denotes the set of all objective (i.e., non-modal)

3 This definition is applicable to a large range of modal logics, but a collapse happens at S5 because NM-S5=S5 [Marek and Truszczy´nski, 1993].

formulas of the underlying propositional language. According to this equation, we can associate a logic SG to each modal logic S. Given ϕ ∈ LK(A), ψ ∈ LK(A), we say that ψ is entailed by ϕ in SG (and write ϕ |=SG ψ) iff ψ belongs to all SG-expansions for ϕ.

Among all ground nonmonotonic logics, the logic S5G (which, unlike NM-S5, is a true nonmonotonic logic) has received considerable attention in the literature and is generally referred to as the logic of minimal knowledge [Halpern and Moses, 1985] (or the logic of maximal ignorance). In fact, independently from its fixed-point characterization, S5G was characterized on a semantic basis, by means of a preference criterion among the models of an agent's knowledge selecting just those models in which objective knowledge (i.e, the set of formulas of type Kϕ such that ϕ ∈ L(A)) is minimal [Halpern and Moses, 1985; Shoham, 1987; Lifschitz, 1994]. As shown in [Shoham, 1987], S5G has a simple, elegant model theory: The S5G models of a theory T are precisely those Kripke structures which are universal (i.e., totally connected) and are maximal set of worlds (w.r.t. set-containment). For details on ground nonmonotonic modal logics and S5G, see [Halpern and Moses, 1985; Lifschitz, 1994; Donini et al., 1997].

Main Problems Studied. The investigations reported in this paper were motivated by the following questions:

1. Given a formula ϕ, which formulas ψ are almost surely true in the Kripke models of ϕ, i.e., how can we characterize the formulas ψ that are true with limit probability one in the Kripke models of ϕ, when the size of these Kripke models grows towards infinity?
2. Given that modal inference under almost sure validity constitutes a form of nonmonotonic reasoning, to which of the nonmonotonic modal logics from the abovementioned plethora of logics does this form of reasoning best correspond?
3. Can we characterize the set of formulas ϕ that guarantee a 0-1 law for the asymptotic probability P(ψ|ϕ) for arbitrary modal formulas ψ?
4. What is the complexity of modal reasoning based on asymptotic conditional probabilities?

For studying these questions, we make a very weak assumption on ϕ, which assures that ϕ does not contradict some principles of knowledge: we assume that ϕ is S5-consistent, i.e., we assume that ϕ is consistent with the axioms of (monotonic) S5, which means that ϕ admits at least one S5-model. This assumption is indeed very weak. It does neither mean that ϕ contains the S5 axioms, or that these axioms should follow from ϕ, nor that ϕ has to be interpreted under S5 Kripke structures only. Our assumption merely requires that formulas such as Kp ∧ K¬p which bluntly contradict some axioms of (monotonic) S5 cannot be deduced from ϕ. If ϕ satisfies this requirement, we say that ϕ is knowledgeconsistent. We make this assumption because knowledgeinconsistent theories are well-known to be inconsistent for all currently known nonmonotonic modal logics anyway, i.e., in each such nonmonotonic logic, a knowledge-inconsistent formula ϕ entails a contradiction and thus all formulas of the modal language LK(A). In particular, with regard to our goal of comparing asymptotic conditional reasoning to nonmonotonic modal logics, there is no point to consider knowledge-inconsistent modal premises. Moreover, we characterize asymptotic conditional reasoning when the premise is a flat modal formula, i.e., a formula without nested occurrences of the modal operator. The flat fragment of a modal logic of knowledge is certainly a very important (if not the most important) syntactically restricted fragment. It consists of the Boolean closure of knowledge bases, i.e., of objective theories under the K operator. In particular, the flat fragment in S5G is extremely powerful and expressive. As shown in [Rosati, 1998], via appropriate translations, this fragment captures the well-known formalisms of default logic and logic programming under the stable model semantics. In the present paper we limit our attention to this flat fragment. However, we think that (by slightly more involved methods) our results carry over to the fully nested fragment (i.e., the fragment with nesting depth greater than 1).

Results. By first answering the second of the above-stated research questions, we show the following main result:

Answer to Question 2: ϕ almost surely entails ψ iff ψ is entailed by ϕ in S5G.

This result gives a fresh probabilistic semantics to the wellknown nonmonotonic modal logic S5G, providing a new justification for S5G based on probabilistic rationality. At the same time, it provides the answers to our questions 1 and 4, too. In fact, as already mentioned, reasoning in S5G has precise characterizations in terms of model-theory and complexity, hence the same characterizations now apply to asymptotic conditional reasoning over Kripke models:

Answer to Question 1: ϕ almost surely entails ψ iff ψ is satisfied by all Kripke models of ϕ that are universal and have a maximal set of worlds.

Answer to Question 4: Deciding whether ϕ almost surely entails ψ is Πp2 -complete. 4

A theory is honest [Halpern and Moses, 1985] iff it has exactly one S5G-model. It has been argued that the epistemic state of a perfectly rational agent is necessarily honest, e.g., it could not be of the form (KT1) ∨ (KT2) where T1 and T2 are theories that contradict each other. Honest premises drastically simplify asymptotic conditional reasoning:

Answer to Question 3: The class of knowledge-consistent premises ϕ that imply a 0-1 law is exactly the class of honest formulas. In other words, the honest formulas are precisely the formulas ϕ such that, for all ψ, the asymptotic probability that ψ holds in the structures in which ϕ is valid is either 0 or 1. Moreover, asymptotic conditional reasoning based on honest theories is only Θp2 -complete.

Due to space limitations, we can only include the sketches of some results in the present version of the paper.

2 Preliminaries

We assume familiarity with modal logics K and S5. We deal with a propositional alphabet A such that either A is finite and fixed, i.e., it is the same for every problem instance, or A is not bounded, but each problem instance comes along with a finite alphabet A as part of the input. We denote by L(A) the set of propositional (or objective) formulas over A, denote by LK(A) the set of modal formulas over A, and denote by LFK (A) the set of flat modal formulas, i.e., the subset of LK(A) of formulas over A satisfying the following abstract syntax:

4Πp2 is the complement of Σp2 =NPNP ; Θp2 is the class of problems solved in PTIME by a logarithmic number of calls to an NP-oracle.

We also use the symbol true to denote the formula a ∨ ¬a, and the symbol false to denote the formula a ∧ ¬a.

We now recall some auxiliary definitions that we will use in the following sections [Marek and Truszczy´nski, 1993; Donini et al., 1997]. Given ϕ ∈ LK(A), we denote by MA(ϕ) the set of modal atoms from ϕ, i.e., the set of subformulas of the form Kψ occurring in ϕ. In the following, we say that an occurrence of a modal atom Kψ in a formula ϕ ∈ LK(A) is strict if it does not lie within the scope of a modal operator.

Given a partition (P,N) of the set MA(ϕ) and a formula ψ ∈ LK(A), we denote by ψ(P,N) the formula obtained from ψ by substituting each strict occurrence in ψ of a modal atom in P with true, and each strict occurrence in ψ of a modal atom in N with false. Notice that, if P ∪N contains MA(ψ), then ψ(P,N) is a propositional formula.

Let ϕ ∈ LK(A) and let (P,N) be a partition of MA(ϕ). We denote by obj ϕ(P, N) the propositional formula obj ϕ(P, N) = ϕ(P, N) ∧ ∧Kψ∈P ψ(P, N).

Given a partition (P,N) of the set MA(ϕ), we say that (P,N) is S5-consistent with ϕ if (P,N) satisfies the following conditions: (1) the propositional formula obj ϕ(P,N) is satisfiable; (2) for each Kψ ∈ N, the propositional formula objϕ(P,N) ∧¬ψ(P,N) is satisfiable. It is immediate to see that there exists a partition of MA(ϕ) S5-consistent with ϕ iff ϕ is knowledge-consistent, i.e., there exists an S5-structure S such that (w, S) |= Kϕ where w is a world of S. Finally, given a structure S = 〈W, R, V 〉 and a world w ∈ W , we say that (P,N) is the partition of MA(ϕ) satisfied by (w, S) if, for each Kψ ∈ MA(ϕ), (w, S) |= Kψ iff Kψ ∈ P .

3 Strong almost-sure conditional validity

In the work of Halpern and Kapron [Halpern and Kapron, 1994], almost sure structure validity is studied by considering all possible Kripke structures equally likely, i.e., uniformly distributed. This amounts to assume that that every propositional variable is true with probability 1/2 in a randomly chosen world. Under such an assumption, the asymptotic probability of ϕ w.r.t. a propositional alphabet A corresponds to the limit limn→∞ |Wϕ n |/|Wn|, where: (i) Wn denotes the set of all n-structures over A, i.e., the structures with n worlds of the form 〈W, R, V 〉, where W = {1, . . . , n}, the accessibility relation R is a binary relation over W, and V is a function mapping each world into a propositional interpretation over A; (ii) Wϕ n denotes the set of all n-structures in which ϕ holds; (iii) |S| represents the cardinality of a set S. Moreover, under the above uniform probability assumption, asymptotic conditional probability of ψ given ϕ corresponds to the limit limn→∞ |W(ϕ∧ψ) n |/|Wϕ n |.

It would be more appealing to consider the notion of strong almost sure validity, where the asymptotic probability of a formula ψ is required to be equal to 1 for every possible probability distribution assigning rational truth probabilities to the propositional variables. It turns out that in the context of [Halpern and Kapron, 1994] both concepts are equivalent, thus all relevant results of [Halpern and Kapron, 1994] extend to strong almost sure validity. In the context of conditional probabilities, these concepts differ, however. In this paper we choose to characterize the notion of strong almost sure conditional validity, which is independent of a particular fixed probability distribution. However, we will use (Section 4) the concept of almost sure conditional validity (i.e., the one corresponding to the uniform distribution of Kripke structures) as a tool for establishing (Section 5) our main result on strong almost sure validity.

More formally, we associate to each propositional atom a ∈ A a rational probability m such that 0 < m < 1, which is interpreted as the probability that the proposition a is true. Such an assignment is part of the input. Assignments giving probability 1 (resp. 0) to a are not considered, since in such cases the proposition a is certainly true (resp. false) and all its occurrences in a formula can be eliminated in a simple way. We assume without loss of generality that m is a finite sum of the negative powers of two. Hence, we say that P is a probability assignment over an alphabet A if P is a function mapping each propositional symbol from A to a rational number m such that there exists a finite binary sequence m1 . . .mp such that m = ∑pi=1 mi 2i .

It is immediate to verify the following relationship between the cardinality of a set of interpetations and the number of different n-structures defined over such interpretations. 5

Lemma 3.1 Let I be a set of propositional interpretations, and let Wn be the set of n-structures defined using the set of interpretations I. Then, |Wn| = |I|n · 2n2 .

Let ϕ, ψ ∈ LK(A), and let P be a probability assignment over A. Then, pnP (ψ|ϕ) denotes the probability that ψ is valid in the n-structures in which ϕ is valid, under the probability assignment P. We are now ready to define almost-sure and strong almost-sure conditional validity.

Definition 3.2 (P-almost-sure validity) Let P be a probability assignment over A. We say that ψ conditioned by ϕ is P-almost-surely valid if limn→∞pnP (ψ|ϕ) = 1, i.e., the asymptotic probability that ψ conditioned by ϕ is valid is 1 under the probability assignment P. Conversely, if limn→∞pnP (ψ|ϕ) < 1, then we say that ψ conditioned by ϕ is not P-almost-surely valid.

Definition 3.3 (strong-almost-sure validity) ψ conditioned by ϕ is strongly almost-surely valid if limn→∞pnP (ψ|ϕ) = 1 for each probability assignment P over A. Conversely, if there exists a probability assignment P over A such that limn→∞pnP (ψ|ϕ) < 1, then we say that ψ conditioned by ϕ is not strongly almost-surely valid.

We denote by SAS(ϕ,A) the set of formulas ψ from LK(A) such that ψ conditioned by ϕ is strongly almost-surely valid.

4 Counting structures

In this section we prove the correspondence between the notion of stable set in nonmonotonic modal logics and strong almost-sure conditional validity with respect to objective formulas, and establish a first correspondence between S5G and strong almost-sure conditional validity in modal logic.

5 We adopt the well-known random worlds method [Grove et al., 1996b; 1996a].

From now on, we denote by h the number of propositional interpretations of A, i.e., h = 2|A| . Moreover, given a formula f ∈ L(A), we denote by hf the number of interpretations of A satisfying f .

We start our analysis by studying the properties of the set of n-structures for f, i.e., the n-structures in which a propositional formula f is valid. First of all, from Lemma 3.1, it follows that the number of n-structures for f is hf · 2n2 .

Then, we recall the definition of stable set of modal formulas. Let f be a satisfiable propositional formula over the propositional alphabet A. The stable set of f in A (denoted by Stable(f,A)) is the unique set of modal formulas T ⊂ LK(A) that satisfies the following conditions: (i) for each ψ ∈ L(A), ψ ∈ T iff f ⊃ ψ is a tautology; (ii) if ψ ∈ T then Kψ ∈ T ; (iii) if ψ ∈ LK(A) - T then ¬Kψ ∈ T ; (iv) T is closed under propositional consequence [Marek and Truszczy´nski, 1993].

Next, we prove the correspondence between formulas strongly almost-surely valid with respect to an objective formula f and the formulas in Stable(f,A). The proof is easily obtained by extending an analogous result in [Halpern and Kapron, 1994].

Lemma 4.1 Let f ∈ L(A) be a satisfiable objective formula. Then, SAS(f, A) = Stable(f, A).

We now introduce two auxiliary lemmas.

Lemma 4.2 Let ϕ be a flat and knowledge-consistent formula, let Wϕ n be the set of n-structures for ϕ and let Dn be the set of n-structures for ϕ in which all worlds satisfy the same partition (P, N) of MA(ϕ) S5-consistent with ϕ. Then, limn→∞ |Dn|/|Wϕ n | = 1.

Proof sketch. The proof is divided in two steps: First, we prove that, if ϕ is a flat and knowledge-consistent formula, limn→∞ |D′n |/|Wϕ n | = 1, where D′n denotes the set of n-structures for ϕ in which no world satisfies an S5-inconsistent partition of MA(ϕ). Then, we concentrate on the set D′n : let D′′n denote the subset of D′n in which two worlds satisfy two different S5-consistent partitions of MA(ϕ) (P1,N1), (P2,N2), let D1n be the subset of D′n in which all worlds satisfy (P1,N1) and let D2n be the subset of D′n in which all worlds satisfy (P2, N2). We prove that either limn→∞ |D′′n |/|D1n | = 0 or limn→∞ |D′′n |/|D2n | = 0.

The following property can be derived by an argument analogous to the proof of Lemma 4.1.

Lemma 4.3 Let ϕ be a flat and knowledge-consistent formula and let (P, N) be a partition of MA(ϕ) consistent with ϕ. Let Wϕ n (P,N) denote the set of n-structures for ϕ in which all worlds satisfy the partition (P,N), and let Dn be the set of n-structures for obj ϕ(P, N)∧µ(N), where µ(N) = ∧Kf∈N ¬Kf. Then, limn→∞ |Dn|/|Wϕ n (P,N)| = 1. Moreover, limn→∞ |Wϕ n (P, N)| = (hobj ϕ (P,N))n · 2n2 .

We now define S5G-preferred partitions of modal atoms.

Definition 4.4 (S5G-preferred partition) Let ϕ ∈ LK(A). A partition (P,N) of MA(ϕ) is S5G-preferred for ϕ if (P,N)

is S5-consistent with ϕ and there exists no other partition (P ′ ,N ′ ) ̸= (P,N) of MA(ϕ) such that (i) (P ′ ,N ′ ) is S5-consistent with ϕ; and (ii) the propositional formula obj ϕ(P,N) ∧¬obj ϕ(P ′ ,N ′ ) is not satisfiable.

It is immediate to verify that S5G-preferred partitions of MA(ϕ) are in one-to-one correspondence with S5G-expansions of ϕ: in particular, each such partition (P,N) identifies the S5G-expansion corresponding to Stable(obj ϕ(P, N ), A).

We are now ready to show a first fundamental step towards the correspondence between S5G and strong almost-sure conditional validity: For each knowledge-consistent modal formula ϕ, to compute (strong) almost sure conditional validity we can safely consider only the set of n-structures in which all worlds satisfy one of the partitions of MA(ϕ) that are S5Gpreferred for ϕ.

Theorem 4.5 Let ϕ be a flat, knowledge-consistent formula, let Wϕ n denote the set of n-structures for ϕ, and let Dn be the union of the sets of n-structures for ϕ in which all worlds satisfy the same partition (P,N) of MA(ϕ), where (P,N) is S5G-preferred for ϕ. Then, limn→∞ |Dn|/|Wϕ n | = 1.

Proof. Let C ′n be the union of the sets of n-structures for obj ϕ(P, N) ∧ µ(N) for each partition (P, N) of MA(ϕ) that is S5-consistent with ϕ. First, by Lemma 4.2 and Lemma 4.3 it follows that limn→∞ |C ′n |/|Wϕ n | = 1. Moreover, let Cn be the union of the sets of n-structures for obj ϕ(P,N) ∧ µ(N) for each partition (P,N) of MA(ϕ) that is S5G-preferred for ϕ: By the same lemmas it follows that limn→∞ |Cn|/|Dn| = 1. Thus, we have to prove that limn→∞ |Cn|/|C ′n | = 1.

Let (P,N) be a partition (P,N) of MA(ϕ) S5G-preferred for ϕ, and consider all the partitions (P ′ , N ′ ) of MA(ϕ) such that objϕ(P,N) is satisfied by all propositional interpretations satisfying objϕ(P ′ ,N ′ ). Let C (P,N) n be the set of nstructures for objϕ(P,N) ∧ µ(N), and let C (P ′ ,N ′ ) n be the union of the set of n-structures for obj ϕ(P ′ ,N ′ ) ∧ µ(N ′ ) for each such partition (P ′ ,N ′ ). Obviously, C (P,N) n ⊆ C (P ′ ,N ′ ) n (since (P,N) is one of such partitions (P ′ ,N ′ )). We now prove that limn→∞ |C(P,N) n | |C(P ′ ,N′ ) n | = 1. Let C ′′ n =

C (P ′ ,N ′ ) n - C (P,N) n . That is, C ′′ n is the set of n-structures for obj ϕ(P ′ ,N ′ ) ∧ µ(N) for each partition (P ′ ,N ′ ) that is S5consistent with ϕ and such that objϕ(P,N) is satisfied by all propositional interpretations satisfying obj ϕ(P ′ ,N ′ ), and there exists at least an interpretation satisfying obj ϕ(P, N) ∧ ¬obj ϕ(P ′ , N ′ ). Now let k be the number of interpretations of A satisfying objϕ(P,N): It is immediate to verify that there can be at most k such different partitions (P ′ ,N ′ ). Moreover, for each such partition (P ′ ,N ′ ), there exists at least a propositional interpretation I that satisfies objϕ(P,N) and does not satisfy obj ϕ(P ′ ,N ′ ). Therefore, from Lemma 4.3

5 Asymptotic conditional probability and S5G

In this section we prove the main result of the paper, which establishes the correspondence between strong almost-sure conditioned validity and entailment in the logic S5G. To this aim, we need some preliminary definitions and properties.

Let A′ be the set of propositional atoms ai such that a ∈ A and 1 ≤ i ≤ m. We define the canonical probability assignment Pc over A′ as follows: Pc(a) = 12 for each a ∈ A′ . Let A be a propositional alphabet and let If be the set of propositional interpretations over A that satisfy f. The canonical probability of a propositional formula f, denoted by cp(f), is defined as cp(f) = |If | 2|A| .

The following auxiliary lemma establishes a sufficient condition over the partitions of MA(ϕ) which implies that limn→∞ pnPc (ψ|ϕ) < 1.

Lemma 5.1 Let ϕ ∈ LFK (A). If there exists a partition (P,N) of MA(ϕ) such that: (1) (P,N) is S5G-preferred for ϕ; (2) for each partition (P ′ , N ′ ) that is S5G-preferred for ϕ, cp(obj ϕ(P, N)) ≥ cp(obj ϕ(P ′ , N ′ )); (3) ψ does not hold in the structures for objϕ(P,N), then lim n→∞ pnPc (ψ|ϕ) < 1.

Let a ∈ A and let P(a) = k where k is a rational number satisfying the definition of probability assignment. Then, we can construct a propositional formula f k (a) defined over an alphabet Ak = {a1 , . . . , amk } (where mk is a number depending on k) such that P(a) = cp(f k (a)). Then, given a probability assignment P over A, we define τP(ϕ) as the formula obtained from ϕ by replacing, for each a ∈ A, each occurrence of a in ϕ with f P(a) (a). Now, in order to prove our main result, we need some auxiliary lemmas.

Lemma 5.2 Let ψ ∈ LK(A), and let f ∈ L(A). Then, ψ ∈ SAS(f,A) iff τP(ψ) ∈ SAS(τP(f),Ak ).

Lemma 5.3 Let ϕ, ψ ∈ LK(A). then, for each partition (P,N) that is S5G-preferred for ϕ, the partition (τP(P), τP(N)) is S5G-preferred for τP(ϕ), while for each partition (τP(P), τP(N)) that is S5G-preferred for τP(ϕ), the partition (P, N) is S5G-preferred for ϕ.

Lemma 5.4 Let ϕ ∈ LK(A). If a partition (P, N) of MA(ϕ) is S5G-preferred for ϕ, then the stable set of obj ϕ(P,N) in A is an S5G-expansion for ϕ. Moreover, if a set T ⊂ LK(A) is an S5G-expansion for ϕ, then there exists a partition (P,N) of MA(ϕ) such that (P,N) is S5G-preferred for ϕ and Stable(obj ϕ(P, N), A) = T .

Theorem 5.5 Let ϕ ∈ LFK (A), ψ ∈ LK(A), and let ϕ be a knowledge-consistent formula. Then, ψ conditioned by ϕ is strongly almost-surely valid iff ϕ |=S5G ψ.

Proof. First, if ϕ |=S5G ψ, then, from definition of entailment in S5G and from Lemma 5.4 it follows that, for each partition (P,N) that is S5G-preferred for ϕ, ψ belongs to Stable(objϕ(P,N),A), consequently, by Lemma 4.1, ψ ∈ SAS(obj ϕ(P,N),A). Hence, by Lemma 5.2 and Lemma 5.3, for each probability assignment P over A, τP(ψ) ∈ SAS(τP(objϕ(P,N)),Ak ). Therefore, by Theorem 4.5, limn→∞pnPc (τP(ψ)|τP(ϕ)) = 1, which implies that ψ conditioned by ϕ is strongly almost-surely valid.

Conversely, if ϕ ̸|=S5G ψ, then by Lemma 5.4 it follows that there exists a partition (P, N) that is S5G-preferred for ϕ and such that ψ does not belong to Stable(objϕ(P,N),A), consequently, by Lemma 4.1, ψ ̸∈ SAS(obj ϕ(P,N),A). Therefore, by Lemma 5.2, τP(ψ) ̸∈ SAS(τP(objϕ(P,N)),Ak ). Moreover, it is immediate to verify the existence a probability assignment P ′ over A such that, for each partition (P ′ , N ′ ) that is S5G-preferred for ϕ, cp(τP ′ (obj ϕ(P, N))) ≥ cp(τP ′(objϕ(P ′ ,N ′ ))). Consequently, by Lemma 5.1, it follows that limn→∞pnPc (τP(ψ)|τP(ϕ)) < 1, i.e., ψ conditioned by ϕ is not strongly almost-surely valid.

6 Complexity results

As explained above, we consider both the case in which A is a fixed finite alphabet and the case in which it is considered as finite but not fixed in advance. If A is finite and fixed, then, based on the algorithm for entailment in S5G reported in [Donini et al., 1997] it can be easily shown that entailment in S5G can be decided in polynomial time, and therefore, by Theorem 5.5, strong almost-sure conditional validity can be decided in polynomial time as well. Consider now the case of a finite, non-fixed alphabet A.

• Theorem 6.1 Let ϕ ∈ LFK (A), ψ ∈ LK(A), and let ϕ be a knowledge-consistent formula. Deciding whether ψ conditioned by ϕ is strongly almost-surely valid is a Πp2 -complete problem.

Proof. Follows immediately from Theorem 5.5 and from the fact that the entailment problem ϕ |=S5G ψ when ϕ ∈ LFK (A) is Πp2 -complete, which is an immediate consequence of Corollary 4.12 of [Donini et al., 1997] and of Theorem 11 of [Rosati, 1998]).

Next, we study a subclass of flat modal formulas for which deciding strong almost-sure conditional validity is computationally easier than in the general case: the class of honest formulas, introduced by [Halpern and Moses, 1985]. A flat formula ϕ is honest iff it has exactly one S5G-model. It is known that deciding whether ϕ is honest is a Θp2 -complete problem. Moreover, if ϕ is honest, then deciding the entailment ϕ |=S5G ψ is also Θp2 -complete. Therefore, from Theorem 5.5 the following property holds.

• Theorem 6.2 Let ϕ ∈ LFK (A), ψ ∈ LK(A), and let ϕ be a honest formula. Deciding whether ψ conditioned by ϕ is strongly almost-surely valid is Θp2 -complete.

Furthermore, the notion of honesty precisely characterizes the subclass of formulas, among the formulas ϕ such that Kϕ is S5-consistent, that condition according to a 0-1 law, i.e., such that either limn→∞pnP (ψ|ϕ) = 1 for each probability assignment P or limn→∞ pnP (ψ|ϕ) = 0 for each probability assignment P, which is immediately implied by Theorem 5.5 and by the fact that a honest formula has a single S5G-model.

7 Conclusions

The present work can be extended in several directions. In particular, we are currently investigating the following issues: (i) strong almost-sure validity for (classes of) conditioning formulas with nested occurrences of modalities; (ii)

extending the study of asymptotic conditional validity to the framework of multimodal logic; (iii) computing P-almostsure conditional validity, i.e., the value of the asymptotic conditional validity for a given probability distribution P of the truth of primitive propositions.