Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

1 Introduction

There has been a great deal of work on characterizing the complexity of the satisfiability and validity problem for modal logics (see [Halpern and Moses, 1992; Ladner, 1977; Spaan, 1993; Vardi, 1989] for some examples). In particular, Ladner 1977 showed that the validity (and satisfiability) problem for every modal logic between K and S4 is PSPACEhard; and is PSPACE-complete for the modal logics K, T, and S4. He also showed that the satisfiability problem for S5 is NP-complete.

What causes the gap between NP and PSPACE here? We show that, in a precise sense, it is the negative introspection axiom: ¬Kϕ ⇒ K¬Kϕ. It easily follows from Ladner's proof of PSPACE-hardness that for any modal logic L between K and S4, there exists a family of formulas ϕn, all consistent with L such that such that |ϕn| = O(n) but the smallest Kripke structure satisfying ϕ has at least 2n states (where |ϕ| is the length of ϕ viewed as a string of symbols).

∗This work was supported in part by NSF under grants CTC0208535, ITR-0325453, and IIS-0534064, by ONR under grants N00014-00-1-03-41 and N00014-01-10-511, and by the DoD Multidisciplinary University Research Initiative (MURI) program administered by the ONR under grant N00014-01-1-0795. The second author was also supported in part by a scholarship from the Brazilian Government through the Conselho Nacional de Desenvolvimento Cient´ıfico e Tecnol´ogico (CNPq).

†Most of this work was done while the author was at the School of Electrical and Computer Engineering at Cornell University, U.S.A.

Leandro Chaves Rˆego †

Statistics Department Federal University of Pernambuco, Brazil e-mail: leandro@de.ufpe.br

By way of contrast, we show that for all of the (infinitely many) modal logics L containing K5 (that is, every modal logic containing the axiom K-Kϕ ∧ K(ϕ ⇒ ψ) ⇒ Kψand the negative introspection axiom, which has traditionally been called axiom 5), if a formula ϕ is consistent with L, then it is satisfiable in a Kripke structure of size linear in |ϕ|. Using this result and a characterization of the set of finite structures consistent with a logic L containing K5 due to Nagle and Thomason 1985, we can show that the consistency (i.e., satisfiability) problem for L is NP-complete. Thus, roughly speaking, adding negative introspection to any logic between K and S4 lowers the complexity from PSPACE-hard to NPcomplete.

The fact that the consistency problem for specific modal logics containing K5 is NP-complete has been observed before. As we said, Ladner already proved it for S5; an easy modification (see [Fagin et al., 1995]) gives the result for KD45 and K45. 1 That the negative introspection axiom plays a significant role has also been observed before; indeed, Nagle 1981 shows that every formula ϕ consistent with a normal modal logic 2 L containing K5 has a finite model (indeed, a model exponential in |ϕ|) and using that, shows that the provability problem for every logic L between K and S5 is decidable; Nagle and Thomason 1985 extend Nagle's result to all logics containing K5 not just normal logics. Despite all this prior work and the fact that our result follows from a relatively straightforward combination of results of Nagle and Thomason and Ladner's techniques for proving that the consistency problem for S5 is NP-complete, our result seems to be new, and is somewhat surprising (at least to us!).

The rest of the paper is organized as follows. In the next section, we review standard notions from modal logic and the key results of Nagle and Thomason 1985 that we use. In Section 3, we prove the main result of the paper. We discuss related work in Section 4.

1 Nguyen 2005 also claims the result for K5, referencing Ladner. While the result is certainly true for K5, it is not immediate from Ladner's argument.

2 A modal logic is normal if it satisfies the generalization rule RN: from ϕ infer Kϕ.

2 Modal Logic: A Brief Review

