From Logic Programming Semantics to the Consistency of Syntactical Treatments of Knowledge and Belief

1 Introduction

The approach most often used in constructing formal theo­ ries for reasoning about multiagent systems is to formalise the agents' beliefs and knowledge through modal opera­ tors. An alternative approach is to formalise these proposi­ tional attitudes as predicates of a first-order predicate logic. This has several advantages, which have been widely dis­ cussed in the literature [Davies, 1990; Attardi and Simi, 1995; Carlucci Aiello eta!. , 1995; McCarthy, 1997; Grant eta!., 2000]. Most importantly, it allows us to quantify over the propositional objects of knowledge and belief as for instance in "agent 1 believes that everything known by agent 2 is also known by agent 1 ", formalised by

This formula has no counterpart in the classical modal op­ erator approach, since if K1 and K2 were modal operators, we would not be able to apply them directly to the variable x (modal operators only apply to well-formed formulas). Thus the predicate approach gives us more expressive power and the ability of agents to refer to the totality of their own and others beliefs, which is important in meta-reasoning.

Unfortunately, the predicate approach easily becomes in­ consistent, since the added expressive power allows the agents to express self-referential beliefs that in some cases turn out to be paradoxical. This was proved by Montague [1963] and Thomason [1980]. They prove that certain axiom schemes describing natural properties of knowledge and be­ lief are inconsistent with formal arithmetic. Their results are reviewed in Section 3. Des Rivieres & Levesque [1988] and Morreau & Kraus [1998] have shown there to be a way out of these inconsistency results: to suitably restrict the set of sen­ tences that we instantiate our axiom schemes of knowledge and belief with. These results are reviewed in Section 3 as well.

In this paper we will show that the results of des Rivieres, Levesque, Morreau and Kraus can be reduced to well-known results in logic programming semantics. This is carried out in Section 4. In Section 5 we give a strengthening of their results, using again the connection to logic programming se­ mantics.

2 Terminology and Notation

We will be using theories of first-order predicate logic to for­ malise propositional attitudes of agents. To prove the consis­ tency of these first-order theories, we use results from logic programming semantics. Below we introduce the kinds of logic programs and first-order languages we will be consider­ ing.

2.1 Logic Programs

All logic programs considered in this paper will be proposi­ tional. Thus, an atom is simply a propositional letter, and a literal is either a propositional letter p or its negation ·p. We take the symbols true and false to be among our propo­ sitional letters with the obvious intended interpretation. A clause is a formula of propositional logic on the form

where H is an atom, n ;:::: 1 and all Li are literals. A proposi­ tional program (or simply a program) is a (possibly infinite) set of clauses. Herbrand models of programs are defined in the usual way. We require that all models assign the truth­ value true to the propositional letter true and false to false.

Given a program P, comp(P) denotes its Clark comple­ tion. Since we work only with propositional programs, the Clark completion is particularly simple. The Clark comple­ tion of P is the following set of equivalences in infinitary propositional logic: for each atom A in P,

• if A does not appear as head of any clause in P, then A f-f false E comp(P) .
• otherwise we have A f-f v iE/ Bi E comp(P) , where {A ,__ Bi I i E I} is the set of clauses in P with head A.

Let P be a propositional program. The dependency graph of P is the directed graph with signed edges defined as fol­ lows. The nodes of the graph are the atoms (propositional letters) occurring in P excluding the special atoms true and false. There is a positive edge from A to B , denoted by (A, B, +), if and only if there is a clause A ,__ L1 1\ · · · 1\ Ln in P such that Li = B for some 1 ::; i ::; n. If Li = --,B then there is a negative edge from A to B, denoted (A, B, - ). We say that A depends on B, denoted by A < B, if there is a proper path from A to B in the graph. We say that A depends negatively on B, denoted by A <1 B, if there is a path from A to B containing at least one negative edge. A program P is called locally stratified if the relation < 1 in the dependency graph of Pis well-founded.

2.2 First-Order Languages

