Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals

1 Introduction

One of the long-standing aims in the area of Knowledge Representation and Reasoning has been to devise computationally attractive reasoning mechanisms for very expressive knowledge bases (KBs). The need for an expressive representation language arises when one needs to deal with incomplete information. For example, a KB may know 1 that either Sue or Sam is a teacher or that Sid is not a teacher without knowing for any particular person that he or she is a teacher. While first-order logic (FOL) is able to represent such incompleteness, it is well known that reasoning in FOL based on classical logical entailment is undecidable. A principled way to arrive at weaker forms of entailment is to come up with appropriate models of limited belief [Levesque, 1984b; Konolige, 1986; Vardi, 1986; Fagin and Halpern, 1988; Fagin et al., 1990; Lakemeyer, 1996; Cadoli and Schaerf, 1992; Delgrande, 1995; Liu et al., 2004], where reasoning can be studied as the question of which beliefs follow logically from believing the sentences in the KB. In order to be able to study

1 Throughout the paper, we will use the terms knowledge and belief interchangeably.

Hector J. Levesque

Dept. of Computer Science University of Toronto, Toronto, Ontario Canada M5S 3A6

hector@cs.toronto.edu

the properties of such a model of belief, it seems particularly desirable to have a perspicuous semantics.

Despite many years of research in this area, there have not been that many proposals of this kind. One notable exception is the work by Liu, Lakemeyer, and Levesque [2004] (henceforth abbreviated as LLL), which is also the starting point of this paper. Based on earlier work by Lakemeyer and Levesque [Lakemeyer and Levesque, 2002], LLL propose the logic SL, which uses as semantic primitive a setup, which is a possibly infinite set of ground clauses closed under unit propagation. Roughly, the clauses in a setup can be viewed as those which the agent believes explicitly. They then consider a sequence of modalities Bk, for k ≥ 0, where Bkφ should be read as "φ is believed at level k." For example, given a clause c, B0c is satisfied by a setup s just in case there is a clause in s contained in c. In other words, at level 0, belief essentially reduces to retrieval wrt. s. At level 1, the agent believes everything that is believed at level 0 and, in addition, the agent is able to reason by cases allowing to split a single clause in s. At belief level 2, the number of possible case splits increases to 2, and so on.

For example, consider a setup s consisting of a single clause (Teacher(sue) ∨ Teacher(sam)). Then s satisfies B0(Teacher(sue) ∨ Teacher(sam) ∨ Teacher(zoe)) by subsumption, but s does not satisfy B0∃x.Teacher(x) because there is no name n for which B0Teacher(n) holds at s. On the other hand, s does satisfy B1∃x.Teacher(x) because we can split the clause in s, and in one case we can choose n = sue and in the other n = sam. LLL present other, more complicated examples which demonstrate that this kind of existential reasoning may easily require many case splits in classical FOL. In fact, this problem alone is known to be undecidable in general [Patel-Schneider, 1985].

In this setting, a reasoning service for a KB can be defined as the problem of computing, for a given k, whether Bkφ is logically implied by B0KB. LLL show that for a certain kind of so-called proper+ KBs, this reasoning service is decidable and indeed tractable in the propositional case.

While this work is an interesting contribution towards a computationally attractive and a semantically well-founded reasoning service, it still has a number of limitations. For one, the beliefs considered by LLL may not themselves refer to beliefs, which is needed to account for introspective agents. For example, continuing the above example, we may want to say that s satisfies B1(∃x.Teacher(x) ∧ ¬B0(∃x.Teacher(x))) and B1(∃x.Teacher(x) ∧ ¬B1Teacher(x)). The latter is particularly interesting as it expresses that the agent believes at level 1 that someone is a teacher but it does not know who that teacher is. In other words, introspection allows the agent to distinguish between de dicto and de re beliefs. Another shortcoming of SL directly related to this distinction is the assumption that all constants of the language are rigid, that is, they are standard names whose identity is known by definition. For example, B0Teacher(bestFriendOfSue) logically entails ∃x.B0Teacher(x), which seems too strong.