We briefly review basic modal logic, introducing the notation used in the statement and proof of our result. The syntax of the modal logic is as follows: formulas are formed by starting with a set Φ = {p, q, . . .} of primitive propositions, and then closing off under conjunction (∧), negation (¬), and the modal operator K. Call the resulting language LK1 (Φ). (We often omit the Φ if it is clear from context or does not play a significant role.) As usual, we define ϕ∨ψ and ϕ ⇒ ψ as abbreviations of ¬(¬ϕ∧¬ψ) and ¬ϕ∨ψ, respectively. The intended interpretation of Kϕ varies depending on the context. It typically has been interpreted as knowledge, as belief, or as necessity. Under the epistemic interpretation, Kϕ is read as "the agent knows ϕ"; under the necessity interpretation, Kϕ can be read "ϕ is necessarily true".

The standard approach to giving semantics to formulas in LK1 (Φ) is by means of Kripke structures. A tuple F = (S, K) is a (Kripke) frame if S is a set of states, and K is a binary relation on S. A situation is a pair (F, s), where F = (S, K) is a frame and s ∈ S. A tuple M = (S,K, π) is a Kripke structure (over Φ) if (S,K) is a frame and π : S × Φ → {true, false} is an interpretation (on S) that determines which primitive propositions are true at each state. Intuitively, (s, t) ∈ K if, in state s, state t is considered possible (by the agent, if we are thinking of K as representing an agent's knowledge or belief). For convenience, we define K(s) = {t : (s, t) ∈ K}.

Depending on the desired interpretation of the formula Kϕ, a number of conditions may be imposed on the binary relation K. K is reflexive if for all s ∈ S, (s, s) ∈ K; it is transitive if for all s, t, u ∈ S, if (s, t) ∈ K and (t, u) ∈ K, then (s, u) ∈ K; it is serial if for all s ∈ S there exists t ∈ S such that (s, t) ∈ K; it is Euclidean iff for all s, t, u ∈ S, if (s, t) ∈ K and (s, u) ∈ K then (t, u) ∈ K. We use the superscripts r, e, t and s to indicate that the K relation is restricted to being reflexive, Euclidean, transitive, and serial, respectively. Thus, for example, S rt is the class of all situations where the K relation is reflexive and transitive.

We write (M, s) |= ϕ if ϕ is true at state s in the Kripke structure M. The truth relation is defined inductively as follows:

A formula ϕ is said to be satisfiable in Kripke structure M if there exists s ∈ S such that (M, s) |= ϕ; ϕ is said to be valid in M, written M |= ϕ, if (M, s) |= ϕ for all s ∈ S. A formula is satisfiable (resp., valid) in a class N of Kripke structures if it is satisfiable in some Kripke structure in N (resp., valid in all Kripke structures in N). There are analogous definitions for situations. A Kripke structure M = (S,K, π) is based on a frame F = (S ′ ,K′ ) if S ′ = S and K′ = K. The formula ϕ is valid in situation (F, s), written (F, s) |= ϕ, where F = (S, K) and s ∈ S, if (M, s) |= ϕ for all Kripke structure M based on F .

Modal logics are typically characterized by axiom systems. Consider the following axioms and inference rules, all of which have been well-studied in the literature [Blackburn et al., 2001; Chellas, 1980; Fagin et al., 1995]. (We use the traditional names for the axioms and rules of inference here.) These are actually axiom schemes and inference schemes; we consider all instances of these schemes.

Prop. All tautologies of propositional calculus

1. (Kϕ∧K(ϕ⇒ψ)) ⇒Kψ (Distribution Axiom)
2. Kϕ⇒ϕ (Knowledge Axiom)
3. Kϕ⇒KKϕ (Positive Introspection Axiom)
4. ¬Kϕ⇒K¬Kϕ (Negative Introspection Axiom)
5. ¬K(false) (Consistency Axiom)
6. MP. Fromϕ and ϕ⇒ψ infer ψ (Modus Ponens)

RN. Fromϕ infer Kϕ (Knowledge Generalization)

The standard modal logics are characterized by some subset of the axioms above. All are taken to include Prop, MP, and RN; they are then named by the other axioms. For example, K5 consists of all the formulas that are provable using Prop, K, 5, MP, and RN; we can similarly define other systems such as KD45 or KT5. KT has traditionally been called T; KT4 has traditionally been called S4; and KT45 has traditionally been called S5.

For the purposes of this paper, we take a modal logic L to be any collection of formulas that contains all instances of Prop and is closed under modus ponens (MP) and substitution, so that if ϕ is a formula in L and p is a primitive proposition, then ϕ[p/ψ] ∈ L, where ϕ[p/ψ] is the result of replacing all instances of p in ϕ by ψ. A logic is normal if it contains all instances of the axiomK and is closed under the inference rule RN. In terms of this notation, Ladner 1977 showed that if L is a normal modal logic between K and S4 (since we are identifying a modal logic with a set of formulas here, that just means that K ⊆ L ⊆ S4), then determining if ϕ ∈ L is PSPACE-hard. (Of course, if we think of a modal logic as being characterized by an axiom system, then ϕ ∈ L iff ϕ is provable from the axioms characterizing L.) We say that ϕ is consistent with L if ¬ϕ /∈ L. Since consistency is just the dual of provability, it follows fromLadner's result that testing consistency is PSPACE-hard for every normal logic between K and S4. Ladner's proof actually shows more: the proof holds without change for non-normal logics, and it shows that some formulas consistent with logics between K and S4 are satisfiable only in large models. More precisely, it shows the following:

Theorem 2.1: [Ladner, 1977]

• (a) Checking consistency is PSPACE complete for every logic between K and S4 (even non-normal logics).
• (b) For every logic L between K and S4, there exists a family of formulas ϕLn, n = 1, 2, 3, . . ., such that (i) for all n, ϕLn is consistent with L, (ii) there exists a constant d such that |ϕLn| ≤ dn, (iii) the smallest Kripke structure that satisfies ϕ has at least 2n states.

There is a well-known correspondence between properties of the K relation and axioms: reflexivity corresponds to T, transitivity corresponds to 4, the Euclidean property corresponds to 5, and the serial property corresponds to D. This correspondence is made precise in the following well-known theorem (see, for example, [Fagin et al., 1995]).

Theorem 2.2: Let C be a (possibly empty) subset of {T, 4, 5, D} and let C be the corresponding subset of {r, t, e, s}. Then {Prop, K, MP, RN} ∪ C is a sound and complete axiomatization of the language LK1 (Φ) with respect to S C (Φ). 3

Given a modal logic L, let S L consist of all situations (F, s) such that ϕ ∈ L implies that (F, s) |= ϕ. An immediate consequence of Theorem 2.2 is that S e , the situations where the K relation is Euclidean, is a subset of SK5 .

Nagle and Thomason 1985 provide a useful semantic characterization of all logics that containK5. We review the relevant details here. Consider all the finite situations ((S, K), s) such that either

1. S is the disjoint union of S1, S2, and {s} and K = ({s} × S1) ∪ ((S1 ∪ S2) × (S1 ∪ S2)), where S2 = ∅ if S1 = ∅; or
2. K = S ×S.

Using (a slight variant of) Nagle and Thomason's notation, let Sm,n, with m ≥ 1 and n ≥ 0 or (m, n) = (0, 0), denote all situations of the first type where |S1| = m and |S2| = n, and let Sm,-1 denote all situations of the second type where |S| = m. (The reason for taking -1 to be the second subscript for situations of the second type will become clearer below.) It is immediate that all situations in Sm,n for fixed m and n are isomorphic-they differ only in the names assigned to states. Thus, the same formulas are valid in any two situations in Sm,n. Moreover, it is easy to check that the K relation in each of the situations above in Euclidean, so each of these situations is in SK5 . It is well known that the situations in Sm,-1 are all in SK5 and the situations in Sm,-1 ∪Sm,0 are all in SKD45 . In fact, S5 (resp., KD45) is sound and complete with respect to the situations in Sm,-1 (resp., Sm,-1 ∪ Sm,0). Nagle and Thomason show that much more is true. Let T L = (∪{Sm,n : m ≥ 1, n ≥ -1 or (m, n) = (0, 0)}) ∩ S L.

Theorem 2.3: [Nagle and Thomason, 1985] For every logic L containing K5, L is sound and complete with respect to the situations in T L.

The key result of this paper shows that if a formula ϕ is consistent with a logic L containing K5, then there exists m, n, a Kripke structure M = (S,K, π), and a state s ∈ S such that ((S, K), s) ∈ Sm,n, Sm,n ⊆ T L, and m+ n < |ϕ|.

3 We remark that soundness and completeness is usually stated with respect to the appropriate class MC of structures, rather than the class S C of situations. However, the same proof applies without change to show completeness with respect to S C , and using S C allows us to relate this result to our later results. While for normal logics it suffices to consider only validity with respect to structures, for non-normal logics, we need to consider validity with respect to situations.

That is, if ϕ is satisfiable at all, it is satisfiable in a situation with a number of states that is linear in |ϕ|.

One more observation made by Nagle and Thomason will be important in the sequel.

Definition 2.4 : A p-morphism (short for pseudoepimorphism) from situation ((S ′ ,K′ ), s′ ) to situation ((S, K), s) is a function f : S ′ → S such that

• f(s′ ) = s;
• if (s1, s2) ∈ K, then (f(s1), f(s2)) ∈ K′ ;
• if (f(s1), s3) ∈ K, then there exists some s2 ∈ S ′ such that (s1, s2) ∈ K′ and f(s2) = s3.

This notion of p-morphism of situations is a variant of standard notions of p-morphism of frames and structures [Blackburn et al., 2001]. It is well known that if there is a pmorphism from one structure to another, then the two structures satisfy the same formulas. An analogous result, which is proved in the full paper, holds for situations.

Theorem 2.5: If there is a p-morphism from situation (F ′ , s′ ) to (F, s), then for every modal logic L, if (F ′ , s′ ) ∈ S L then (F, s) ∈ S L.

Now consider a partial order on pairs of numbers, so that (m, n) ≤ (m′ , n′ ) iff m ≤ m′ and n ≤ n′ . Nagle and Thomason observed that if (F, s) ∈ Sm,n, (F ′ , s′ ) ∈ Sm′ ,n′ , and (1,-1) ≤ (m, n) ≤ (m′ , n′ ), then there is an obvious p-morphism from (F ′ , s′ ) to (F, s): if F = (S,K), S = S1 ∪ S2, F ′ = (S ′ ,K′ ), S ′ = S ′1 ∪ S ′2 (where Si and S ′ i for i = 1, 2 are as in the definition of Sm,n), then define f : S ′ → S so that f(s′ ) = s, f maps S ′1 onto S1, and, if S2 ̸= ∅, then f maps S ′2 onto S2; otherwise, f maps S ′2 to S1 arbitrarily. The following result (which motivates the subscript -1 in Sm,-1) is immediate from this observation and Theorem 2.5.

Theorem 2.6: If (F, s) ∈ Sm,n, (F ′ , s′ ) ∈ Sm′ ,n′ , and (1,-1) ≤ (m, n) ≤ (m′ , n′ ), then for every modal logic L, if (F ′ , s′ ) ∈ T L then (F, s) ∈ T L.

3 The Main Results

We can now state our key technical result.

Theorem 3.1: If L is a modal logic containing K5 and ¬ϕ /∈ L, then there exist m, n such that m+ n < |ϕ|, a situation (F, s) ∈ S L ∩ Sm,n, and structure M based on F such that (M, s) |= ϕ.

Proof: By Theorem 2.3, if ¬ϕ /∈ L, there is a situation (F ′ , s0) ∈ T L such that (F ′ , s0) ̸|= ¬ϕ. Thus, there exists a Kripke structure M ′ based on F ′ such that (M ′ , s0) |= ϕ. Suppose that F ′ ∈ Sm′ ,n′ . If m′ + n′ < |ϕ|, we are done, so suppose that m′ + n′ ≥ |ϕ|. Note that this means m′ ≥ 1. We now construct a a situation (F, s) ∈ Sm.n such that (1, -1) ≤ (m, n) ≤ (m′ , n′ ), m + n < |ϕ|, and (M, s) |= ϕ for some Kripke structure based on F . This gives the desired result. The construction of M is similar in spirit to Ladner's 1977 proof of the analogous result for the case of S5.

Let C1 be the set of subformulas of ϕ of the formKψ such that (M ′ , s0) |= ¬Kψ, and let C2 be the set of subformulas of ϕ of the form Kψ such that KKψ is a subformula of ϕ and (M ′ , s0) |= ¬KKψ ∧Kψ. (We remark that it is not hard to show that if K is either reflexive or transitive, then C2 = ∅.)

Suppose that M ′ = (S ′ ,K′ , π′ ). For each formula Kψ ∈ C1, there must exist a state sC1 ψ ∈ K′ (s0) such that (M ′ , sC1 ψ ) |= ¬ψ. Note that if C1 ̸= ∅ then K′ (s0) ̸= ∅. Define I(s0) = {s0} if s0 ∈ K′ (s0), and I(s0) = ∅ otherwise. Let S1 = {sC1 ψ : Kψ ∈ C1} ∪ I(s0). Note that S1 ⊆ K′ (s0) = S ′1 , so |S1| ≤ |S ′1 |. If Kψ ∈ C2 then KKψ ∈ C1, so there must exist a state sC2 ψ ∈ K′ (sC1 Kψ ) such that (M ′ , sC2 ψ ) |= ¬ψ. Moreover, since (M ′ , s0) |= Kψ, it must be the case that sC2 ψ /∈ K′ (s0). Let S2 = {sC2 ψ : Kψ ∈ C2}. By construction, S2 ⊆ S ′2 , so |S2| ≤ |S ′2 |, and S1 and S2 are disjoint. Moreover, if S1 = ∅, then C1 = ∅, so C2 = ∅ and S2 = ∅.

Let S = {s0} ∪S1 ∪S2. Define the binary relation K on S by taking K(s0) = S1 and K(t) = S1 ∪ S2 for t ∈ S1 ∪ S2. In the full paper, we show that K is well defined; in particular, we show that (a) s0 /∈ S2 and (b) if s0 ∈ S1, then S2 = ∅. We also show that K is the restriction of K′ to S.

Let M = (S,K, π), where π is the restriction of π′ to {s0}∪S1∪S2. It is well known [Fagin et al., 1995] (and easy to prove by induction on ϕ) that there are at most |ϕ| subformulas of ϕ. Since C1 and C2 are disjoint sets of subformulas of ϕ, all of the formKψ, and at least one subformula of ϕ is a primitive proposition (and thus not of the formKψ), it must be the case that |C1| + |C2| ≤ |ϕ| - 1, giving us the desired bound on the number of states.

In the full paper we show, by a relatively straightforward induction on the structure of formulas, that for all states s ∈ S and for all subformulas ψ of ϕ (including ϕ itself), (M, s) |= ψ iff (M ′ , s) |= ψ. The proof proceeds by induction on the structure of ϕ.

By construction, (F, s) ∈ Sm,n, where m = |S1| and n = |S2|. We have already observed that m+n < |ϕ|, |S1| ≤ |S ′1 |, and |S2| ≤ |S ′2|. Thus, (m, n) ≤ (m′ , n′ ). It follows from Theorem 2.6 that (F, s) ∈ T L ⊆ S L. This completes the proof.

The idea for showing that the consistency problem for a logic L that contains K5 is NP-complete is straightforward. Given a formula ϕ that we want to show is consistent with L, we simply guess a frame F = (S, K), structure M based on F , and state s ∈ S such that (F, s) ∈ Sm,n with m+n < |ϕ|, and verify that (M, s) |= ϕ and Sm,n ⊆ T L. Verifying that (M, s) |= ϕ is the model-checking problem. It is well known that this can be done in time polynomial in the number of states of M, which in this case is linear in |ϕ|. So it remains to show that, given a logic L containing K5, checking whether Sm,n ⊆ T L can be done efficiently. This follows from observations made by Nagle and Thomason 1985 showing that that, although T L may include Sm′ ,n′ for infinitely many pairs (m′ , n′ ), T L has a finite representation that makes it easy to check whether Sm.n ⊆ T L.

Say that (m, n) is a maximal index of T L if m ≥ 1, Sm,n ⊆ T L, and it is not the case that Sm′ ,n′ ⊆ T L for some (m′ , n′ ) with (m, n) < (m′ , n′ ). It is easy to see that T L can have at most finitely many maximal indices. Indeed, if (m, n) is a maximal index, then there can be at most m+n-1 maximal indices, for if (m′ , n′ ) is another maximal index, then either m′ < m or n′ < n (for otherwise (m, n) ≤ (m′ , n′ ), contradicting the maximality of (m, n)). Say that m ≥ 1 is an infinitary first index of T L if Sm,n ⊆ T L for all n ≥ -1. Similarly, say that n ≥ -1 is an infinitary second index of T L if Sm,n ⊆ T L for all m ≥ 1. Note that it follows from Theorem 2.6 that if (1, -1) ≤ (m, n) ≤ (m′ , n′ ), then if m′ is an infinitary first index of T L, then so is m, and if n′ is an infinitary second index of T L, then so is n. Suppose that m∗ is the largest infinitary first index of T L and n∗ is the largest infinitary second index of T L, where we take m∗ = n∗ = ∞ if all first indices are infinitary (or, equivalently, if all second indices are infinitary), we take m∗ = 0 if no first indices are infinitary, and we take n∗ = -2 if no second indices are infinitary. It follows from all this that T L can be represented by the tuple (i, m∗ , n∗ , (m1, n1), . . . , (mk, nk)), where

• i is either 0 or 1, depending on whether S0,0 ∈ T L;
• m∗ is the largest infinitary first index;
• n∗ is the largest infinitary second index; and
• ((m1, n1), . . . , (mk, nk) are the maximal indices.

Given this representation of T L, it is immediate that Sm,n ⊆ T L iff one of the following conditions holds:

• (m, n) = (0, 0) and i = 1;
• 1 ≤m≤m∗ ;
• -1 ≤ n ≤ n∗ ; or
• (m, n) ≤ (mk, nk).

We can assume that the algorithm for checking whether a formula is consistent with L is "hardwired" with this description of L. It follows that only a constant number of checks (independent of ϕ) are required to see if Sm,n ⊆ T L. 4

Putting all this together, we get our main result.

Theorem 3.2: For all logics L containing K5, checking whether ϕ is consistent with L is an NP-complete problem.

4 Discussion and RelatedWork

We have shown all that, in a precise sense, adding the negative introspection axiom pushes the complexity of a logic between K and S4 down from PSPACE-hard to NP-complete. This is not the only attempt to pin down the NP-PSPACE gap and to understand the effect of the negative introspection axiom. We discuss some of the related work here.

A number of results showing that large classes of logics have an NP-complete satisfiability problem have been proved recently. For example, Litak and Wolter 2005 show that the satisfiability for all finitely axiomatizatble tense logics of linear time is NP-complete, and Bezhanishvili and Hodkinson 2004 show that every normal modal logic that properly extends S52 (where S52 is the modal logic that contains two modal operators K1 and K2, each of which satisfies the axioms and rules of inference of S5 as well as the axiom K1K2p ⇔ K2K1p) has a satisfiability problem that is NP-complete. Perhaps the most closely related result is that of Hemaspaandra 1993, who showed that the consistency problem for any normal logic containing S4.3 is also NP-complete. S4.3 is the logic that results from adding the following axiom, known in the literature as D1, to S4:

4 Here we have implicitly assumed that checking whether inequalities such as (m, n) ≤ (m′ , n′ ) hold can be done in one time step. If we assume instead that it requires time logarithmic in the inputs, then checking if Sm,n ⊆ T L requires time logarithmic in m+ n, since we can take all of m∗, n∗ ,m1, . . .mk, n1, . . . , nk to be constants.

D1 is characterized by the connectedness property: it is valid in a situation ((S,K), s) if for all s1, s2, s3 ∈ S, if (s1, s2) ∈ K and (s1, s3) ∈ K, then either (s2, s3) ∈ K or (s3, s2) ∈ K. Note that connectedness is somewhat weaker than the Euclidean property; the latter would require that both (s2, s3) and (s3, s2) be in K.

As it stands, our result is incomparable to Hemspaandra's. To make the relationship clearer, we can restate her result as saying that the consistency property for any normal logic that contains K and the axioms T, 4, and D1 is NP-complete. We do not require either 4 or T for our result. However, although the Euclidean property does not imply either transitivity or reflexivity, it does imply secondary reflexivity and secondary transitivity. That is, if K satisfies the Euclidean property, then for all states s1, s2, s3, s4, if (s1, s2) ∈ K, then (s2, s2) ∈ K and if (s2, s3) and (s3, s4) ∈ K, then (s2, s4) ∈ K; roughly speaking, reflexivity and transitivity hold for all states s2 in the range of K. Secondary reflexivity and secondary transitivity can be captured by the following two axioms:

Both T′ and 4′ follow from 5, and thus both are sound in any logic that extends K5. Clearly T′ and 4′ also both hold in any logic that extends S4.3, since S4.3 contains T, 4, and the inference rule RN. We conjecture that the consistency property for every logic that extends K and includes the axioms T′ , 4′ , and D1 is NP-complete. If this result were true, it would generalize both our result and Spaan's result.

Vardi 1989 used a difference approach to understand the semantics, rather than relational semantics. This allowed him to consider logics that do not satisfy the K axiom. He showed that some of these logics have a consistency problem that is NP-complete (for example, the minimal normal logic, which characterized by Prop, MP, and RN), while others are PSPACE-hard. In particular, he showed that adding the axiom Kϕ ∧ Kψ ⇒ K(ϕ ∧ ψ) (which is valid in K) to Prop, MP, and RN gives a logic that is PSPACE-hard. He then conjectured that this ability to "combine" information is what leads to PSPACE-hardness. However, this conjecture has been shown to be false. There are logics that lack this axiom and, nevertheless, the consistency problem for these logics is PSPACE-complete (see [Allen, 2005] for a recent discussion and pointers to the relevant literature).

All the results for this paper are for single-agent logics. Halpern and Moses 1992 showed that the consistency problem for a logic with two modal operators K1 and K2, each of which satisfies the S5 axioms, is PSPACE-complete. Indeed, it is easy to see that if Ki satisfies the axioms of Li for some normal modal logic Li containingK5, then the consistency problem for the logic that includes K1 and K2 must be PSPACE-hard. This actually follows immediately from Ladner's 1977 result; then it is easy to see that K1K2, viewed as a single operator, satisfies the axioms of K. We conjecture that this result continues to hold even for non-normal logics.

We have shown that somewhat similar results hold when we add awareness to the logic (in the spirit of Fagin and Halpern 1988), but allow awareness of unawareness [Halpern and Rˆego, 2006]. In the single-agent case, if the K operator satisfies the axioms K, 5, and some (possibly empty) subset of {T, 4}, then the validity problem for the logic is decidable; on other hand, if K does not satisfy 5, then the validity problem for the logic is undecidable. With at least two agents, the validity problem is undecidable no matter which subset of axioms K satisfies. We conjecture that, more generally, if the K operator satisfies the axioms of any logic L containing K5, the logic of awareness of unawareness is decidable, while if K satisfies the axioms of any logic between K and S4, the logic is undecidable.

All these results strongly suggest that there is something about the Euclidean property (or, equivalently, the negative introspection axiom) that simplifies things. However, they do not quite make precise exactly what that something is. More generally, it may be worth understanding more deeply what is about properties of the K relation that makes things easy or hard. We leave this problem for future work.

Acknowledgments

We thank the IJCAI reviewers for useful comments and for catching an error in the previous version of the paper.