Belief, Awareness, and Two-Dimensional Logic

1 Introduction

There has been a long story in philosophy to find a suitable semantics for logics of knowledge and belief since the twen­ tieth century. The subject was picked up by researchers in the area of artificial intelligence, in which human reasoning or resource-bounded agents reasoning is considered.

The standard approach for characterizing knowledge and belief is based on the possible-worlds model. The intuitive idea which was discovered and labelled by Hintikka [Hin­ tikk~, 1962], is that an agent considers a number of situations as possible. Under this interpretation, an agent is said to be­ lieve a fact if it is true in all the states that the agent regards as possible. Thus belief is modelled by means of accessibil­ ity relations as they are present in possible worlds models. The model is a structure M of the form (S, 1r, R1, ... , Rn), where S is the set of all worlds, 1r is the truth assignment for every atom and every world, and R;, i = 1, . .. , n, are the binary relations inS.

On the basis of the possible worlds model a logic of be­ lief can be devised. To this end, introduce modal operators L1 , . .. , Ln, L; to be interpreted as "the agent i believes that", and give them formal semantics by a clause: M, s f= L;cp if and only if for each world t such that R;(s, t) it holds that M, t f= cp. To complete the logic, assume that, besides propo­ sitional atoms, formulas can also be composed by means of the usual propositional connectives""', 1\, V, ->,and...-..

· Authors were supported in part by the logical structure of cogni­ tion in open worlds project grant under ministry of education, China grant 2000DXM720.40002.

1 Corresponding author. E-mail address: hssjse@zsu.edu.cn

In order to be sure that certain properties that intuitively hold of belief are valid in this setting, some constraints should be put on the accessibility relation R ;. The standard way to do that is requiring that R; be serial, transitive, and Eu­ clidean. From these constraints, three intuitive properties of belief can be captured: consistency, positive introspection, and negative introspection (they are reflected as the below ax­ ioms A5, A3, and A4 respectively).

This notion of belief is completely characterized by the following sound and complete axiom system, traditionally called KD45.

AI: All tautologies of propositional logic

A2: L;(cp -> '¢) -> (L;cp-> L;'¢) A3: L;cp-> L;L;cp A4: ""' L;cp -> L; ""' L;cp AS: ""'L;(cpl\ ""'cp) Rl: cp, 'P-> '1/JN

R2: cpj L;cp

Modelling knowledge and belief of this kind yields what Hintikka called logical omniscience. Logical omniscience presupposes that an agent's beliefs are closed under logical consequence. Furthermore, valid sentences are alwa7s be­ lieved. It is clear that rational agents can never be so mtelh­ gent that they become omniscient.

To avoid these undesired properties, something non­ standard is needed. In the literature there appear quite anum­ ber of drastically varying approaches. Of these, of particular interest to us is awareness logic.

A number of ways of modelling awareness and actual be­ lief have been suggested in the literature, among them we would like to refer to [Rantala, 1982], [Fagin and Halpern, 1988], [Wansing, 1990] and [Thijsse, 1996].

The main problem of logical omniscience is that it forces an agent to believe too much. Fagin and Halpern suggested a variation of the standard Kripke model [Fagin and Halpern, 1988], named the logic of general awareness (abbreviated GAL). The underlying idea is to use awareness as a "sieve" to remove the undesired parts of the logic. Though an agent im­ plicitly believes a fact, the agent may not believe it explicitly if it is not aware of it. GAL distinguishes between implicit belief and explicit belief by the following equation:

Explicit Belief= Implicit Belief+ Awareness

The model is endowed with function Ai that act as a kind of sieve, filtering out explicit beliefs from the bulk of implicit beliefs. The model is a tuple M of the form (S,1T,Rl,---,Rn,Al,-·-,An), where S, 1T, and R1 , . .. , Rn have their usual meanings. For each possible worlds, Ai(s) is an arbitrary set of formulas of the language, indicating the formulas that the agent i is aware of in s.

The language contains operators A1 , . .. , An, which reflect awareness, as well as the implicit belief operators £ 1 , ... , Ln and explicit belief operators B1 , ... , Bn.

The semantics of the language is as usual, except for adding two clauses for the operators Ai and Bi. Note that the one for Ai is not expressed recursively.