In this paper we will address both of these issues by extending the logic SL to the new logic LB. The idea of a setup and how beliefs at different levels come about will be lifted from SL. Full introspection will be built into the new logic allowing an arbitrary nesting of beliefs at all levels and in any order. One of the main results of this paper will be that introspective reasoning remains decidable and that reasoning about nested beliefs is reducible to reasoning about non-nested beliefs in SL. Our proposal to deal with unknown individuals is inspired by recent work by De Giacomo et al [2011]. Again we will provide a decidable reduction to reasoning in SL. To keep the technical treatment of unknown individuals simple, we will consider them only for non-nested beliefs.

Considering introspection is perhaps most interesting when an agent is able to draw conclusions about what it does not believe. To specify a reasoning service with this feature, the assumption of B0KB turns out to be too weak, as it only says that at least the sentences of the KB are believed explicitly so that nothing is entailed about what is not believed. What is needed instead is a notion that the sentences in the KB are all that is believed or that the KB is only-known. For this purpose we will introduce another operator O so that the reasoning service is then characterized by the beliefs which are entailed by OKB. To simplify matters for the purposes of this paper, we only consider O at level 0 and hence leave out the subscript altogether.

1.1 RelatedWork

Modelling belief has had a long tradition starting with Hintikka's possible-world approach [Hintikka, 1962] (see also [Halpern and Moses, 1992]). While intuitively appealing, the possible-world model suffers from the logical omniscience problem [Hintikka, 1975] so that reasoning services based on this model are intractable in the propositional case and undecidable when the language is first order. The approaches addressing the logical omniscience problem can roughly be characterized as syntactic or semantic. The syntactic approaches include [Konolige, 1986; Vardi, 1986; Fagin and Halpern, 1988] and either include sets of sentences as part of the interpretation of belief or use notions such as awareness to rule out certain beliefs. Examples of the semantic approach are [Levesque, 1984b; Cadoli and Schaerf, 1992; Lakemeyer, 1996], which are based on tautological entailment [Anderson and Belnap, 1975; Dunn, 1976; Patel-Schneider, 1985] using four truth values instead of the usual two. While the syntactic approach can be criticized for being perhaps too fine-grained and not providing enough guidance as to which beliefs to include and which to leave out, the semantic approaches are much more in line with the possible-world tradition, but they also have a significant downside: the beliefs that follow from believing the sentences in a knowledge base are extremely weak, as Modus ponens is completely ruled out. For example, from p and p ⊃ q it is not possible to infer q. Moreover, these approaches also need to deal with the fact that reasoning about existentials is undecidable even without Modus ponens [Patel-Schneider, 1985]. Hence reasoning becomes even weaker once decidability is restored. The model of belief underlying the logic SL can be seen as a compromise between the two camps. On the one hand, there is a syntactic flavour in that setups consist of clauses. On the other hand, there are well-motivated semantic rules which determine the beliefs at any level. Most importantly, reasoning becomes more and more powerful with increasing belief levels while remaining decidable. For these reasons, SL is an attractive starting point for further investigations into limited, semantically coherent reasoning.

The rest of the paper is organized as follows. In the next chapter, we introduce the logic LB and demonstrate its connection to SL and further properties. In Section 4 we show how reasoning about nested beliefs in the context of proper+ KBs can be reduced to reasoning in SL. In Section 5, we consider unknown individuals and then we conclude.

2 The Logic LB