We use L to range over languages of first-order predicate logic. We take the connectives of first-order logic to be ', 1\ and 3. When using V, --t , f-f and V in formulas, these formu­ las are simply abbreviations of formulas containing only--, , 1\ and 3. We require all languages L to contain the one-place predicate symbols T and P . P will be used as a predicate that picks out a set of (codes of) formulas in L. Twill, de­ pending on the context, be used to express one of our syntac­ tic attitudes belief or knowledge. By L- {T} we denote the language L with the predicate symbol T removed. We will assume that all considered languages contain a parametrised coding. By a parametrised coding in L we understand an injective map r ·.., from the formulas of L into the terms of L satisfying:

• (i) For any formula <p in L, the term r <p.., has the same free variables as r.p (but r r.p 1 is not itself a variable).
• (ii) For any formula <p(x) inLand any term T which is free for x in <p(x ), r <p(T)' is the term obtained by substitut­ ing T for all free occurrences of x in r <p( x )..,.
• (iii) The coding is well-founded, that is, there is no infinite sequence of formulas <p0 , <p1 , <p2 . . . such that r <pi+1 .., is a term in 'Pi for all i E .N.

We refer to [Feferman, 1984] for the construction of a parametrised coding. Feferman's coding does not satisfy (ii), but a simple variant of it will. r <p .., is called the code of r.p. The intended interpretation of a formula T( <p ') is that " <p is known" or "r.p is believed". We assume all first-order languages L to contain the language of Peano arithmetic. Throughout the paper, by formal arithmetic we mean Robin­ son's arithmetic, though any other standard formalisation of arithmetic could have been used in its place. We identify first­ order languages L with their sets of sentences. By a sentence in L we understand a closed formula, that is, a formula with­ out any occurrences of free variables. The set of ground terms of L is denoted Terms( L) .

To avoid confusion between formulas of propositional pro­ grams and formulas of first-order languages we will use Latin letters for the former and Greek letters for the latter .

2.3 Regular Formulas and RPQ Formulas

We now define the sets of first-order sentences which we in­ tend to prove that our axiom schemes of knowledge and belief can consistently be instantiated with.

Definition 1. Let L be a first-order language. The set of reg­ ular formulas of L is the least set satisfying:

• (i) Any atomic formula of L- {T} is a regular formula.
• (ii) If r.p and 'lj; are regular formulas and x is a variable, then r.p 1\ 'lj;, ' 'P and 3x<p are regular formulas.
• (iii) If <p is a regular formula then T(r <p ') is a regular for­ mula.

Our definition differs slightly from the one given by Mor­ reau and Kraus [ 1998]. Instead of using a parametrised cod­ ing, they have an ( n + 1 )-place predicate symbol rn for each n, such that instead of writing T( <p(x 1. ... , Xn )'), where x1 , . .. , Xn are the free variables of <p, they would be writing Tn( <p ', X1, ... , Xn ) where r. 1 is then a stan­ dard (non-parametrised) Godel coding. To simplify matters, we have chosen to take care of the free variables by using a parametrised coding rather than by introducing infinitely many predicate symbols of different arities.

As an example of a regular formula we have, for a suitable choice of L ,

expressing that the agent knows Mike's telephone number. If we have more than one agent, we can of course introduce a predicate symbol Ti for each agent i . In that case the follow­ ing sentence also becomes regular:

expressing that agent 1 believes agent 2 to have correct beliefs about the departure time of the train. As an example of a non­ regular formula we have

expressing that the user believes that the system only utters what it believes to be the case. It is non-regular because Tsystem is applied directly to a variable and not to the code of a formula. To allow expressing beliefs such as this one, Mor­ reau and Kraus [ 1998] extended the set of regular formulas to a more inclusive class called the RPQ formulas.

Definition 2. Let L be a first-order language. The set ofRPQ formulas of L is the least set satisfying:

• (i) Any atomic formula of L- {T} is an RPQformula.
• (ii} If cp and 1/J are RPQ formulas and x is a variable, then cp 1\ 1/J, ''P and 3xcp are RPQformulas.
• (iii} If cp is an RPQformula then T( cp ') is an RPQformula.
• (iv) If cp is any formula in L, then 3x (P(x) 1\ cp) is an RPQ formula.

This definition also differs from the one given by Morreau and Kraus [ 1998]. It defines a slightly more inclusive set of formulas, and at the same time it is simpler, since it avoids Morreau and Kraus' use of two distinct collections of vari­ ables.

By regular sentence we understand a closed regular for­ mula, and by RPQ sentence a closed RPQ formula.

3 Review of Previous Results

Consider the following axiom schemes in a first-order lan­ guage L:

• AI. T( cp ') ---+ cp

• A4. T( cp '), if cp is a theorem in formal arithmetic.

As already mentioned, T(' cp ') is intended to denote either "cp is known" or "cp is believed". Thus, for instance, the first axiom scheme expresses that everything known (believed) is true. It seems reasonable to characterise knowledge by the ax­ iom schemes A1-A4 and beliefby A2-A6. But the following theorem shows that this is not always possible.

Theorem 3 (Montague [1963), Thomason [1980)). Let L be a first-order language. Formal arithmetic extended with any of the following sets of axioms is inconsistent.

• (a) The axiom schemes of knowledge, Al-A4, instantiated over the sentences of L.
• (b) The axiom schemes of belief, A2-A6, instantiated over the sentences of L.

The inconsistency of (a) is Montague's result, and the in­ consistency of (b) is Thomason's result. A way out of these inconsistency results is to restrict the set of sentences that we instantiate AI-A6 with. This strategy gives us the following positive results.

Theorem 4 (des Rivieres and Levesque (1988)). Let L be a first-order language. Formal arithmetic extended with any of the following sets of axioms is consistent.

• (a) The axiom schemes of knowledge, Al-A4, instantiated over the regular sentences of L.
• (b) The axiom schemes of belief, A2-A6, instantiated over the regular sentences of L.

Theorem 5 (Morreau and Kraus (1998)). Theorem 4 still holds when we replace "regular sentences " with "RPQ sen­ tences".

Theorem 4 is proved in [des Rivieres and Levesque, 1988] by a careful translation from a corresponding first-order modal logic. Theorem 5 is proved in [Morreau and Kraus, 1998] by a similar translation from a corresponding second­ order modal logic. In the following section we give proofs of their results taking a completely different route. We show that the problems can be reduced to problems of consistency of particular logic programs.

Instead of working directly with the axiom schemes A I­ A6, we will most of the time be working with the truth scheme which is the following axiom scheme:

This is often sufficient since, as the following lemma shows, instances of axiom schemes A I-A6 are logical consequences of corresponding instances of the truth scheme. To prove that the axiom schemes AI-A6 instantiated over a set of sentences S are consistent, it thus suffices to prove the consistency of the truth schema instantiated over that same set.

Lemma 6. Let L be a first-order language, and letS be a set of sentences in L satisfying:

if cp and 1/J are in S then T(' cp '), ''P and cp 1\ 1/J are in S.

Let M be a model of L in which T(' cp ') ~ cp holds for all cp inS. Then all of Al-A6 hold in Mfor all cp, 1/J inS.

Proof That AI holds in M when cp is in S is a trivial con­ sequence of the fact that T( cp ') ~ cp holds in M . To see that A2 holds in M, we first note that if cp is in S then -, (T( cp ') 1\ ''P) is in S as well, by assumption on S. This sentence is an abbreviation ofT( cp ') ---+ cp, so we get that the following instance of the truth schema holds in M:

Using this together with the fact that AI holds in M, we get that T('T( cp ') ---+ cp ')holds in M. That is, A2 holds in M . A3-A6 are proved to hold in M in a similar manner. D

4 From LP Semantics to Consistent Treatments of Knowledge and Belief

The results of this paper are based on the following lemma.

Lemma 7 (Przymusinski (1987), Sato (1990]). If a pro­ gram P is locally stratified then comp(P) has a Herbrand model.

Our formulation is taken from [Sato, 1990]. It should be noted that Sato is not considering infinite programs in his pa­ per, but his proof carries over without modification to this more general framework. This is because Sato is consider­ ing the set of ground instances of non-propositional programs rather than these programs themselves. The set of ground in­ stances of a finite non-propositional program is in general an infinite propositional program, that is, the kind of logic pro­ gram we are considering in this paper.

Definition 8. Let L be a first-order language, and let S be a set of sentences in L. We define an infinite program PL,S as follows. For every sentence cp in L, the program PL,S contains a propositional atom denoted p'P. The clauses of PL,S are given by:

The relation between models of the program PL,s and models of the first-order language Lis given by the following lemma.

Lemma 9. Let L and S be as above. If comp( PL,S) has a Herbrand model M then L has a Herbrand model N satisfy­ ing:

• (i) For every sentence cp in L,

Proof Assume M is a model ofcomp(PL,s). comp(PL,s) is the following set of equivalences:

Let N be the following Herbrand model of L:

(i) is proved by induction on the syntactic complexity of cp. If cp is an atom then (1) holds by definition of N. To prove (1) for sentences of the form cp 1\ '1/J, ·cp and 3xcp(x) we simply use (2), (3) and (4), respectively. For the case of ·cp the proof is:

where the first equivalence is by (3) and the third is by induc­ tion hypothesis. The two remaining cases are proved simi­ larly. Thus (i) holds. Furthermore, using (i) and (5), we get for all cp E S:

Lemma 10. Let L be a first-order language and let R be the set of regular sentences in L. The propositional program PL,R is locally stratified.

Proof To simplify matters we will throughout this proof be identifying every propositional letter p'P with the correspond­ ing first-order sentence cp in L. It should always be clear from the context whether cp is used to denote the first-order sen­ tence or the corresponding propositional letter. Thus, by the identification, the nodes of the dependency grapL of PL Rare all sentences in L. The edges are: '

• (cp 1\ '1/J, cp, +)and (cp 1\ '1/J, '1/J, +),for all cp, '1/J E L.
• (·cp, cp,- ), for all cp E L.
• (3xa(x), a(T), +), for3xa(x) ELand T E Terms(L) .
• (T(r cp '), cp, +),for all cp E R.

Edges of the first type are called /\-edges, edges of the second type are called ·-edges, edges of the third type are called 3edges and edges of the last type T-edges.

We have to prove that PL,R is locally stratified. Actually, we will be proving something slightly stronger. We will prove that the relation < in the dependency graph of PL,R is well­ founded. That is, we will prove that there does not exist any path of infinite length in the graph. Assume the opposite, that is, assume the existence of an infinite path u.

Claim. u contains infinitely many T-edges.

Proof of claim. Assume the opposite. Then there will be an infinite subpath u' of u containing no T-edges. Thus all edges on u' must be /\-, ·- or 3-edges. But note that for any such edge, the start node will have higher syntactic complex­ ity than the end node. Thus, along u' the syntactic complexity will be strictly decreasing, which contradicts u' being infinite. This proves the claim. 0

With every formula cp in L we now associate a natural num­ ber d(cp), called the T-degree of cp. The T-degree is defined recursively by

• d(cp) = 1 + d('lj;), ifcp = T('lj;') for some '1/J.
• d( cp) = 0, if cp is any other atomic formula.
• d( cp) = max{ d( '1/J) I '1/J is a subformula of cp}, otherwise.

The well-foundedness of the parametrised coding ensures that d is well-defined. By the above claim, u contains an infinite number ofT-edges. Let cp be the end node of such an edge. Then cp is regular. Let u' be the infinite subpath of u having cp as its start node. Then every node on u' must be a regular formula ( c.f. the definition of a regular formula). This implies that every edge on u' is

• (i) either a/\-, ·- or T-edge,
• (ii) or of type (3xa(x), a(T), +),where a(x) does not contain T(x) as a subformula.

Item (ii) follows from that fact that when x is a variable then T(x) is not a regular formula, and therefore no formula hav­ ing T(x) as a subformula can be regular either. Now note that on any edge of type (i) or (ii), the T-degree of the end node will be less than or equal to the T -degree of the start node. Thus the T -degree will be monotonically decreasing along u' and must therefore be constant from some point. But then from this point it can not contain any T -edges, since the T -degree of the end node of such an edge is always one less than the T -degree of the start node. This contradicts the claim ~~. 0

Lemma 11. Let L be a first-order language and let S be a set of sentences in L. If PL,S is locally stratified then any Herb rand model of L-{T} can be expanded into a Herb rand model of L in which T(r cp ') f--7 cp holds for all cp in S.

Proof Let M denote a Herbrand model of L- {T}. Let P be the program PL,s extended with the following clauses:

PL ,S is assumed to be locally stratified, and since P has the same dependency graph as PL,s, then P must be lo­ cally stratified as well. Therefore comp(P) has a Herbrand model M', by Lemma 7. Finally, Lemma 9 gives us the exis­ tence of a Herbrand model N of L in which the equivalences T( cp ') ....,. cp hold for all cp in S. To see that N expands M we just have to note that if cp is an atom in L - {T} then

M f= 'P =} p'P +- true E P =} M' f= p'P =} N f= 'P and

M f= ''P =} p'P +- false E P =} M' f= 'P'P =} N f= ·tp, where the last implications are by (i) in Lemma 9. D

Theorem 12. Let L be a first-order language and let U be a theory in L- {T} containing formal arithmetic. !JUhas a Herbrand model then U extended with any of the following sets of axioms has a Herbrand model.

• (i) The axiom scheme T( cp ') ....,. cp instantiated over the regular sentences of L.
• (ii) The axiom schemes of knowledge, Al-A4, instantiated over the regular sentences of L.
• (iii) The axiom schemes of belief, A2-A6, instantiated over the regular sentences of L.

Proof Assume U has a Herbrand model M. Let R denote the set of regular sentences in L. By Lemma 10, PL,R is locally stratified. So by Lemma 11, M can be expanded into a Herb rand model N in which T( cp ') ....,. cp holds for all regular cp. This proves (i). (ii) and (iii) then immediately follow, using Lemma 6. D

Theorem 4 is an immediate consequence of Theorem 12, when taking U to be formal arithmetic. The machinery we have introduced can also be applied to prove Theorem 5. It is an immediate consequence of the following corollary to The­ orem 12.

Corollary 13. Theorem 12 still holds when we replace "reg­ ular sentences " with "RPQ sentences". Furthermore, the ex­ tension ofP in the Herbrand model constructed will be the set of codes of regular sentences.

Proof Let S denote the set of RPQ sentences of L. Modify the program PL,s by removing every clause of the form

where T is not the code of any regular sentence. Call the new program Q L,S. It is easy to see that Q L,S is locally strat­ ified, using the argument given in the proof of Lemma 10. Lemma 11 still holds when we use QL,S instead of PL,s, so any Herbrand model of U can be expanded into a model of L in which T( cp ') ....,. cp holds for all RPQ sentences. This proves (i) in Theorem 12 with "regular sentences" replaced by "RPQ sentences". (ii) and (iii) then follows from Lemma 6. D

5 Strengthening the Results

We now strengthen the results obtained above. We want to define a set offormulas more inclusive than the RPQ formulas that the truth scheme T( cp ') ....,. cp can safely be instantiated with. For this we need a couple of new definitions.

Definition 14. Let L be a first-order language and let cp be a formula in L. The set of formulas occurring in cp is defined as the least set containing cp and satisfying:

• If /3 is a subformula of a formula a occuring in cp, then /3 is occuring in cp.
• !JT( a') is occurring in cp, then a is occurring in cp.

Assume '!j; is a formula occurring in cp. The occurrence is said to be negative if '!j; occurs in a formula a where ·a occurs in cp. Otherwise the occurrence is called positive. An occurence of '!j; in tp is said to be protected if '!j; occurs in a formula a where :Jx (P(x ) 1\ a) occurs in cp.

Thus, for instance, cp occurs in formulas such as T( cp ') 1\ · '1/J and T( ·T( cp ') 1\ '!j; ') but not in A( cp ') when A =f. T. cp has positive occurrence in T( cp ') 1\ ·'1/J but negative occurrence in T( ·T( cp ') 1\ 7/J ').

Definition 15. Let L be a first-order language. A formula cp in L is said to be weakly RPQ if, for any variable x, the formula T(x) only occurs positively or protected in cp.

Note that in an RPQ formula, every occurrence ofT(x) for some variable x is protected, so every RPQ formula is also weakly RPQ. Thus the set of RPQ formulas is a subset of the set of weakly RPQ formulas. It is furthermore a proper subset, since among the weakly RPQ formulas we have e.g. :Jx(aboutJove(x) 1\T(x)), which is not RPQ. The previously obtained results can be extended to the weakly RPQ formulas.

Theorem 16. Let L be a first-order language and let U be a theory in L- {T}. IfU has a Herbrand model, then U extended with the axiom scheme

instantiated over the set of weakly RPQ sentences has a Her­ brand model.

Proof Let S denote the set of weakly RPQ formulas. Us­ ing Lemma 11, it suffices to prove that PL,S is locally strat­ ified. As in the proof of Corollary 13, we can consider the modified program QL,S instead. To obtain a contradiction, assume QL,S is not locally stratified. Then <1 in the depen­ dency graph of Q L,s is not well-founded, that is, there must exist an infinite path a containing infinitely many negative edges. As in the proof of Lemma 10, we get that a must con­ tain infinitely many T-edges. Let cp be the end node of such an edge. Then cp is weakly RPQ. Let a' be the infinite sub­ path of a having this node as its start node. Then every node on a' must be weakly RPQ. As noted in the proof of Lemma 10, if every edge on a' is

• (i) either a/\-, ·- or T-edge,
• (ii) or of type (:Jxa( x), a( T), +) where a( x) does not con­ tain T(x) as a subformula,

then u' can not be infinite. Thus, every node on u' must have an occurrence ofT(x ) for some variable x. Since all nodes are weakly RPQ, in each of these T( x) is either positive or protected. But ifT(x) occurs protected in <p, there can be no infinite path starting at <p. Thus, in every formula <p on u', T(x ) must occur positively (for some variable x). But this implies that all edges in the path are positive, which contra­ dicts our assumption. 0

The above theorem also relates to a result by Pedis [1985]. Perl is showed that a modified truth scheme T( <p ') ,__. <p* is consistent with arithmetic. It is easily seen that the set of instances of the (unmodified) truth scheme shown to be con­ sistent by Pedis' result is contained in the set of instances shown to be consistent by Theorem 16.

In view of the results by Montague and Thomason (Theo­ rem 3), there is a limit to how many instances of our axiom schemes we can add while still retaining consistency. The set of weakly RPQ sentences is quite close to this limit, as is made clear by the following example.

Example. Let L be a first-order language containing three one-place predicate symbols A, P and T. One of the simplest examples of a formula which is not weakly RPQ in L is the formula 3x (A(x) 1\ -,T(x)) . Let us call this formula '1/J. In '1/J, T(x) occurs negatively and unprotected (since A =/:- P). Let U be the theory consisting of the following axioms

U obviously has a Herbrand model M, but we will show that U extended with the single axiom

does not have a Herbrand model. This shows that Theorem 16 no longer holds if we to the weakly RPQ sentences add a sentence such as '1/J . Assume, to obtain a contradiction, that there exists a Herbrand model N in which all of (6), (7) and (8) holds. Then we obtain the following contradiction:

6 Conclusion

We have been showing that results on the consistency of the predicate approach to knowledge and belief can be proved through the use of well-known results from logic program­ ming semantics. This connects the two research fields in a new and interesting way, and have furthermore allowed us to strengthen the previously known results on the consistency of the predicate approach. It is expected that the connection be­ tween the two fields can be pursued further to get even better consistency results. This might be done by using some of the results from the literature on logic programming semantics that strengthen Lemma 7.

Acknowledgments

I would like to thank the following persons for guiding me in the direction that led to this paper: J0rgen Fischer Nilsson, Mai Gehrke, Joao Alexandre Leite and Ken Satoh. Special thanks to Roy Dyckhoff for his interest in my work and his many valuable comments.