• M, sf= Airp iff rp E Ai(s);
• M, sf= Birp iff rp E Ai(s) and M, s f= Lirp.

The explicit beliefs are just those implicit beliefs that belong to the awareness set. The sentence

is valid in the model. Fagin and Halpern showed in [Fagin and Halpern, 1988] that by adding A6 to KD45, the resultant system completely characterize the semantics of GAL.

GAL, despite its simplicity, is a very flexible and powerful tool. Wansing exhibited in [Wansing, I 990] that a slight gen­ eralization of GAL (Let Ri be any binary relation in S) can characterize every modal system that contains classical logic.

GAL has also some disadvantages. Useful information is neglected in this semantics. There are two reasons that com­ mit an agent not to explicitly believe a sentence rp: one is that the agent is not aware of rp; the other is that the agent does not implicitly believe rp. GAL cannot express these different situations. Even if we know the fact that an agent does not explicitly believe a sentence, we still do not know where it comes from. In our proposal, the difference between them is able to be distinguished.

In GAL, it is possible for a sentence to be true even if the agent is not aware of some parts of the sentence. For example, consider the sentence "if an agent believes that it rains, it will take an umbrella." (formalized as Birp -+ 'lj;). The sentence can be true in a world s even if the agent is not aware of anything about "rain" in s. In a different opinion of belief and awareness, it may be argue that the above sentence seems nonsensical to the agent if it does not know what the "rain" is. From that opinion, the sentence can never be simply true. We will introduce a method such that different opinions of belief and awareness can be easily modelled.

It is important to distinguish between objective truth and subjective truth. It is reasonable for the above sentence to be objective true (as a truth of fact), but not subjective true (from the point of view of the agent). We leave the item aside for the moment. We will present two logics below. The first logic only concern about subjective truth. The notion will be picked up in the second logic.

We use a different way to add awareness sieve to doxas­ tic logics. What we use is two-dimensional logics. In two­ dimensional logics, the value of a formula rp ranges over the set {(1, 1), (0, 1), (1, 0), (0, 0)} . Each member of the set is called a truth-degree. Every truth degree has two dimen­ sions. Intuitively, the first dimension of a truth-degree, called a truth-value, represents the truth value of rp and the second, called an awareness-value, keeps track of the value of the awareness condition (we will clarify the notion below) of rp. Though the logic looks like a type of four-valued logic, it is in fact two-valued. Whichever way it is read, we are still left with two-values, with 1 as true and 0 as false.

We got the idea of using two-dimensional logics in this way from theoretical linguistics, where two-dimensional log­ ics are used to give the semantic concept of presupposition [Bergmann, 1991]. Usually, the sentence "a exists" is looked upon as the presupposition of the sentence "a is P". We in­ terpret "an agent is aware of rp" as "rp exists in the agent's memory". And then we treat the sentence as the presuppo­ sition of the sentence "the agent explicitly believe rp". Here the presupposition is indeed the existence of a denotation of rp in the agent's memory. We call it the awareness condition. The denotation is subjective. It denotes things in the given memory, unlike in the case of the sentence "a exists", whose usual meaning is that a has an objective denotation. Another difference between them is that the subjective denotation is a denotation of a sentence other than a denotation of a term.

Two-dimensional logics allow us to calculate the truth value of a sentence and its awareness condition indepen­ dently. This gives us flexibility to construct different mod­ els of actual belief. Intuitively, the awareness condition of a sentence should affect its truth value. However, it may be no agreement on what the effect should be. By amending its matrices, two-dimensional logics are flexible enough to char­ acterize different concepts of actual belief.

It is easy to see that GAL can be represented by a two­ dimensional logic. The only thing we need to do is to make the awareness condition of a sentence does not disturb its truth value.

We would like to emphasize again that what we present in this paper is not only a more rigorous concept of actual belief than GAL's, but also a method by which different opinions to actual belief can be modelled readily. We will give two doxastic logics use two-dimensional logics in the rest of the paper. The first logic can be viewed as an example of using our method, in which a more limited concept of actual be­ lief is presented. The second logic extend the first logic to a hybrid system.

To be concise, we only consider one agent mode and use operators B, L, A substitute for Bi, Li, Ai respectively. It is easy to extend the results of the paper to multi-agent mode.

We think many-dimensional logics may play an important role in may topics. The problems in many topics are in the following style: There are several factors that affect the out­ come event's situation. To construct a logical structure of such problem, many-dimensional logics are preferred. Each factor or outcome is put in a different dimension of the truth degree. In such a many-dimensional semantics, it can be clearly indicated that how the factors affect the outcome. Of course, it is an "out of focus" topic in the present paper.

By the way, we got some ideas of this paper from our work on "Open Worlds". Interested readers may refer to [Shier and Hu, 2001].

2 Two-Dimensional Awareness Logics

2.1 Semantics

By awareness different people can understand in quite differ­ ent ways. In this section, we present a logic in which a sen­ tence's awareness condition is considered as a very rigorous limitation to the sentence: If the awareness condition is not satisfied, then the sentence is nonsensical to the agent and is invariably false. We call the resultant logic two-dimensional awareness logic, abbreviated TDAL.

The language of TDAL is the same as GAL's. A TDAL model is a tuple M = (S, 1r, R, A), where,

• S is a non-empty set of possible worlds;
• 1r is a truth degree assignment function from the set of atoms to {(1, 1), (0, l)} per possible world. By conven­ tion, the parentheses and commas of truth degrees are dropped;
• R ~ S X S is a binary relation that is serial, transitive, and Euclidean;
• A is the awareness function, assigning each possible world a set of formulas.

The matrices are:

Notice that V and 1\ can be defined from "' and ~. The latter two connectives are considered as primary.

The truth degree conditions for the modal operators are:

• 1r(s, A<p) = 11 if <p E A(s); otherwise, 1r(s, A<p) = 01.
• 1r(s,Lt.p) = 11if7r(t,<p) = 11or1r(t,<p) = 10forallt such that (s, t) E R; otherwise, 1r(s, L<p) = 01.
• 1r(s,B<p) = 11 if1r(s,A<p) = 11 and1r(s,L<p) = 11; 1r(s,B<p) = 01 if1r(s,A<p) = 11 and1r(s, L<p) = 01; 1r( s, B<p) = 00 if 1r( s, A<p) = 01.

<p is satisfied ins if and only if1r(s, <p)=l1, denoted by M , s f= <p. <p is valid if and only if M, s f= <p for every model M and every possible world s, denoted by f= <p.

The semantics of TDAL needs some explanations. The as­ signment function 1r is indeed two-valued. It assigns only two values, 11 and 01, to each atom. The primary awareness­ value is always assigned as 1. Only an occurrence of the B operator can introduce falseness as awareness-value. The reason is this: The awareness condition only makes sense when explicit belief is considered. An atom has no aware­ ness condition at all. It is natural to assign atoms a trivial awareness-value, i.e. an always true value. It is easy to see that this definition is sound: an always true awareness-value does not disturb the calculation of truth value. This also ex­ plains the semantic definition of A and L operators, where the awareness-value of each formula of the form A<p or L<p is always true.

Awareness-value is contagious: the awareness-value of a sentence governed by one of the binary connectives is false if the awareness-value of one of its immediate components is false. If the awareness-value is always true, the truth-value is calculated classically.

Clearly, TDAL is along skeptical lines. It characterizes a cautious agent: the agent deems a sentence to be true only if every propositional part of it has no uncertainty.

Note that the semantics ofTDAL can be reduced to a three­ valued logic because the truth degree 10 can never result, nei­ ther from logical connectives nor from modal operators. 10 can be dropped safely from the matrices. At first sight, the resulting three-valued propositional logic looks the same as weak Kleene logic. If we substitute the truth values t,f and u for the truth degrees 11, 0 l and 00 respectively, then we get the matrices of weak Kleene logic. However, the two logics are quite different. In TDAL, the assignment function is in­ deed two-valued, unlike Kleene's. 00 can only result from ap­ plication of the modal operator B. This characteristic makes TDAL very different than weak Kleene logic. For example, there are no propositional tautologies in weak Kleene logics, but in TDAL, some of them are preserved.

2.2 Discussion And Formalization

Definition 2.1 An occurrence of a B operator in a formula <p is bound if that occurrence is in the scope of one of the modal operators; otherwise, such an occurrence of B is free. A formula <p is bound iff each occurrence in it of B is bound, and <p is free iff it is not bound.

Some classical tautologies are not valid in TDAL. A limi­ tation is required in order to make them valid.

Proposition 2.2 The following sentences are valid in TDAL.

(A 7) all bound classical tautologies.

Proof Trivial. 0

The next proposition shows that the axioms with respect to the properties of implicit belief are all preserved in TDAL, as they should be.

Proposition 2.3 A2-A5 are all valid in TDAL.

Proof The proof is as usual. 0

Intuitively, the axiom A6, which characterize explicit be­ lief, should not hold in TDAL because we have a different view to awareness condition here. It is just the case. This is easy to see by taking a model that contains a worlds s such that the agent is not aware of <p ins. Instead of A6, we have the following axioms and rules to characterize properties of explicit belief.

We use cp* to denote the formula obtained from 'P by sub­ stituting A¢1\L¢ for all free occurrences of B¢ in tp. Clearly, cp* is bound.

Proposition 2.4 The following sentences and rules are all valid in TDAL:

• (R3) A¢1 , ... , A¢n I 'P .--. cp*, where for all free occurrences of B¢ in cp, A¢ E {A¢1, ... , A¢n}·
• (R4) 'PI A¢, where B¢ occurs free in cp.
• (A8) (LA¢11\ ... /\LA¢n)--> L(cp <--> cp*), whereforallfree occurrences of B¢ in tp, A¢ E {A¢1, ... , A¢n}.
• (A9) Lcp--> LA¢, where B¢ occurs free in cp.

Proof The proof is as usual. D

These sentences are quite intuitive to the semantics of TDAL. The system corresponding to the semantics of TDAL consists of axioms A2-A5, A 7-A9, and rules R l-R4. Call it the system T.

These sentences and rules are in quite generalized forms. To put a clearer explanation ofTDAL, we consider those that are close to A6. As we have known, A6 is not valid in TDAL. However, A6 will be satisfied if a condition is satisfied. It is easy to verify that the rule Acpl\t:: ...... Bcp is valid in TDAL, as well as the sentence LAcp --. L(Acp 1\ Lcp <--> Bcp) (Also, they can be derived from system T). We may see the rule as a process: In the beginning, the agent is not aware of a sentence 'P so that the substitute instance of A6 of 'P is not true; if by some reasons the agent is aware of cp, then it will deem the substitute instance of A6 of 'P to be true. Thus, if the agent implicitly believes that it is able to be aware of cp, then it also implicitly believes that the substitute instance of A6 of 'P is true. That is just the above sentence's meaning.

Note that the sentence L(Acp 1\ Lcp <--> Bcp) is not valid in TDAL. Thus, in general, A6 is not an implicit belief of the agent. That is to say, the agent may never be aware of some sentences (maybe they are too long and too complicate). So, for Acp 1\ Lcp .--. Bcp to be an implicit belief, there has to put a condition: The agent (implicitly) believes Acp.

In general, the deduction theorem does not hold. A limited version of the deduction theorem is presented.

Theorem 2.5 Iff f--r cp, then f--r (L'l/;1 1\ ... 1\ L'l/Jn) --> Lcp, where '1/;1 , . . . , '1/Jn are members off that are used in the derivation r f--r 'P·

Proof Consider a derivation 'f!I, ... , 'Pn of 'P from r. We show by induction on i ( i ::;: n) that f--r ( L'l/;1 1\ ... 1\ L'l/Jn) --. L'f!i· The inductive steps for 'Pi an axiom, for 'Pi E r, and for 'Pi a conclusion from Rl are clear.

Suppose 'Pi=Ltpj is obtained from 'Pj by R2. By induction hypothesis, f--r (L'l/;1 1\ .. . 1\ L'l/Jn) --> L'f!j· By A2, f--r Lcpj -t LL'f!j· Thus f--r (L'l/;1 1\ ... 1\ L'l/Jn)--. L'Pi·

Suppose that 'Pi=x .--. x* is obtained from A¢1, ... , A¢n by R3. By induction hypothesis, f--r (L'l/;1 1\ ... 1\ L'l/Jn) -t LA¢1, .. . , f--r (L'l/;1 1\ ... 1\ L'l/Jn) --. LA¢n· Then by A8, we have f--r (L'l/;1 1\ ... 1\ L'l/Jn) -t L'f!i· The inductive steps for R4 is similar to R3 's. D

A set of formulas is consistent if one cannot derive from it 'P and "" 'P for some formula tp. A set of formulas is maximal consistent if it is consistent and any strict superset is incon­ sistent.

Lemma 2.6 (I) Any consistent set is included in a maximal consistent set. (2) If r is maximal consistent, then for all formulas 'P and '1/J the following hold: (a) If B ¢ occurs free in 'P infers that A¢ E f, then either tp E r or"" tp E f; (b) if 'P E f and 'P -t '1/J E f, then '1/J E f; (c) if tp is provable, then 'PEr.

Proof The proof is left to the reader. D

Theorem 2.7 The system Tis sound and complete with re­ spect to TDAL.

Proof The soundness is easy to see. We prove complete­ ness using standard techniques with modifications to fit the context.

It is sufficient to show that every consistent formula is sat­ isfiable. We do so by constructing a canonical Kripke model M, containing a possible world sr for every maximal con­ sistent set r, such that M, sr F 'P iff 'P E r. Since every consistent formula is contained in some maximal consistent set, this suffices. Let M = (S, 1r, R, A), where

• S = {r Iris a maximal consistent set};
• 1r(sr,p) = 11 ifp E f; 7r(sr ,p) = 01 ifp Efi';
• A( sr) = { 'P I Acp E r};
• (sr,,sr2) E Riff{cp I Lcp E ri} ~ r2.

Axioms A3, A4 and A5 guarantee that the binary relation R as defined is indeed transitive, Euclidean, and serial.

By induction on the structure of cp, we show that M, sr f= 'P iff 'P E r. The cases when 'P is an atom or 'P = A 'I/; is directly proved from the definition of M.

Suppose 'P ="" '1/J. (1) Suppose 'P E r. Because the in­ ference rule cp,;;;cp can be derived for the system T, '1/J ~tr and so, by inductive hypothesis, sr W'l/J. By R4, if B¢ occurs free in '1/J, then A¢ E r. Then by R3, sr F '1/J <-t '1/;*. We get sr fr!'l/J*. Because '1/;* is bound, sr F"" '1/;*. Thus sr F"" 1/J. (2) Suppose sr f= cp. Then sr fr!'l/J and for every free occur­ rence of B¢ in '1/;, sr f= A¢ and so, by inductive hypothesis, '1/J Efi'. Also we have A¢ E r. Then by Lemma 2.6,"" '1/J E r. The inductive step for --. is similar.

Suppose 'P = L'l/J. (1) Suppose L'l/J E r. It is directly ob­ tained from the definition that sr f= L'l/J. (2) Suppose Lcp t;tf. Consider the set r' = {xI Lx E r}. We show that r' f--r 1/J does not hold. Indeed, by assuming otherwise, we would have r' f--r '1/J and so, by theorem 2.5, {Lx1, ... , Lxn} f--r L'l/;, where XI ... Xn are all distinct formulas in r' that are used in the derivation r' f--r '1/J. So r f--r L'l/J, contrary to the consistency of r. Thus r' U {"" '1/J} is consistent and so, it is contained in some maximal consistent set r". By the def­ inition of r', we have sr Rsr" and '1/J f:f". By inductive hypothesis, sr" IF'l/J and so, sr ltf=L'l/J.

Suppose 'P = B'!f;. Note that the two rules, A~,~cp and A::lLcp can be derived from R3 and R4. Using the two rules, a process similar to the inductive step for L can demonstrate thatB'l/; E r iffsr F B'l/;. D

3 Hybrid Two-Dimensional Awareness Logic

3.1 Semantics

Thijsse presented in [Thijsse, 1996] a noteworthy method of modeling actual belief. His so-called hybrid system consists of an inner partial logic (within the actual belief operator) and an outer classical logic. It is implemented by distinguish­ ing two kinds of truth relations: a bivalent truth relation, re­ flecting objective truth and a trivalent truth relation, reflecting subjective truth.

Our proposal is to take TDAL as the inner logic, unlike Thijsse's logic, where partial logic is adopted. There is a rea­ sonable motivation to proceed TDAL into a hybrid semantics. As has been shown, "truth" discussed in TDAL is indeed sub­ jective truth: In TDAL, the meaning of a sentence being said to be true is that from the point of view of an agent it is true. The semantics of TDAL is reasonable only if we understand it in this way. For example, it is intuitive that A6 should be objectively true; however, from the point of view of an agent, it may not be (subjectively) true.

We call the resultant logic hybrid two-dimensional aware­ ness logic, abbreviated HTAL. Formally, a HTAL model is a tuple M = (S, 1r, R, A) with its usual meaning. There are two truth relations, f= and II-, where f= is just the truth rela­ tion defined in TDAL, and where II- is defined as follows :

• M,slf-p¢?7r(s,p) =ll;
• M, s II-"' <p ¢:? M, sii-'P does not hold;
• M,s lf-cp--+ '¢ ¢:? M, s lf-cpdoesnotholdor M,s If- '¢;
• M, s If- Acp ¢:? <p E A(s);
• M, s If- L<p ¢:} M , sF= L<p;
• M, s If- B <p ¢:} M, s F= B<p.

Validity is defined as overall classical truth: If- <p ¢:? M, s 11<p for all models and possible worlds.

When checking the truth value of a formula, one starts with a two-valued evaluation and is dragged into the multi-valued mode only by the belief operators. Within the belief opera­ tors, sentence's truth value is calculated by TDAL, reflecting subjective truth. Outside belief operators, it is calculated clas­ sically, reflecting objective truth.

Except adopting different logic as inner logic, there is another significant difference between HTAL and Thijsse's logic. In the latter, partiality is specified by evaluation, and does not come from the limitation to actual belief. Its "hy­ brid" character when taken by itself is irrelevant to an aware­ ness condition. While in HTAL, the jumping-off point is in­ deed two-valued, both for inner logic and outer logic. Atoms are always assigned values classically. The non-classical as­ pect appears only when a belief operator occurs.

3.2 Discussion And Formalization

ln contrast to TDAL, where limited versions of A6 and classi­ cal tautologies are present, A6 and all classical tautologies are valid in HTAL. This is reasonable because validity in HTAL is defined as over-all classical truth, which reflects objective truth.

The two truth relations f= and II- are closely related.

Proposition 3.1 (i) If M , s f= <p, then M, slf- <p.

• (ii) If M , sll- <p and <p is bound, then M , s f= <p.

Proof The proof is by induction on the structure of <p. Details are left to the readerD

It directly follows from proposition 3. l(i) that TDAL is a sub-logic of HTAL. All provable formulas of system T are valid in HTAL.

The necessity rule, R2, does not hold in general in HTAL. Instead, there is a limited version.

R2': from <p to infer Lcp, where <p is bound.

It is easy to verify that R2' is valid in HTAL.

The system corresponding to the semantics of HTAL con­ sists of all axioms of KD45 and T, R 1 and R2'. Call it the sys­ tem H. To prove the completeness of H, the following propo­ sition is needed.

Proposition 3.2 If'¢ 1-r <p, then 1-H L'¢ --+ Lcp.

Proof Let cp1 , . . . , 'Pn be the given T-deduction of <p from ·!j;. We show by induction on i ::::; n that 1-H L'¢ --+ Lcpi .

Suppose 'Pi = '¢. 1-H L'¢ --+ L<pi because the formula is a propositional tautology.

Suppose 'Pi is an axiom of H. Then 'Pi is also an axiom of H and 'Pi is bound. Applying R2' to it, we get f- 1-1 Lcpi and so, 1-H L'¢ --+ L<pi.

Suppose 'Pi is obtained from 'Pk='Pj --+ 'Pi and ({)j by Rl, where k, j < i . Then by induction hypothesis, f- H L'¢ --+ L(<pj --+ 'Pi) and f-H L'¢ --+ Lcpj. By Al, A2 and Rl, 1-H L'¢ --+ Lcpi.

Suppose 'Pi=L<pj is obtained from 'Pj by R2', where j < i. By induction hypothesis, 1-H L'¢ --+ Lcpj. By A3, f- H L<pj --+ LL<pj. So 1-H L'¢ --+ LLcpj. D

Notice that a standard canonical model of H is indeed a classical Kripke model. So to prove the completeness of H, a more complicated canonical model has to be considered. The model is similar to the H-canonical model presented in [Thi­ jsse, 1996]. The set of worlds of the model contains just one H-maximal consistent set as its root, all other worlds are T­ maximal consistent set. The root is not accessible from other worlds. Formally, for a given H-maximal consistent set ~' define the H-canonical model M of~ as (S, 1r, R , A), where

• S = { sE} U Sr, where Sr = { sr I r is a T-maximal consistent set};
• for every s::, E S ,1r(s::, ,p) = 11 ifp E ~; 1r(s::,,p) = 01 if p (j~, where pis an atom.
• foreverys::, E S,A(s::,) = {cp I Acp E ~};
• (s::,, St-. 2 ) E Riff {<pI L<p E ~I} <:;; ~2, where St-. 1 E Sand s:-. 2 E Sr.

The next lemma makes clear the benefit of H-canonical model.

Lemma 3.3 Let M be an H-canonical model of~- Then for any formula <p,

• (i) M, sr f= <p if and only if <p E r, where sr E Sr
• (ii) M, SE II- <p if and only if <p E ~

Proof Since the sub-model of M obtained by restricting it to ST is just a canonical model of the system T, the proof of (i) has already been given in Theorem 2.7.

The proof of (ii) is by induction on the structure of cp. The basic steps, cp is an atom and cp = A'lj;, are direct. Because H contains all classical tautologies, the induction step for rv and ----+ is carried out by the standard techniques of propositional reasonmg.

Suppose cp = L'lj;. (1) Suppose L'lj; E 2:. It follows from the definition that for all sr such that sr; Rsr, 1jJ E r and so, M , sr f= 1jJ and then, M, sr; II- L'lj;. (2) Now focusing on the other direction, suppose L'lj; f:I:. Consider the set r = {x I Lx E 2:}. By proposition 3.2, using steps similar to those in the proof of theorem 2.7, it can be shown that r ry 1jJ does not hold. Thus r U {"" 1/J} is T-consistent and so it is contained in some T-maximal consistent set r'. By the definition of r, we have I:Rf' and 1jJ E1f'. Then sr' ~1/J and so, sr; II- L'lj; does not hold. The inductive step for the B operator is similar. D

Notice that the axioms A3-A5 are contained in all worlds of the H-canonical model. So by proposition 3.1(i), M, s lf-cp for all worlds s in M, where cp E { A3, A4, A5}. Thus the rela­ tion R defined in the H-canonical model is indeed transitive, Euclidean, and serial.

Theorem 3.4 System His sound and complete for the seman­ tics of HTAL.

Proof The soundness is easy to check. To show complete­ ness, suppose f- H cp does not hold. Then there exists a H­ maximal consistent set 2: such that cp \t'I:. Construct a H­ canonical model of 2: with designated world 2:. By lemma 3.3, M, sr; II- cp does not hold. D

4 Conclusion

Many doxastic logics have been suggested in the literature, reflecting quite different concepts of actual belief. One may wonder why there are so many proposals. Were all of us to agree on what human belief is, an "unique right" model of be­ lief would be possible. However, it is not the case, as can be seen from philosophical controversies continuing from long ago. Thus all of the logics have their own claim to "correct­ ness", if they have clear explanations.

The method using two-dimensional logic to model aware­ ness and actual belief has, in our opinion, particular benefits. Processing awareness condition independently gives us more flexibility in controlling the model that is constructed. Differ­ ent opinions about the relation between awareness and actual belief will be reflected in different models, which can be ob­ tained by amending the underlying two-dimensional logic. Of course, there are other, maybe many, alternatives to the logics presented in this paper. For example, it is possible to give a doxastic logic with the two-dimensional logic presented by Bergmann in [Bergmann, 1991], in which the logic is in­ tended to be along Russellian lines. Examination of this or other forms of doxastic logics and the relations among them would call for further research.

There has begun to be use of awareness logic for net pro­ tocol verification [Accorsi, 2001]. We think the method presented in this paper may be useful in that purpose. This also calls for further research.

5 Acknowledgements

We would like to thank Nuel Belnap for his detailed reading of the earlier version of this paper and numerous pertinent comments and criticisms.