The language is a first-order modal dialect with an infinite supply of predicate symbols of every arity, including =, and an infinite supply of standard names #1, #2, #3, . . . , which are syntactically treated like constants but which are intended to be isomorphic to the (fixed) domain of discourse. 2 For now, no other constants or function symbols are allowed. Besides the usual connectives ¬, ∨ and the quantifier ∃ we have modal operators Bk for k = 0, 1, 2, . . . and the modal operator O. The terms of the language are variables and standard names. An atomic formula is either a predicate symbol P with terms as arguments or of the form (t = t′ ) where t and t′ are terms. Formulas are the least set which contain the atomic formulas, and if α and β are formulas and x a variable, then so are ¬α, α ∨ β, ∃x.α,Bkα, and Oα, with the restriction that O may not appear within the scope of any modal operator and that for any Oα, α contains no modal operators. We also allow the special symbol □, intended to represent the empty clause, to appear as a subformula within the scope of a modal operator. Bkα should be read as "α is believed at level k" and Oφ as "φ is all that is known (or only-known)."

As is customary, we will freely use the logical connectives ∧,⊃,≡ and the quantifier ∀ as the usual syntactic abbreviations. Given a formula α, we write αxn to mean the result of replacing every free occurrence of x within α by n.

Predicate symbols applied to standard names are called primitive formulas. Sentences are formulas without free variables. Formulas without modal operators are called objective, formulas where all predicate symbols other than = appear within the scope of a modal operator are called subjective, and formulas which do not mention O are called basic.

2 In other words, standard names can be thought of as constants that satisfy the unique name assumption and an infinitary version of domain closure. See [Levesque, 1984a] for a discussion of why the assumption of a countably infinite domain is not really a limitation.

As clauses play an essential role in the semantics, we introduce them here together with some other conventions. A clause is a disjunction of literals, where a literal is either an atomic formula or its negation. The complement of a literal l is often denoted as l. We will identify a clause with the set of literals it contains. A primitive clause is a clause which consists only of primitive formulas and their negations. In other words, primitive clauses mention neither variables nor =. As already mentioned, the empty clause is denoted as □. A unit clause is a clause with a single literal.

Given a set s of primitive clauses, the closure of s under unit propagation, which we denote as UP(s), is defined as the least set s′ which contains s, and if unit clause l ∈ s′ and {l} ∪ c ∈ s′ , then c ∈ s′ . VP(s) is defined as the set {c | c is a primitive clause and there exists a c′ ∈ UP(s) such that c′ ⊆ c}.

The semantics of LB is based on worlds, which determine what is true apart from the agents beliefs, and setups, which determine what the agent believes. A world is a mapping from the set of all primitive formulas to {0, 1}. A setup is a possibly infinite set of primitive clauses. Roughly, these represent what the agent believes explicitly (at level 0). As we will see, beliefs at higher levels will be obtained by case splitting from the given setup.

Given a world w and a setup s, the truth of a sentence α, written as s, w |= α is defined as follows:

1. s,w |= P(⃗n) iff w[P(⃗n)] = 1;
2. s,w |= (n =m) iff n,m are identical standard names;
3. s,w |= ¬α iff s,w |̸= α;

1. s, w |= ∃x.α iff s, w |= αxn for some standard name n;
2. s, w |= Bkα iff s, s, k |= α (defined below);

Compared to classical logic, only the last three rules are non-standard. Rule 5 is somewhat special as it gives a substitutional account of quantification. This is possible because the set of standard names is essentially the universe of discourse and part of the language. While there are philosophical arguments criticizing substitutional interpretations [Kripke, 1976], it allows us to make de dicto vs. de re distinctions in a simple manner and it greatly simplifies the overall technical apparatus. Let us now turn to the semantics of belief.

Let the length of a basic formula α, denoted as |α|, be defined in the usual way except that we let |Bkα| = (k + 1) + |α|. It is easy to see that |Bkα| > |α| and |Bk+1α| > |Bkα| for all k. To make sure that the following inductive definition of s, s′ , k |= α is well-founded, we need to define a measure that not only takes into account the length of α but also k. A simple way to achieve this is as follows: for any pair (k, α), let ‖ (k, α) ‖= (k + 1) + |α|.

For any setups s, s′ , any k ≥ 0 and any basic sentence α, we let s, s′ , k |= α be the least relation that satisfies the following:

1. s, s′ , k |= α if □ ∈ UP(s′ );
2. s, s′ , k |= c if k = 0, c is a clause and c ∈ VP(s′ );

1. s, s′ , k |= (n =m) if n,m are identical std. names; s, s′ , k |= ¬(n = m) if n, m are distinct std. names;

The above rules state the various ways sentences can be believed at level k. Rule 8 simply says that as soon as the empty clause is derivable by unit propagation, then everything is believed. Rule 9 deals with the base case of belief at level 0, that is, a clause is explicitly believed if it is a member of VP(s′ ) or, equivalently, a superset of a clause in UP(s′ ). Rule 10 deals with the the case where k > 0 and it is possible to establish that α is believed at level k - 1 after splitting a clause. Rule 11 means that we have perfect reasoning about equalities and this is independent of any setup. Rules 12-14 establish certain "obvious" beliefs, for example from either believing α or believing β one can conclude believing α ∨ β (Rule 13). Finally, Rule 15 deals with nested beliefs. As we will see, the effect is a fully introspective agent. Notice that s′ is replaced by s on the RHS. In fact, this rule is the reason why we require two setups. While s′ may change due to Rule 10, s remains fixed and determines the interpretation of all nested beliefs.

With the semantics of Bkα in hand, let us now take a brief look at the meaning of O. Intuitively, the definition says that to only-know α the agent believes α explicitly and no other setup with truly fewer explicit beliefs believes α explicitly. We will come back to O in more detail in Section 4.

To conclude the semantic definitions, we say that a sentence α is valid (written |= α) iff s,w |= α for all setups s and all worlds w. When α is subjective, the world w plays no role and we will often write s |= α instead of s, w |= α.

3 The connection with the logic SL

We begin our investigations of the properties of LB by introducing a slight variant of SL and establishing that the two logics agree on all sentences of SL. Its formulas consist of all basic subjective sentences of LB yet without nesting of beliefs.

We begin by introducing (Bkφ)↓, which, roughly, denotes the SL formula resulting from pushing the belief operator into φ. The purpose is to allow obvious conclusions from (Bkφ)↓ to Bkφ. For any φ ∈ L, the SL formula (Bkφ) ↓ is defined as follows:

1. (Bkc)↓ = Bkc, where c is a clause;
2. (Bk(t = t′ ))↓ = (t = t′ );
3. (Bk¬(t = t′ ))↓ = ¬(t = t′ );

1. (Bk¬¬φ)↓ = Bkφ;
2. (Bk(φ ∨ψ))↓ = (Bkφ ∨Bkψ), where φ or ψ is not a clause;
3. (Bk¬(φ ∨ψ))↓ = (Bk¬φ ∧Bk¬ψ);
4. (Bk∃x.φ)↓ = ∃x.Bkφ;
5. (Bk¬∃x.φ)↓ = ∀x.Bk¬φ.

As discussed above, the semantics of SL is based on setups. Worlds are not needed as only subjective formulas are considered. Let s be a setup. Then for any sentence α ∈ SL, s |=SL α (read "s satisfies α in SL") is defined inductively 3 as follows:

1. s |=SL (d = d′ ) iff d and d′ are the same constant;
2. s |=SL ¬α iff s ̸|=SL α;
3. s |=SL α∨ β iff s |=SL α or s |=SL β;
4. s |=SL ∃x.α iff for some constant d, s |=SL αx d ;
5. s |=SL Bkφ iff one of the following holds:
6. (a) inconsistent: □ ∈ UP(s);
7. (b) subsume: k = 0, φ is a clause c, and c ∈ VP(s);
8. (c) reduce: φ is not a clause and s |=SL (Bkφ)↓;
9. (d) split: k > 0 and there is some c ∈ s such that for all ρ ∈ c, s ∪ {ρ} |=SL Bk-1φ.

A sentence α is valid in SL (|=SL α) if for every setup s, we have that s |=SL α.

We deviate slightly from the original proposal of SL by adding the rule (5a), which says that everything is believed as soon as □ is part of the setup after unit propagation. While this changes some properties of beliefs about =, 4 it is easy to see that all other results, including those about decidability, remain the same.

In order to establish that LB and SL coincide on all sentences of SL, the following lemma is needed.

Lemma 1 For any objective φ, setups s and s′ and k ≥ 0, s |=SL Bkφ iff s′ , s, k |= φ

Proof: The proof is by induction on k and |φ|. Let k = 0. If φ is a clause c, then s |=SL B0c iff c ∈ VP(s) iff s′ , s, 0 |= c. The other cases for φ follow easily by induction. Here we consider only ∃: s |=SL B0∃x.φ iff s |=SL ∃xB0φ iff s |= B0φxn for some n iff (by ind.) s′ , s, 0 |= φxn for some n iff s′ , s, 0 |= ∃xφ.

Suppose the lemma holds for k-1. Here we only consider the case for splitting a clause. (The other cases follow again by a simple induction on |φ|.) Let s |=SL Bkφ and suppose there is a c ∈ s such that for all ρ ∈ c, s ∪ {ρ} |=SL Bk-1φ. Then, by induction, s′ , s ∪ {ρ}, k - 1 |= φ for all ρ ∈ c and hence s′ , s, k |= φ. The reverse direction in case of clause splitting is analogous.

Using this lemma it is easy to show that Lemma 2 For every α ∈ SL, setup s, and world w, s |=SL α iff s, w |= α.

3 LLL demonstrate that the induction is indeed well defined.

4 For example, while Bke ≡ e is valid in the original SL for all e mentioning only =, we only have that ¬Bk□ ⊃ (Bke ≡ e) is valid.

As an immediate consequence, we obtain

In other words, for basic non-nested sentences, LB inherits all the properties of SL. For example, we have that for any i, j there is a k s.t. |=Biφ ∧Bj(φ ⊃ ψ) ⊃Bkψ. 5

We now consider proper+ KBs, which were originally introduced in [Lakemeyer and Levesque, 2002] and are an extension of the proper KBs proposed in [Levesque, 1998]. Let θ denote a substitution of all variables by standard names. We write αθ as the result of applying the substitution to α. We use ∀α to mean the universal closure of α. We let e range over ewffs, which are quantifier-free formulas containing no predicate symbols other than =.

Let e be an ewff and c a clause. Then a formula of the form ∀(e ⊃ c) is called a ∀-clause. A KB is called proper+ if it is a finite non-empty set of ∀-clauses. Given a proper+ KB, we define gnd(KB) as the possibly infinite setup {cθ | ∀(e ⊃ c)∈ KB and |= eθ}. In the following we will use KB both as a set of sentences and as a conjunction of the sentences it contains.

An example proper+ KB is {∀x, y.(x = #1 ∧ y = #2) ⊃ (Teacher(x) ∨ Teacher(y), ∀x.x ̸= #1 ⊃ Female(x)}.

LLL established that determining the beliefs at any level k of a proper+ KB is decidable.

Theorem 2 (LLL) For any proper+ KB and objective φ, |=SL B0KB ⊃ Bkφ is decidable.

Given Thm. 1, we obtain the same decidability result for LB:

Corollary 1 For any proper+ KB and objective φ, the validity of B0KB ⊃ Bkφ is decidable in LB.

LLL proved that the reasoning service as defined by the above implications, is always sound with respect to classical reasoning and they showed tractability in the propositional case. Given the undecidability of classical reasoning, reasoning is also necessarily incomplete. For example, we have that |̸= B0p ⊃ Bk(q ∨ ¬q) for all k.

Let us now go beyond SL and consider nested beliefs.

4 Nested beliefs

We begin by generalizing a result by LLL, which says that anything that is believed at level k is also believed at levels higher than k.

Proposition 1 For any basic α, |= Bkα ⊃ Bk+1α.

Proof: Suppose s,w |= Bkα. We need to consider two cases for s. If s is empty, then a simple induction on |α| shows that for all k, j, s, s, k |= α iff s, s, j |= α, from which the lemma follows. Now let s be non-empty. Again, a simple induction on |α| shows that for all s, s′ and literal ρ, if s, s′ , k |= α then s, s′ ∪ {ρ}, k |= α. By assumption, we have s, s, k |= α. We can then pick an arbitrary clause c ∈ s such that for all ρ ∈ c, s, s ∪ {ρ}, k |= α, from which s, w |= Bk+1α follows using Rule 15 of the semantics.

5 We remark that, given our slight change of the semantics of SL, this property holds for all objective ψ and not just equality-free ψ as in the original SL.

It is easy to see that our model of belief is fully introspective. For example, if p is believed at some level k then at any level j it is believed that p is believed at k. We also obtain the Barcan formula since standard names are the fixed universe of discourse.

Proposition 2

1. |=Bkα ⊃BjBkα
2. |= ¬Bkα ⊃Bj¬Bkα
3. |= ∀xBkα ⊃Bk∀xα.

Proof: Here we only prove (1.). Let s,w |= Bkα. Then s, s, k |= α. By Rule 15, we then also have s, s, j |= Bkα from which s, w |= BjBkα follows.

4.1 A reasoning service for introspective KBs

We now turn to the issue of specifying a reasoning service for introspective proper+ knowledge bases in LB. As we argued already in the beginning, being able to draw conclusions about its own ignorance, an agent needs to assume that its KB is all that it knows, and it is for this purpose that we included the only-knowing operator O in our logic. The specification of the reasoning service will then be in terms of the valid sentences of the form

Let us begin by considering which setups s only-know a proper+ KB. It turns out that there is essentially a unique s with this property:

Theorem 3 s,w |=OKB iff VP(s) = VP(gnd(KB)).

Proof: For the only-if direction, let s |= OKB. Then s |= B0KB. Hence s |= B0c for all c ∈ gnd(KB) and, therefore, c ∈ VP(s). As shown by LLL, this implies VP(gnd(KB)) ⊆ VP(s). To show that VP(s) ⊆ VP(gnd(KB)), suppose otherwise. Then VP(gnd(KB)) ⊊ VP(s). However, VP(gnd(KB)) |= B0KB, contradicting the assumption that s |=OKB.

Conversely, let VP(s) = VP(gnd(KB)). Then clearly s |= B0KB. Now consider a setup s′ with VP(s′ ) ⊊ VP(s). Then there is a c ∈ gnd(KB) such that c ̸∈ VP(s′ ). But then s′ |̸= B0c and hence s′ |̸=B0KB.

Hence it suffices to consider only the possibly infinite setup gnd(KB) when determining whether implications of the form OKB ⊃ Bkα are valid. As a consequence, O can be replaced by B0 in the case of objective beliefs.

Theorem 4 For any proper+ KB and objective φ,

Proof: The if direction is immediate since |= OKB ⊃ B0KB. Conversely, let |= OKB ⊃ Bkφ and s |= B0KB. Then VP(gnd(KB)) ⊆ VP(s). By Theorem 3, VP(gnd(KB)) |= OKB. Thus, by assumption, VP(gnd(KB)) |=Bkφ. By Prop. 4 of LLL, s |=Bkφ.

We are now ready to consider nested beliefs of a KB. For example, suppose sam and sue are standard names and let KB = (Teacher(sue) ∨ Teacher(sam)), which can easily be massaged into proper+ form. As expected, we have

that is, the KB believes at level 1 that someone is a teacher but does not knowwho it is.

Proof: By Theorem 3, it suffices to consider s |=OKB with s = {Teacher(sue) ∨Teacher(sam)}. Then we have s, s, 1 |= ∃x.Teacher(x) because we can split the clause in s and obtain s, s∪{Teacher(sam)}, 0 |= ∃x.Teacher(x) (choose x = sam) in one case and s, s ∪ {Teacher(sue)}, 0 |= ∃x.Teacher(x) (choose x = sue) in another.

However, s, s ∪ {Teacher(sam)}, 0 |= ¬B1Teacher(sam) because s, s, 1 |̸= B1Teacher(sam), and similar for x = sue.

Putting things together, we therefore have that s |= B1(∃x.Teacher(x) ∧ ¬B1(Teacher(x))).

Note also that |= OKB ⊃ ¬B0(∃x.Teacher(x)) since at level 0 we are not allowed to reason by cases.

The main question now is how to automate introspective reasoning for proper+ KBs. As we will see, we can leverage an idea originally proposed by Levesque [1984a] for a classical modal reasoner, where reasoning about nested beliefs is reduced to reasoning about objective beliefs.

The key idea is to replace occurrences of nested beliefs such as B1(Teacher(x)) by a description of the known teachers. In our example, there are no known teachers and hence the formula is replaced by FALSE. 6 As we will see, nested beliefs such as B1¬B0(Teacher(x)) can be handled recursively.

The approach then is to define, given an objective formula φ with free variables ⃗x, a function RES[k, φ, KB], which produces an ewff e which describes for which standard names ⃗n the sentence φ⃗x ⃗n is believed at level k.

Let φ be an objective formula and KB be proper+. Suppose that n1, . . . , nk, are all the names in φ or in KB, and that n′ is some name that does not appear in φ or in KB. Then RES[k, φ, KB] is defined by:

1. If φ has no free variables, then RES[k, φ, KB] is TRUE, if |=B0KB ⊃Bkφ, and FALSE, otherwise.
2. If x is a free variable in φ, then RES[k, φ, KB] is

For KB = (Teacher(sue) ∨ Teacher(sam)) and φ = Teacher(x) we obtain RES[1, φ, KB] = (x = sam∧FALSE)∨ (x = sue ∧ FALSE) ∨ (x ̸= sam ∧ x ̸= sam ∧ FALSE), which simplifies to FALSE. If instead KB = Teacher(sue) then RES[0, φ, KB] = (x = sue∧TRUE)∨(x ̸= sue∧FALSE), which simplifies to x = sue.

The correctness of our definition of RES is reflected in the following result.

Lemma 3 For any proper+ KB, any objective φ with free variables x1, . . . , xl, and standard names n1, . . . , nl, |= B0KB ⊃ Bkφx1 n1 · · ·xl nl iff |= RES[k, φ, KB]x1 n1 · · ·xl nl .

The proof is by induction on l and closely follows a similar argument in [Levesque, 1984a].

The following definition gives us the means to deal with arbitrary nestings of beliefs.

6 We write TRUE as shorthand for ∀x.(x = x) and FALSE as shorthand for ¬TRUE.

Given a proper+ KB and a basic formula α, ||α||KB is the objective formula defined by

||α||KB = α, when α is objective;

Thus, given our example KB about Sue and Sam, ||∃x.Teacher(x) ∧ ¬B1Teacher(x)||KB results in ∃x.Teacher(x) ∧ ¬FALSE (after simplification), which further simplifies to ∃x.Teacher(x).

Lemma 4 Let s = gnd(KB), α any basic formula with free variables x1, . . . , xl, and n1, . . . , nl standard names. Then s, s, k |= αx1 n1 · · ·xl nl iff s, s, k |= ||α||KB x1 n1 · · ·xl nl

With this lemma it is easy to show that

Since ||α||KB is objective, and together with Theorem 4, we obtain immediately:

Finally, given the decidability result for objective beliefs (Corollary 1) of proper+ KBs and the fact that RES appeals to this decision problem only a finite number of times, we obtain

Corollary 3 For any proper+ KB and basic α, the validity of OKB ⊃ Bkα is decidable in LB.

5 Unknown individuals

Let us now turn to the issue of dealing with unknown individuals such as bestFriendOfSue. For that we augment the language with an infinite set of constants, which are treated as additional terms. The difference between constants and std. names will be that constants can denote different std. names. To simplify matters, we restrict the language for this section to basic formulas without nested beliefs (i.e. similar to SL) and call the new logic LBu .

The semantics needs to be extended to account for the new terms. In the case of a world w, we interpret constants by mapping them into the standard names, e.g., w[a] = #1. We also need to extend clauses and setups. An e-clause is like a clause except that it may contain an ewff e as an additional disjunct. A ground e-clause is an e-clause without free variables, but it may contain constants. An e-setup is a possibly infinite set of ground e-clauses. This allows us, for example, to model knowledge of the kind ∀x.a ̸= x ⊃ T (x) as the infinite e-setup {(a = n) ∨ T(n) | for all std. names n}. Let a cmap ν be a mapping from constants into standard names. We write αν to mean α with every constant a replaced by ν(a). Given an e-setup s, let sν = {cν | {e} ∪ c ∈ s, where |= ¬eν}. In words, sν is a setup containing the clause part of those e-clauses in s with constants replaced by std. names, where e comes out false. For the above example, if ν(a) = #1 then sν = {T (#2), T (#3), . . .}.

The truth of a formula α is now defined wrt. a world w and an e-setup s. Compared to the previous semantics of LB, only Rules 1,2, and 6 need to be changed. Rules 1 and 2 need to deal, in the obvious way, with the denotation of constants as specified by the world w (details omitted). Rule 6 is replaced by the following:

Note that the RHS talks only about setups in the old sense and formulas without constants, that is, we can use the existing semantic rules 8-15 of LB to evaluate its truth value. Validity in LBu is defined as truth in all worlds and e-setups.

We now address the problem of deciding the beliefs of a proper+ KB, where constants are allowed in ∀-clauses. Since we do not deal with nested beliefs, it suffices to consider the validity of formulas of the form B0KB ⊃ Bkφ for objective φ. E.g., let KB = {(P(a) ∨ Q(a), ∀x.x ̸= #1 ⊃ ¬P(x)}, where a is a const. Then |= B0KB ⊃ B0(a ̸= #1 ⊃ Q(a)).

Let gnde (KB) = {{¬eθ} ∪ cθ | ∀(e ⊃ c) ∈ KB}, that is, gnde (KB) is a grounding of KB where the ewffs are kept as part of the resulting e-clauses. We then have

(The proof is similar to an analogous result by LLL for SL.) We then have a result similar to one by De Giacomo et al. [2011] (Theorem 5) for proper KBs with unknowns:

Theorem 6 Let s = gnde (KB). Let a1, . . . , am be the constants in KB and φ. Let H be the set of those c-maps ν s.t. ν(a1) ranges over all std. names in KB and φ plus one more, and for all 1 ≤ i < m, ν(ai+1) ranges over all names that ν(ai) ranges over plus one more. Then for all ν, sν, sν, k |= φν iff for all ν ∈ H, sν, sν, k |= φν.

This result establishes that finitely many substitutions of constants by std. names suffice to determine the beliefs of a KB. Using Lemma 5 and the fact that gnde (KB)ν = gnd(KBν) we then obtain

Theorem 7 Let KB, φ,H be as in the previous theorem. |=B0 ⊃Bkφ iff |=SL B0KBν ⊃Bkφν for all ν ∈ H.

Note that this reduces the problem of determining the beliefs of a KB with unknown individuals to a finite number of decidable validity problems in SL. Hence

Corollary 4 For any proper+ KB and objective φ, the validity of B0KB ⊃ Bkφ is decidable in LBu .

6 Conclusions

The paper has established that the decidable reasoning service for proper+ KBs proposed by LLL can be faithfully extended to deal with introspection. Moreover, unknown individuals can also be accommodated without sacrificing decidability. As for future work, an immediate task is to combine the results on introspection and unknown individuals. Besides decidability it will also be interesting to identify special cases where reasoning remains tractable for a fixed k. Finally, going beyond constants and allowing function symbols in some way is yet another challenge.