Dayan Pérez-Quintana

Christos Bilitos

J Ruiz-García

D Gonzalez-Ovejero

Miguel Beruete

Flat Lens Antenna using Gap Waveguide Technology at Millimeter Waves

In this paper, a flat lens antenna using Gap Waveguide (GW) technology working in the millimeter waves band was designed. The metamaterial lens is fed using a Groove Gap Waveguide (GGW) horn antenna in order to achieve a plane wavefront at broadside. Both devices, metalens and GGW antenna achieve excellent radiation results when combined together. Due to metallic composition, the structure presents more robustness, low loss, and adaptability to a flat surface, able to be used in millimeter wave application.

I. INTRODUCTION

With the rapid development of modern wireless communication technology, the fifth-generation (5G) mobile standard and Internet of Things (IoT), the 60 GHz frequency band has received a special attention due to its potential functional benefits. The demand for faster speed, the greater volume of information required and multibeam antennas with high gain, have gained increasing attention from the engineering community to solve all of these modern problems.

A fundamental obstacle that must be circumvented to achieve a full development of high frequency technology is the problem of guiding waves with low loss. Traditional feeding systems like waveguides and microstrip lines suffer from increasing loss as the frequency grows. In last decade, Gap Waveguide (GW) technology has gained a lot of interest since it is a reliable and competitive alternative for high-frequency communications [START_REF] Kildal | Local Metamaterial-Based Waveguides in Gaps Between Parallel Metal Plates[END_REF] with three main variants: groove-gap waveguide (GGW) [START_REF] Berenguer | Propagation Characteristics of Groove Gap Waveguide Below and Above Cutoff[END_REF], ridge-gap waveguide (RGW) [START_REF] Perez-Quintana | Compact Groove Diamond Antenna in Gap Waveguide Technology with Broadband Circular Polarization at Millimeter Waves[END_REF] and microstrip-gap waveguide (MGW) [START_REF] Liu | Design and Fabrication of a High-Gain 60-GHz Cavity-Backed Slot Antenna Array Fed by Inverted Microstrip Gap Waveguide[END_REF]. GW shows considerable improvements compared to standard metallic waveguides, such as low loss, it does not require electric contact and it is easily adaptable to flat surfaces [START_REF] Park | A photonic bandgap (PBG) structure for guiding and suppressing surface waves in millimeter-wave antennas[END_REF]. It also has a lower manufacturing cost with respect to traditional hollow waveguides, since the tolerances are coarser alleviating the fabrication constraints.

Beyond that, it is evident that designing a high gain and broadband antenna using this technology opens new avenues for high frequency communication. There is an increasing interest in MTS antennas due to their ability to provide high gains, while at the same time maintaining a light weight and a low profile, making them excellent candidates for lens antenna applications such as the Luneburg Graded Index (GRIN) lens [START_REF] Luneburg | Mathematical Theory of Optics[END_REF]. In order to improve the antenna characteristics, a very attractive idea is to use classic antennas in GW technology and combine it with the metalenses. Therefore, the main objective of this investigation is to combine these technologies to have antennas with good radiation characteristics and support the implementation of 5G mobile communications.

II. DESIGN OF THE LENS

Typically, metasurfaces consist of sub wavelength patches or metallic elements arranged in a regular lattice arrangement [START_REF] Park | A photonic bandgap (PBG) structure for guiding and suppressing surface waves in millimeter-wave antennas[END_REF]. By loading a Parallel Plate Waveguide (PPW) with a fakir's bed of nails consisting of metallic posts of different height, we can emulate the behavior of an artificial dielectric for a TM surface wave [START_REF] Bosiljevac | Non-Uniform Metasurface Luneburg Lens Antenna Design[END_REF]. Here, a metal-only metasurface antenna is implemented in order to overcome the dielectric losses associated with typical lens antennas in the microwave band, as well as provide integrity to the antenna in harsh environmental conditions.

Realizing this concept, a planar Luneburg lens is considered as it offers full azimuthal scan with fan beams in the V-band taking even more advantage of the all-metal lens properties. The refractive index of a Luneburg lens follows the next equation:

= 2 - ( 1
)
Where r is the distance between the point of interest and the center of the lens, and R is the radius. Simulating the dispersion diagram of the unit-cell, as shown in Fig. 1(a), we can see the formation of a stop band, which in turn shows single mode propagation with a linear, non-dispersive behavior in a large bandwidth within the considered frequency range, making this unit-cell a suitable candidate for the realization of the lens. The parameters are the periodicity puc of the unit-cell, the width of the metallic post auc, and the ground height hground. By varying the ground height where the post lays, thus varying the effective height of the post we are able to derive an effective refractive index at single frequency (Fig. 1(b)).

Matching that to the profile on the Luneburg lens and mapping the corresponding ground height of each unitcell, we can construct the final geometry of the metasurface lens with radius equal to 5λ0 and the PPW height being d = 2.1 mm above the maximum metallic post height (huc,max = 1.3mm) where λ0 is the freespace wavelength at the design frequency f0 = 60 GHz. The lens system is first fed with a conventional H-plane sectoral horn giving satisfactory results, Fig 1(c).

III. ANTENNA DESIGN

Up to this point, we have modulated a surface using a bed of nails to achieve the Luneburg lens behavior and have excited it with a classical metallic horn. The next step is to feed the Luneburg lens with a horn antenna made in GGW technology.

The first step is to design a horn antenna using GGW technology able to obtain a similar phase center than the classical horn used before. Applying the theory studied in [START_REF] Kildal | Local Metamaterial-Based Waveguides in Gaps Between Parallel Metal Plates[END_REF], Fig. 2(a) shows the GGW horn antenna used to feed the metalens. In this case, a single pin (inset of Fig. 2(a)) of height h=1.5 mm and periodicity p=1 mm generates a bandgap around 40-80 GHz. This frequency band is adequate for our design. In this case, the main objective is to achieve a similar phase center than the classical horn antenna to feed the Luneburg lens. Fig. 2(b) shows the GGW horn antenna placed on the metasurface edge, in order to obtain similar radiation characteristics as before. Finally, Fig. 2(c) shows the normalized vertical component of the electric field from a top view. Analyzing it, it is clear that we achieve a plane wave in the broadside direction, in good agreement with the previous results using a conventional H-plane sectoral horn. It is clearly seen that the lens manages and transforms the wavefront from the GGW horn antenna into a plane wave. This time, the GGW horn antenna used gives similar radiation characteristic that in combination with a Luneburg lens improves the results in a more compact design.

VI. CONCLUSIONS

To sum, in this article an analysis of a Luneburg lens excited by a GW horn antenna has been presented. A metamaterial lens has been synthesized using metallic pins to modulate a specific permittivity in order to achieve a plane wave at broadside direction. A GGW horn antenna was designed, that combined with the metasurface achieved excellent radiation characteristic. Furthermore, thanks to its fully metallic structure and design, this system has more robustness, low loss and adaptability to plane surfaces; i.e., necessary features for millimeters applications.

Fig. 1 .

 1 Fig. 1. (a) Dispersion diagram of the unit cell for the following dimensions: puc = 0.8mm, auc= 0.3 mm and hground = 0.75mm. (b) Equivalent refractive index as a function of the unit cell's ground height hground at f0 = 60 GHz. (c) Normalized electric field magnitude |Re{Ez}| at 60 GHz for the planar PPW Luneburg lens of radius R = 5λ0 fed with an H-plane sectoral horn.

Fig. 2 .

 2 Fig. 2. (a) GGW Horn Antenna. (b) Luneburg lens plus GGW horn antenna. (c) Normalized electric field magnitude |Re{Ez}| at 58 GHz in decibel scale.

ACKNOWLEDGEMENT

This research was funded by Spanish Ministerio de Ciencia, Innovación y Universidades, Project RTI2018-094475-B-I00 (MCIU/AEI/FEDER,UE).


Emiliano Lorini

Pengfei Song

A Computationally Grounded Logic of Awareness

We introduce a multi-agent logic of explicit, implicit belief and awareness with a semantics using belief bases. The novelty of our approach is that an agent's awareness is not a primitive but is directly computed from the agent's belief base. We prove soundness and completeness of the logic relative to the belief base semantics. Furthermore, we provide a polynomial embedding of the logic of propositional awareness into it, and a polynomial embedding of our logic into the logic of general awareness. Thanks to the latter embedding, we show that the satisfiability checking problem for our logic is PSPACE-complete. Finally, we extend it by the notions of public announcement and private belief expansion.

Introduction

The notion of awareness was introduced in the area of epistemic logic by Fagin & Halpern (F&H) [START_REF] Fagin | Belief, awareness, and limited reasoning[END_REF] to cope with the problem of logical omniscience [START_REF] Hintikka | Knowledge and belief[END_REF]. Their approach is syntactic to the extent that they associate a subset of formulas to each agent at each state, indicating the formulas the agent is aware of. Following the idea suggested by Levesque [START_REF] Levesque | A logic of implicit and explicit belief[END_REF], F&H make the distinction between explicit belief and implicit belief, where explicit belief is defined to be implicit belief plus awareness.

There is another tradition in the formalization of awareness, initiated by Modica & Rustichini [START_REF] Modica | Awareness and partitional information structures[END_REF][START_REF] Modica | Unawareness and partitional information structures[END_REF] and Heifetz et al. [START_REF] Heifetz | Interactive unawareness[END_REF][START_REF] Heifetz | A canonical model for interactive unawareness[END_REF]. They support a semantic approach by letting possible worlds be associated with a subset of all propositional variables being defined. Hence, an agent is aware of a formula if and only if, every atomic proposition occurring in the formula is defined at every epistemically accessible state for the agent. Such a notion of awareness is often called propositional awareness in opposition to the notion of general awareness, according to which an agent can be "primitively" aware not only of atomic propositions but also of complex formulas. Halpern et al. [START_REF] Joseph | Alternative semantics for unawareness[END_REF][START_REF] Halpern | Interactive unawareness revisited[END_REF] prove an equivalence result between the syntactic approach and the semantic approach for propositional awareness. van Ditmarsch et al. [START_REF] Hans Van Ditmarsch | Implicit, explicit and speculative knowledge[END_REF] give a novel notion called speculative knowledge, which is also built on propositional awareness.

The concept of explicit belief, which is central in the logic of awareness, is closely related to the concept of belief base [START_REF] Nebel | Syntax based approaches to belief revision[END_REF][START_REF] Makinson | How to give it up: A survey of some formal aspects of the logic of theory change[END_REF][START_REF] Ove | Theory contraction and base contraction unified[END_REF][START_REF] Rott | Just because": Taking belief bases seriously[END_REF]. The latter plays an important role in the AGM approach to belief revision [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF] and, more generally, in the area of knowledge representation and reasoning (KR). Recently, in [START_REF] Lorini | In praise of belief bases: Doing epistemic logic without possible worlds[END_REF][START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF] we defined a formal semantics for multi-agent epistemic logic exploiting belief bases which clearly distinguishes explicit from implicit belief. Specifically, according to this semantics, an agent explicitly believes that a certain fact ↵ is true if ↵ is a piece of information included in the agent's belief base. On the contrary, the agent implicitly believes that ↵, if ↵ is derivable from the agent's belief base. A logic of explicit and implicit belief, called Logic of Doxastic Attitudes (LDA), was defined on the top of this semantics. The logic was further enriched in a series of papers with the aim of capturing higher-order epistemic reasoning in robots [START_REF] Lorini | Exploiting belief bases for building rich epistemic structures[END_REF], the notions of "only believing" [START_REF] Lorini | Decision procedures for epistemic logic exploiting belief bases[END_REF] and graded belief [START_REF] Lorini | A computationally grounded logic of graded belief[END_REF], and of elucidating the connection between distributed belief and belief merging [START_REF] Herzig | A logic of explicit and implicit distributed belief[END_REF].

In this paper, we extend the semantics introduced in [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF] and the corresponding logic LDA with propositional awareness. We call LDAA the resulting logic. The novelty of our approach lies in the fact that the notion of awareness is not primitive but is computed from, and therefore grounded on, the notion of belief base. In particular, for an agent to be aware of a proposition p, p has to be included in the agent's vocabulary, that is to say, there should exist a formula in the agent's belief base which contains p. From this perspective, we o↵er a minimalistic logic approach to explicit, implicit belief and awareness in which only the former concept is primitive, while the other two concepts are defined from it.

The paper is organized as follows. In Section 2, we present the language of our logic of explicit, implicit belief and awareness. In Section 3, we first present the belief base semantics with respect to which the language is interpreted. Then, we introduce two alternative semantics which are closer in spirit to the standard semantics for epistemic logic based on multi-relational Kripke structures. We show that the three semantics are all equivalent with respect to the language under consideration. Section 4 presents axiomatic results for our logic, while in Section 5 we explore the connection between our logic and the logic of propositional awareness (LPA) [START_REF] Joseph | Alternative semantics for unawareness[END_REF], by providing a satisfiability preserving translation of the latter into the former. In Section 6, we establish the connection between our logic and the logic of general awareness (LGA) [START_REF] Fagin | Belief, awareness, and limited reasoning[END_REF], by providing a satisfiability preserving translation of the former into the latter. Thanks to the latter embedding, we show that that the satisfiability checking problem for our logic is PSPACE-complete. Section 7 clarifies the ontological foundation of our logic LDAA in connection with the logic of propositional awareness (LPA) and the logic of general awareness (LGA). Section 8 presents two dynamic extensions of the static setting, the first by public announcement and the second by the notion of private belief base expansion. In Section 9 we conclude.

Language

This section presents the language of the Logic of Doxastic Attitudes with Awareness (LDAA) to represent explicit beliefs, implicit beliefs, and awareness. It extends the language in [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF] with the awareness modality. Let Atm = {p, q, . . .} be a countably infinite set of atomic propositions and let Agt = {1, . . . , n} be a finite set of agents. The language L 0 (Atm, Agt) is defined as follows:

↵ ::= p | ¬↵ | ↵ 1 ^↵2 | 4 i ↵ | i ↵
, where p ranges over Atm and i ranges over Agt.

The language L LDAA (Atm, Agt) adds to L 0 (Atm, Agt) a new level with implicit belief operators and is defined as follows:

' ::= ↵ | ¬' | ' 1 ^'2 | 2 i ' | i '
, where ↵ ranges over L 0 (Atm, Agt) and i ranges over Agt.

When it is unambiguous from the context, we write L 0 instead of L 0 (Atm, Agt) and L LDAA instead of L LDAA (Atm, Agt). The other Boolean connectives _, !, $, > and ? are defined from ¬ and ^in the standard way. The formula 4

i ↵ is read "agent i explicitly believes that ↵ is true". The formula i ' is read "agent i is aware of '". The 4 i -operator can be iterated, which means that the language contains expressions for higher-order explicit beliefs, such as 4 i 4 j ↵, which is read "agent i explicitly believes that agent j explicitly believes that ↵ is true". The iteration is possibly a mix of explicit belief and awareness, such as 4 i j ↵, which is read "agent i explicitly believes that agent j is aware of ↵". The formula 2 i ' is read "agent i implicitly believes that ' is true". The dual operator 3 i is defined as follows:

3 i ' def = ¬2 i ¬', where 3
i ' is read "' is consistent with agent i's explicit beliefs"1 . Note that the modality i appears at both levels of the language, but the modality 4 i only appears at the first level. As a result, we can have awareness operators in the scope of explicit belief operators, but not implicit belief operators in the scope of explicit belief operators. Moreover, both the explicit belief and implicit belief operator are allowed inside the awareness operator. It is because the concept of propositional awareness allows awareness of any formula that is constituted by atomic propositions of which the agent is aware.

Since we represent a propositional notion of awareness, i.e., being aware of a formula is equivalent to being aware of every atomic proposition occurring in it, we need the following inductive definition to represent the set of atomic propositions occurring in a formula ', noted Atm('):

Atm(p) = {p}, Atm(¬') = Atm('), Atm(' 1 ^'2 ) = Atm(' 1 ) [ Atm(' 2 ), Atm(4 i ↵) = Atm(↵) Atm(Y i ') = Atm('), for Y 2 { , 2}. Let ✓ L LDAA be finite, we define Atm( ) = S '2 Atm(').

Semantics

In this section, we present three families of formal semantics for L LDAA . The first semantics exploits belief bases. An agent's set of doxastic alternatives and awareness set are not primitive but computed from them. The second semantics is a Kripke-style semantics, in which we require each agent's set of doxastic alternatives to be equal to the set of worlds in which his explicit beliefs are true, and the agent's awareness set to be equal to the set of of atomic propositions occurring in his explicit beliefs. The third semantics relaxes these requirements, so that an agent's set of doxastic alternatives is included in the set of worlds in which the agent's explicit beliefs are true, and the set of atomic propositions occurring in an agent's explicit beliefs is a subset of the agent's awareness set.

Multi-Agent Belief Base Semantics

The basic constituent of our semantics is the following notion of state.

Definition 3.1 A state is a tuple S = (B 1 , . . . , B n , A 1 , . . . , A n , V ) where, • B i ✓ L 0 is agent i's belief base for any i 2 Agt, • A i = Atm(B i ) is agent i's awareness set for any i 2 Agt, • V ✓ Atm is the actual environment.
The set of all states is denoted by S.

With the definition of state, we have the following interpretations for the formulas in L 0 .

Definition 3.2 For any S = (B 1 , . . . , B n , A 1 , . . . , A n , V ) 2 S: S |= p () p 2 V, S |= ¬↵ () S 6 |= ↵, S |= ↵ 1 ^↵2 () S |= ↵ 1 and S |= ↵ 2 , S |= 4 i ↵ () ↵ 2 B i , S |= i ↵ () Atm(↵) ✓ A i .
Note that the awareness component of Definition 3.1 is unnecessary, as we could interpret the operator i equivalenty by postulating "S |= i ↵ i↵ Atm(↵) ✓ Atm(B i )". The reason we keep it is that it has counterparts in the notional model semantics and quasi-notional model semantics we will define in Sections 3.2 and 3.2. In the quasi-notional model semantics, an agent's awareness set is supposed to be a superset of the set of atomic propositions occurring in the agent's belief set.

Note that the notion of awareness represented by the i -operator is propositional, i.e., being aware of a formula is equivalent to being aware of every atomic proposition occurring in the formula. Such a notion of awareness is different from the notion of general awareness according to which an agent can be aware of p ^q without being aware of p _ q.

The following definition introduces the concept of multi-agent belief-awareness model.

Definition 3.3 A multi-agent belief-awareness model (MABA) is a pair (S, Cxt),
where S 2 S and Cxt ✓ S.

Cxt is the agents' context or common ground [START_REF] Stalnaker | Common ground[END_REF]. It corresponds to the body of information that the agents share and that they use to make inferences from their explicit beliefs. Following [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF], in the following definition we compute the agents' epistemic accessibility relations from their belief bases. With the accessibility relation defined, we have the following semantic interpretation for formulas in L LDAA . The boolean case is defined in the usual way and omitted.

Definition 3.5 Let (S, Cxt) be a MABA with S = (B 1 , . . . , B n , A 1 , . . . , A n , V ). Then, (S, Cxt) |= ↵ () S |= ↵, (S, Cxt) |= 2 i ' () 8S 0 2 Cxt, if (S, S 0 ) 2 R i then (S 0 , Cxt) |= ', (S, Cxt) |= i ' () Atm(') ✓ A i .
The following two definitions specify two interesting properties of MABAs.

= (B 0 1 , . . . , B 0 n , A 0 1 , . . . , A 0 n , V 0 ) 2 Cxt, i 2 Agt and ↵ 2 B 0 i we have S 0 |= ↵.
For X ✓ {GC, BC}, MABA X is the class of MABAs satisfying all the conditions in X. MABA ; is the class of all MABAs, and we write MABA instead of MABA ; . It is easy to see that MABA {GC,BC} = MABA {BC} .

Let ' 2 L LDAA , we say that ' is valid for the class MABA X if and only if, for every (S, Cxt) 2 MABA X we have (S, Cxt) |= '. We say that ' is satisfiable of the class MABA X if and only if ¬' is not valid for the class MABA X .

Notional Model Semantics

In this section we introduce an alternative Kripke-style semantics for the language L LDAA based on notional doxastic-awareness models. The latter extend notional doxastic models defined in [START_REF] Lorini | In praise of belief bases: Doing epistemic logic without possible worlds[END_REF][START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF] by awareness functions.

Definition 3.8 A notional doxastic-awareness model (NDAM) is a tuple M = (W, D, A, N , V) where,
• W is a non-empty set of worlds,

• D: Agt ⇥ W ! 2 L0 is a doxastic function, • A: Agt ⇥ W ! 2 Atm is an awareness function, • N : Agt ⇥ W ! 2 W is a notional function, • V: Atm ! 2 W is a valuation function.
and such that, given the following inductive definition of the semantic interpretation of formulas in L LDAA : w), it satisfies the following conditions (C1) and (C2), for all i 2 Agt and for all

(M, w) |= p () w 2 V(p), (M, w) |= ¬' () (M, w) 6 |= ', (M, w) |= ' ^ () (M, w) |= ' and (M, w) |= , (M, w) |= 4 i ↵ () ↵ 2 D(i, w), (M, w) |= 2 i ' () 8u 2 N (i, w), (M, u) |= ', (M, w) |= i ' () Atm(') ✓ A(i,
w 2 W : (C1) A(i, w) = Atm D(i, w) , (C2) N (i, w) = T ↵2D(i,w) ||↵|| M , where ||↵|| M = {u 2 W : (M, u) |= ↵}.
We recall that the term 'notional' is borrowed from the philosopher D. Dennett [START_REF] Daniel | The Intentional Stance[END_REF][START_REF] Daniel | Précis of the intentional stance[END_REF] (see, also, [START_REF] Konolige | A deduction model of belief[END_REF]): an agent's notional world is a world at which all the agent's explicit beliefs are true.

This idea is clearly expressed by Condition (C2): a world is in N (i, w) (i.e., agent i's set of notional worlds at w) if and only if it satisfies all explicit beliefs that agent i has at w.

The following definitions specify global consistency (GC) and belief correctness (BC) for notional models. Definition 3.9 The NDAM M = (W, D, A, N , V) satisfies global consistency if and only if, for any i 2 Agt and for any w 2 W , N (i, w) 6 = ;. Definition 3.10 The NDAM M = (W, D, A, N , V) satisfies belief correctness if and only if, for any i 2 Agt and for any w 2 W , w 2 N (i, w).

For any X ✓ {GC, BC}, NDAM X is the class of NDAMs satisfying the conditions in X. NDAM ; is the class of all NDAMs, and we write NDAM instead of NDAM ; . Analogously to MABAs, we have NDAM {GC,BC} = NDAM {BC} . A NDAM M = (W, D, A, N , V) is finite if and only if W , D(i, w), and V (w) are finite sets for every i 2 Agt and every w 2 W , where

V (w) = {p 2 Atm : w 2 V(p)}. As A(i, w) = Atm D(i, w) , it follows that, if M is finite, A(i, w
) is also a finite set for any i 2 Agt and any w 2 W . We use finite-NDAM X to denote the class of finite NDAMs satisfying the conditions in X.

Let ' 2 L LDAA , we say that ' is valid for the class NDAM X if and only if, for every M = (W, D, A, N , V) 2 NDAM X and for every w 2 W , we have (M, w) |= '. We say that ' is satisfiable for the class NDAM X if and only if ¬' is not valid for the class NDAM X .

Quasi-Model Semantics

This section provides an alternative semantics for the language L LDAA based on a more general class of models, called quasi-notional doxastic-awareness models (quasi-NDAMs) in which the restrictions on the notional and awareness function are weakened. Definition 3.11 A quasi-notional doxastic-awareness model (quasi-NDAM) is a tuple M = (W, D, A, N , V) where W, D, A, N , V together with the semantic interpretation of formulas in L LDAA are as in Definition 3.8, except that Condition (C1) and (C2) are replaced by the following weaker conditions, for all i 2 Agt and for all w 2 W :

(C1 ⇤ ) Atm D(i, w) ✓ A(i, w), (C2 ⇤ ) N (i, w) ✓ T ↵2D(i,w) ||↵|| M .
As for NDAMs, for any X ✓ {GC, BC}, QNDAM X is the class of quasi-NDAMs satisfying the conditions in X. QNDAM ; is the class of all quasi-NDAMs, and we write QNDAM instead of QNDAM ; . As for MABAs and NDAMs, we have QNDAM {GC,BC} = QNDAM {BC} . A quasi-NDAM M = (W, D, A, N , V) is finite if W , D(i, w), A(i, w) and V (w) are finite sets for every i 2 Agt and every w 2 W . We use finite-QNDAM X to denote the class of finite quasi-NDAMs satisfying the conditions in X. Validity and satisfiability of formulas for a class QNDAM X are defined in the usual way.

Equivalence Results

In this section, we present equivalence results between the five di↵erent semantics for L LDAA we presented above (i.e., MABA, NDAM, finite-NDAM, QNDAM and finite-QNDAM).

Equivalence between quasi-NDAMs and finite quasi-NDAMs

First of all, we consider the relationship between QNDAM and finite-QNDAM. Let us define a filtrated model for the proof.

Let M = (W, D, A, N , V) be a (possibly infinite) quasi-NDAM and let ⌃ ✓ L LDAA be an arbitrary finite set of formulas which is closed under subformulas. The equivalence relation ⌘ ⌃ on W is defined as follows:

⌘ ⌃ = {(w, v) 2 W ⇥ W : 8' 2 ⌃, (M, w) |= ' i↵ (M, v) |= '}.
Let [w] ⌃ be the equivalence class of the world w generated by the relation ⌘ ⌃ . The model M ⌃ = (W ⌃ , D ⌃ , A ⌃ , N ⌃ , V ⌃ ) is the filtration of M under ⌃ where:

• W ⌃ = {[w] ⌃ : w 2 W },
• for any i 2 Agt and for any

[w] ⌃ 2 W ⌃ , D ⌃ (i, [w] ⌃ ) = ( T u2[w] ⌃ D(i, u)) \ ⌃,
• for any i 2 Agt and for any

[w] ⌃ 2 W ⌃ , A ⌃ (i, [w] ⌃ ) = T u2[w] ⌃ A(i, u) \⌃,
• for any i 2 Agt and for any

[w] ⌃ 2 W ⌃ , N ⌃ (i, [w] ⌃ ) = {[u] ⌃ 2 W ⌃ : 9v 2 [w] ⌃ , 9v 0 2 [u] ⌃ such that v 0 2 N (i, v)}, • for any p 2 Atm, V ⌃ (p) = {[w] ⌃ : (M, w) |= p} if p 2 Atm(⌃), V ⌃ (p) = ; otherwise.
We have the following filtration lemma showing that the filtrated model is semantically equivalent with the original model with respect to ⌃.

(M ⌃ , [w] ⌃ ) |= '.
Proof The proof is by induction on the structure of '. For the cases other than ' = i , the proof is identical with that of Lemma 4 in the appendix of [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF]. So we only need to prove the case ' = i . ()) Suppose (M, w) |= i with i 2 ⌃. Thus, Atm( ) ✓ A(i, w). Hence, by the definition of A ⌃ (i, [w] ⌃ ) and the fact that ⌃ is closed under subformulas, we have Atm(

) ✓ A ⌃ (i, [w] ⌃ ). It follows that (M ⌃ , [w] ⌃ ) |= i . (() For the other direction, suppose (M ⌃ , [w] ⌃ ) |= i with i 2 ⌃. Thus, Atm( ) ✓ A ⌃ (i, [w] ⌃ ). Hence, by the definition of A ⌃ (i, [w] ⌃ ), Atm( ) ✓ A(i, w). It follows that (M, w) |= i . ⇤
The following proposition highlights that M ⌃ is finite and preserves the properties of M . Proposition 3.1 Let ⌃ ✓ L LDAA be an arbitrary finite set of formulas which is closed under subformulas and let

M ⌃ = (W ⌃ , D ⌃ , A ⌃ , N ⌃ , V ⌃ ) be a filtration of M = (W, D, A, N , V) under ⌃.
Then, M ⌃ is a finite quasi-NDAM. Moreover, for any x 2 {GC, BC}, if M satisfies x, then M ⌃ also satisfies it.

Proof By the proof of Proposition 12 in the appendix of [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF], we have that, M ⌃ is finite and satisfies Condition (C2 ⇤ ) in Definition 3.11, and that, for any x 2 {GC, BC}, if M satisfies x, then M ⌃ also satisfies it. Here, we only need to prove that M satisfies Condition (C1 ⇤ ) in Definition 3.11. Suppose ' 2 D ⌃ (i, [w] ⌃ ), we need to prove that Atm(') ✓ A ⌃ (i, [w] ⌃ ). By the definition of D ⌃ (i, [w] ⌃ ), we have ' 2 D(i, w). By Condition (C1 ⇤ ), it follows that, Atm(') ✓ A(i, w). By the definition of A ⌃ (i, [w] ⌃ ) and the fact that ⌃ is closed under subformulas, we have Atm(') ✓ A ⌃ (i, [w] ⌃ ). As a result,

A ⌃ (i, [w] ⌃ ) ◆ Atm(D ⌃ (i, [w] ⌃ )).
⇤

The following lemma is a straighforward consequence of Lemma 3.1 and Proposition 3.1. Lemma 3.2 Let X ✓ {GC, BC} and ' 2 L LDAA . If ' is satisfiable for the class QNDAM X then ' is satisfiable for the class finite-QNDAM X .

Equivalence between finite NDAMs and finite quasi-NDAMs

Our next result concerns the equivalence between finite-NDAM and finite-

QNDAM. Lemma 3.3 Let X ✓ {GC, BC} and ' 2 L LDAA . If ' is satisfiable for the class finite-QNDAM X , then ' is satisfiable for the class finite-NDAM X .
Proof We are going to build a finite NDAM from a finite quasi-NDAM without changing the satisfiability of '. To accomplish this goal, two things are essential in the construction. Firstly, we enlarge each agent's belief base with an identifier proposition to make his set of doxastic alternatives smaller and coincide with his set of notional worlds. Secondly, we combine the identifier with some tautologies by conjunctions, so that the set of atomic propositions occurring in his belief base is equal to his awareness set.

Since the set of identifiers and Atm(') are disjoint, the satisfiability of ' is not a↵ected if ' is of the form p, 4 i or i . If ' is of the form 2 i , its satisfiability is not a↵ected since agent i's set of epistemically accessible states does not change as a consequence of the transformation.

Let M = (W, D, A, N , V) be a finite quasi-NDAM that satisfies ', i.e., there exists w 2 W such that (M, w) |= '. We define the set of all atomic propositions occurring in some awareness set of some agent at some world in M as follows:

T (M ) = [ w2W,i2Agt A(i, w).
Since M is finite, T (M ) is also finite.

We have the following injective function which assigns an identifier to each agent at each world in W .

f : Agt ⇥ W ! Atm \ T (M ) [ Atm(') .
As Atm is infinite while W , T (M ), Agt and Atm(') are finite, such an injection exists.

We define a new model

M 0 = (W 0 , D 0 , A 0 , N 0 , V 0 ) with W 0 = W , N 0 = N and
where D 0 , V 0 and A 0 are defined as follows. For every i 2 Agt and for every

w 2 W : A 0 (i, w) = A(i, w) [ {f (i, w)}, D 0 (i, w) = D(i, w) [ 8 > < > : f (i, w) ^0 B @ p2A(i,w)\Atm D(i,w) (p _ ¬p) 1 C A 9 > = > ;
.

Moreover, for every p 2 Atm:

V 0 (p) = V(p) i f p 2 T (M ) [ Atm('), V 0 (p) = N (i, w) i f p = f (i, w), V 0 (p) = ; otherwise .
It is easy to verify that M 0 satisfies Condition (C1) and (C2) in Definition 3.8. Thus, M 0 is a finite NDAM. The rest of the proof consists in checking that, for every x 2 {GC, BC}, if M satisfies x then M 0 also satisfies x, which is straightforward, and that, (M, w) |= ' i↵ (M, w) |= '. We prove the latter by induction on the structure of '.

The case ' = p is immediate from the definition of V 0 . The boolean cases are straightforward. Let us prove the case ' = 4 i ↵. ()) Suppose (M, w) |= 4 i ↵. Then, we have ↵ 2 D(i, w). Hence, by the definition of D 0 , ↵ 2 D 0 (i, w). Thus, (M 0 , w) |= 4 i ↵.

(() Suppose (M 0 , w) |= 4 i ↵. Then, we have ↵ 2 D 0 (i, w). Since f (i, w) 6 2 Atm( 4i ↵), by the definition of D 0 , we have that,

↵ 6 = f (i, w) ^0 @ p2A(i,w)\Atm(D(i,w)) (p _ ¬p) 1 A .
Thus, ↵ 2 D(i, w) and, consequently, (M, w) |= 4 i ↵. Then, let us prove the case '

i = i . ()) Suppose (M, w) |= i . Then, we have Atm( ) ✓ A(i, w). Hence, by the definition of A 0 , Atm( ) ✓ A 0 (i, w). Thus, (M 0 , w) |= i . (() Suppose (M 0 , w) |= i . Then, we have Atm( ) ✓ A 0 (i, w). The definition of A 0 ensures that f (i, w) 6 2 Atm( ). Thus, Atm( ) ✓ A(i, w) and, consequently, (M, w) |= i . At last, let us prove the case ' = 2 i . (M, w) |= 2 i means that (M, u) |= for all u 2 N (i, w), which is equivalent to (M 0
, u) |= for all u 2 N 0 (i, w) by the induction hypothesis and the the fact that N 0 (i, w) = N (i, w). The latter means that (M 0 , w) |= 2 i . Now we have that (M, w) |= ' i↵ (M, w) |= '. Then, if M satisfies ', M 0 satisfies ' as well. ⇤

Equivalence between MABAs and NDAMs

The following lemma concerns the equivalence between MABA and NDAM.

Lemma 3.4 Let ' 2 L LDAA and X ✓ {GC, BC}. Then, ' is satisfiable for the class MABA X if and only if ' is satisfiable for the class NDAM X .

Proof The proof is almost identical to that of Lemma 7 in the appendix of [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF]. Here we only give a quick sketch. For the left-to-right direction, we prove the following weaker result: if ' is satisfiable for the class MABA X , then ' is satisfiable for the class QNDAM X . Then, by Lemma 3.2 and Lemma 3.3, we have that if ' is satisfiable for the class MABA X , then ' is satisfiable for the class NDAM X . For the right-to-left direction, we first transform the NDAM M = (W, D, A, N , V) into a non-redundant NDAM, where there are no identical worlds in W . Then we build a MABA from the latter. It is easy to prove that such transformations preserve satisfiability of '. ⇤

The following theorem is the main result of this section.

Theorem 3.1 Let ' 2 L LDAA and X ✓ {GC, BC}. Then, the following five statements are equivalent:

• ' is satisfiable for the class MABA X ,

• ' is satisfiable for the class NDAM X ,

• ' is satisfiable for the class QNDAM X , • ' is satisfiable for the class finite-QNDAM X ,

/ / NDAM X / / QNDAM X ✏ ✏ finite NDAM X / / O O finite QNDAM X O O o o
• ' is satisfiable for the class finite-NDAM X .

Proof The theorem is a direct consequence of Lemmas 3.2, 3.3 and 3.4. ⇤

Axiomatics

In this section, we define some variants of the LDAA logics and prove their soundness and completeness for their corresponding model classes.

We define the base logic LDAA to be the extension of classical propositional logic given by the following axioms and rule of inference:

2 i ' ^2i (' ! ) ! 2 i (K 2i ) 4 i ↵ ! 2 i ↵ (Int 4i,2i )
4 i ↵ ! i ↵ (Int 4i, i ) i ' $ p2Atm(') i p (AGPP) ' 2 i ' (Nec 2i )
For X ✓ {D 2i , T 2i }, let LDAA X be the extension of logic LDAA by every axiom in X, where,

¬(2 i ' ^2i ¬') ( D 2i ) 2 i ' ! ' (T 2i )
As usual, for every logic LDAA X with X ✓ {D 2i , T 2i } and for every ' 2 L LDAA , we write `LDAAX ' to mean that ' is deducible in LDAA X , which is defined as usual. We say that the set of formulas from

L LDAA is LDAA X - consistent if there are no formulas ' 1 , . . . , ' m 2 such that `LDAA X (' 1 ^. . . 'm ) ! ?. In particular, ' is LDAA X -consistent if {'} is LDAA X -consistent. Clearly, the logics LDAA {D2 i ,T2 i } and LDAA {T2 i } are identical since Axiom D 2i is deducible in LDAA {T2 i } .
Proof The proof is by induction on the structure of the formula '. For the cases ' atomic, Boolean, or of the form 2 i , the proof is standard by means of Proposition 4.1 and Lemma 4.2. The proof for the case ' = 4

i ↵ goes as follows:

4 i ↵ 2 w i↵ ↵ 2 D LDAAX (i, w) i↵ (M LDAAX , w) |= 4 i ↵. For the case ' = i ,
M LDAAX , 8p 2 Atm(↵), p 2 A LDAAX (i, w), which means Atm(↵) ✓ A LDAAX (i, w). For Condition (C2 ⇤ ), we have to prove that if ↵ 2 D LDAAX (i, w) then N LDAAX (i, w) ✓ ||↵|| M LDAA X . Suppose ↵ 2 D LDAAX (i,
4.1 Let X ✓ {D 2i , T 2i }. Then,
• LDAA X is sound and complete for the class NDAM {cf (x):x2X} ,

• LDAA X is sound and complete for the class MABA {cf (x):x2X} .

Relationship with Propositional Awareness

In this section, we build a connection between LDAA and the logic of propositional awareness (LPA), where the latter, first introduced in [START_REF] Joseph | Alternative semantics for unawareness[END_REF], is a special case of the logic of general awareness (LGA) by Fagin & Halpern [START_REF] Fagin | Belief, awareness, and limited reasoning[END_REF]. Specifically, we provide a polynomial, satisfiability preserving translation from the language of LPA to the language of LDAA. The language of LPA, denoted by L LPA (Atm, Agt), is defined by the following grammar:

' ::= p | ¬' | ' 1 ^'2 | B i ' | A i ' | X i '
, where p ranges over Atm and i ranges over Agt. When it is unambiguous from the context, we write L LPA instead of L LPA (Atm, Agt). At the semantics level, the logic of propositional awareness exploits awareness structures in which the awareness function is assumed to be propositional.

Definition 5.1 A propositional awareness model (PAM) is a tuple M = (⌦, ) , ⇢, ⇡) where,
• ⌦ is a non-empty set of states,

• ): Agt ⇥ ⌦ ! 2 ⌦ is a doxastic accessibility function, • ⇢ : Agt ⇥ ⌦ ! 2 Atm is a propositional awareness function, • ⇡ : Atm ! 2 ⌦ is a valuation function.
The class of propositional awareness models is denoted by PAM.

For a PAM M = (⌦, ), ⇢, ⇡) and s 2 ⌦, a pair (M, s) is called a pointed PAM. We write s ) i t for t 2 )(i, s). We say that a PAM M = (⌦, ), ⇢, ⇡) satisfies global consistency (GC) if, for every s 2 ⌦ and i 2 Agt, there is t 2 ⌦ such that s ) i t. We say that it satisfies belief correctness (BC) if, for every s 2 ⌦ and i 2 Agt, s ) i s. For every X ✓ {GC, BC}, we note PAM X the class of propositional awareness models satisfying every property in X. The semantic interpretation of formulas in L LPA relative to a pointed PAM is defined as follows.

Definition 5.2 Let M = (⌦, ), ⇢, ⇡) be a PAM and s 2 ⌦. Then, (M, s) |= p () s 2 ⇡(p), (M, s) |= ¬' () (M, s) 6 |= ', (M, s) |= ' ^ () (M, s) |= ' and (M, s) |= , (M, s) |= B i ' () 8t 2 ⌦, if s ) i t then (M, t) |= ', (M, s) |= A i ' () Atm(') ✓ ⇢(i, s), (M, s) |= X i ' () (M, s) |= B i ' and (M, s) |= A i '. We translate formulas of L LPA (Atm, Agt) into formulas of L LDAA (Atm, Agt)
via the following translation function tr 1 : L LPA (Atm, Agt) ! L LDAA (Atm, Agt):

tr 1 (p) = p for p 2 Atm, tr 1 (¬') = ¬tr 1 ('), tr 1 (' 1 ^'2 ) = tr 1 (' 1 ) ^tr 1 (' 2 ), tr 1 (A i ') = i tr 1 ('), tr 1 (B i ') = 2 i tr 1 ('), tr 1 (X i ') = p2Atm(') i p ^2i tr 1 (').
The interesting aspect of the previous translation is that the LPA notion of explicit belief is mapped into the combination of implicit belief plus awareness in our logic LDAA, and not directly into the LDAA notion of explicit belief. This highlights that the two notions of explicit belief do not capture the same type of epistemic attitude. While the LDAA notion represents an agent's actual belief which is active in his working memory and instantly accessible to him (we assume an agent's belief base to be a rough approximation of his working memory), the LPA notion is aimed at capturing the agent's relevant beliefs that are built from his actual vocabulary. 2As the following theorem highlights, the translation is satisfiability preserving.

Theorem 5.1 Let ' 2 L LPA and X ✓ {GC, BC}. Then, ' is satisfiable for the class PAM X if and only if tr 1 (') is satisfiable for the class NDAM X .

Proof We first prove a weaker result of the left-to-right direction, i.e., if ' is satisfiable for the class PAM X , then tr 1 (') is satisfiable for the class QNDAM X . Let M = (⌦, ), ⇢, ⇡) be a PAM and let s 2 ⌦ such that (M, s) |= '. We build the corresponding M 0 = (W, D, A, N , V) as follows:

• W = ⌦, • 8i 2 Agt and 8s 2 ⌦, D(i, s) = {p _ ¬p : (M, s) |= A i p}, • 8i 2 Agt and 8s 2 ⌦, A(i, s) = ⇢(i, s), • 8i 2 Agt and 8s 2 ⌦, N (i, s) = )(i, s), • 8p 2 Atm, V(p) = ⇡(p).
We prove that M 0 is a quasi-NDAM by showing that it satisfies Condition (C1 ⇤ ) and (C2 ⇤ ) in Definition 3.11.

For Condition (C1 ⇤ ), by the semantics of PAM and the definitions of D(i, s) and A(i, s), it is easy to show that, Atm D(i, s) = A(i, s) for every i 2 Agt and every s 2 W , which implies Atm D(i, s) ✓ A(i, s).

For Condition (C2 ⇤ ), by the definition of D(i, s), there are only tautologies in it. So we have that

T tr1(')2D(i,w) ||tr 1 (')|| M = W . Then, clearly, Condition (C2 ⇤ ) is satisfied.
It is easy to verify that, for every x 2 {GC, BC}, if M satisfies x then M 0 satisfies it as well.

By induction on the structure of ', we prove that, for all s 2 ⌦, (M, s) |= ' i↵ (M 0 , s) |= tr 1 ('). For the case ' = p and the boolean cases ' = ¬ and ' = 1 ^ 2 , it is straightforward. Now we consider the case ' = A i . Suppose (M, s) |= A i . By the semantics of PAMs, it is equivalent to Atm( ) ✓ ⇢(i, s). By the definition of A(i, s) and the function tr 1 , the latter is equivalent to Atm tr 1 ( ) ✓ A(i, s). And in turn the latter means (M 0 , s) |= i tr 1 ( ). Then, by the function tr 1 , the latter is equivalent to (M 0 , s) |= tr 1 (A i ). Let us consider the case ' = B i . Suppose (M, s) |= B i . By the induction hypothesis, we have

|| || M = ||tr 1 ( )|| M 0 . (M, s) |= B i means that )(i, s) ✓ || || M .
By the definition of N (i, s) and the fact that

|| || M = ||tr 1 ( )|| M 0 , the latter it equivalent to N (i, s) ✓ ||tr 1 ( )|| M 0 , which is equivalent to (M 0 , s) |= 2 i tr 1 ( ). The latter means (M 0 , s) |= tr 1 (B i
) by the definition of the function tr 1 .

Finally, let us consider the case ' = X i . Suppose (M, s) |= X i . Given the fact that X i is equivalent to A i ^Bi and A i is equivalent to V p2Atm( ) A i p, by the previous cases, it means that, (M 0 , s) |= V p2Atm( ) A i p ^2i tr 1 ( ). By the function tr 1 , the latter is equivalent to (M 0 , s) |= tr 1 (X i ). Thus, we conclude that (M, s) |= ' i↵ (M 0 , s) |= tr 1 (') for all s 2 ⌦. Then we have that, if ' is satisfiable for the class PAM X , then tr 1 (') is satisfiable for the class QNDAM X . By Theorem 3.1, it follows that, if ' is satisfiable for the class PAM X , then tr 1 (') is satisfiable for the class NDAM X .

Then we prove the right-to-left direction. Let M = (W, D, A, N , V) be a NDAM. We build the model M 0 = (⌦, ), ⇢, ⇡) as follows:

• ⌦ = W , • 8i 2 Agt and 8w 2 W , )(i, w) = N (i, w), • 8i 2 Agt and 8w 2 W , ⇢(i, w) = A(i, w), • 8p 2 Atm, ⇡(p) = V(p).
Obviously, M 0 is a PAM. And it is easy to verify that, for every x 2 {GC, BC}, if M satisfies x then M 0 satisfies it as well.

The next step is to prove that for all w 2 W , (M, w) |= tr 1 (') i↵ (M 0 , w) |= '.

The case ' = p and the boolean cases are straightforward.

Let us consider the case ' = A i . Suppose (M, w) |= tr 1 (A i ). By the semantics of NDAMs and the function tr 1 , it is equivalent to Atm( ) ✓ A(i, w). By the definition of ⇢(i, w), the latter is equivalent to Atm( ) ✓ ⇢(i, w). Then by the semantics of PAMs, the latter is equivalent to (M

)(i, w) ✓ || || M 0 , which is equivalent to (M 0 , w) |= B i . Finally, let us consider the case ' = X i . Suppose (M, w) |= tr 1 (X i ). Given the fact that X i is equivalent to B i ^Ai and A i is equivalent to V p2Atm( ) A
i p, by the previous cases, it is equivalent to (M 0 , w) |= B i ^Ai , which in turn is equivalent to (M 0 , w) |= X i . Thus, we conclude that (M, w) |= tr 1 (') i↵ (M 0 , w) |= ' for all w 2 W . Therefore, if tr 1 (') is satisfiable for the class NDAM X , then ' is satisfiable for the class PAM X . ⇤ Theorem 5.1 shows that the translation of a LPA-formula is satisfiable if and only if the LPA-formula is satisfiable too. This highlights that L LDAA is at least as expressive as L LPA . We do not know whether they have the same expressivity. What we can a rm is that the formula ¬4 i (p ^p) ^2i p ^ i p is satisfiable in the class NDAM, but it cannot be satisfied in the class PAM, if we translate 4 i , 2 i , and i into X i , B i , and A i , respectively. Again this shows that the LPA notion of explicit belief and the LDAA notion of explicit belief capture epistemic attitudes of di↵erent nature.

Relationship with General Awareness

In the previous section, we have studied the relationship between our logic LDAA and the logic of propositional awareness. We have provided a polynomial embedding of the latter into the former.

As we have emphasized in the introduction, the notion of propositional awareness is generally distinguished from general awareness introduced for the first time in [START_REF] Fagin | Belief, awareness, and limited reasoning[END_REF]. Unlike propositional awareness whereby an agent can only be "primitively" aware about atomic propositions and awareness about complex formulas is generated from it, in general awareness an agent can also be "primitively" aware about complex formulas. On the conceptual level, the crucial di↵erence between propositional and general awareness is that the former captures a 'relevance-based' form of awareness, while the latter is closer to an 'accessibility-based' interpretation of the notion of awareness. On the one side, propositional awareness corresponds to all propositions that are relevant for the agent in the actual situation and which constitute the agent's actual vocabulary. From a cognitive point of view, being propositionally aware of a certain fact or proposition means imagining it, thinking about it, holding a mental representa-tion of it. On the other side, general awareness corresponds to all facts whose truth is instantly accessible to the agent. Being generally aware of a certain fact means being able to instantly assess whether this fact is true, given the information at our disposal. This second conception is made explicit by Fagin & Halpern, according to whom the notion of awareness is "...open to a number of interpretations. One of them is that an agent is aware of a formula if he can compute whether or not it is true in a given situation within a certain time or space bound" [7, p. 41]. 3In this section, we explore the connection between the logic LDAA and Fagin & Halpern's logic of general awareness. We will provide a polynomial embedding of the former into the latter and, thanks to this embedding, we will obtain a complexity result for the LDAA-satisfiability checking problem.

The logic of general awareness (LGA) has the same language as the logic of propositional awareness we introduced in Section 5, that is, L LGA = L LPA . Nonetheless, it di↵ers at the semantic level, where formulas are interpreted with respect to the following notion of general awareness model. Definition 6.1 A general awareness model (GAM) is a tuple M = (⌦, ), ⇢, ⇡) where,

• ⌦ is a non-empty set of states,

• ): Agt ⇥ ⌦ ! 2 ⌦ is a doxastic accessibility function, • ⇢ : Agt ⇥ ⌦ ! 2 L
LGA is a general awareness function,

• ⇡ : Atm ! 2 ⌦ is a valuation function.
The class of general awareness models is denoted by GAM.

For every X ✓ {GC, BC}, we note GAM X the class of general awareness models satisfying every property in X, where GC and BC for GAMs are defined in the same way as for PAMs.

The only di↵erence between propositional awareness models and general awareness models is that in the latter the awareness function is about generic formulas while in the former it is only about atomic propositions. The interpretation of formulas in L LGA relative to a pointed GAM is exactly as in Definition 5.2 except for the awareness operators which are interpreted by the following rule: s). In order to relate our logic LDAA to LGA, let us extend the set of atomic formulas as follows:

(M, s) |= A i ' () ' 2 ⇢(i,
Atm + = Atm [ {aw (i,p) : i 2 Agt and p 2 Atm},
where aw (i,p) is a special atom denoting the fact that agent i is propositionally aware of p. Such special atoms are crucial for the embedding since they allow us to "simulate" the notion of propositional awareness in the context of the general awareness framework. Note that we have made a conceptual shift when moving from LPA to LGA, since in LPA the operator A i represents propositional awareness, while in LGA the same operator represents general awareness and the special atoms aw (i,p) are used to represent propositional awareness.

We translate formulas of LDAA into formulas of LGA via the following translation function tr 2 : L LDAA (Atm, Agt) ! L LGA (Atm + , Agt):

tr 2 (p) = p for p 2 Atm, tr 2 (¬') = ¬tr 2 ('), tr 2 (' 1 ^'2 ) = tr 2 (' 1 ) ^tr 2 (' 2 ), tr 2 (4 i ↵) = X i tr 2 (↵) ^p2Atm(↵) aw (i,p), tr 2 (2 i ') = B i tr 2 ('), tr 2 ( i ') = p2Atm(') aw (i,p).
For every set of formulas ✓ L LDAA (Atm, Agt), we slightly abuse notation and define tr 2 ( ) = S '2 tr 2 (') . As the previous translation indicates, the LDAA notions of implicit belief and propositional awareness are mapped into the corresponding LGA notions. The LDAA notion of explicit belief is mapped into LGA explicit belief plus propositional awareness, represented by the special atoms aw (i,p). In this sense, the LDAA notion of explicit belief is stronger than the LGA notion. This is due to the fact that in LDAA propositional awareness and explicit belief are logically related since the former is computed from the latter, whereas in LGA explicit belief is logically related to general awareness but is not logically related to propositional awareness. Indeed, in LGA there is no connection between the explicit belief operator X i and the propositional awareness atoms aw (i,p). A more thoughtful discussion on this conceptual di↵erence will be given in Section 7. We have the following embedding theorem. Theorem 6.1 Let ' 2 L LDAA (Atm, Agt) and X ✓ {GC, BC}. Then, ' is satisfiable for the class NDAM X if and only if tr 2 (') is satisfiable for the class

GAM X .
Proof We first prove the left-to-right direction.

Suppose M = (W, D, A, N , V) is a NDAM and w 2 W such that (M, w) |= '. We build the GAM M 0 = (⌦, ), ⇢, ⇡) as follows:

• ⌦ = W , • for every w 2 ⌦, ) (i, w) = {v 2 ⌦ : v 2 N (i, w)},
• for every w 2 ⌦, ⇢(i, w) = tr 2 D(i, w) ,

• ⇡(p) = V(p) for each p 2 Atm,

• ⇡ aw (i,p) = {w 2 W : p 2 A(i, w)} for each i 2 Agt and w 2 W .

It is easy to verify that M 0 is a general awareness structure and that, for every x 2 {GC, BC}, if M satisfies x then M 0 satisfies it as well.

By induction on the structure of ', we are going to show that (M, w) |= ' if and only if (M 0 , w) |= tr 2 ('). The atomic case, boolean cases and case ' = i are straightforward and we do not need to prove them. Let us prove the case , w) |= tr 2 ('), since we supposed (M, w) |= '. As for the right-to-left direction, we are going to prove a weaker result: if tr 2 (') is satisfiable for the class GAM X then ' is satisfiable for the class QNDAM X . Let M = (⌦, ), ⇢, ⇡) be a GAM and s 2 ⌦ such that (M, s) |= tr 2 (').

' = 4 i ↵. ()) (M, w) |= 4 i ↵ means ↵ 2 D(i,
We build the structure M 0 = (W, D, A, N , V) as follows:

• W = ⌦, • for every s 2 ⌦ and i 2 Agt, D(i, s) = {↵ 2 L LDAA :)(i, s) ✓ ||tr 2 (↵)|| M , tr 2 (↵) 2 ⇢(i, s) and 8p 2 Atm, (M, s) |= aw (i,p)}, • for every s 2 ⌦ and i 2 Agt, N (i, s) =)(i, s), • for every s 2 ⌦ and i 2 Agt, A(i, s) = p 2 Atm : s 2 ⇡ aw (i,p) , • V(p) = ⇡(p) for p 2 Atm.
It is easy to verify that M 0 belongs to the class QNDAM and that, for every x 2 {GC, BC}, if M satisfies x then M 0 satisfies it as well.

By induction on the structure of ', we are going to show that (M, s) , s) |= ', since we supposed (M, s) |= tr 2 ('). We have proved that if tr 2 (') is satisfiable for the class GAM X , then ' is satisfiable for the class QNDAM X . From Theorem 3.1, it follows that if tr (') is satisfiable for the class GAM X , then ' is satisfiable for the class NDAM X . ⇤

|=
In the light of Theorems 3.1 and 6.1, we have that, for every formula ' 2 L LDAA (Atm, Agt), ' is satisfiable for the class MABA X if and only if tr 2 (') is satisfiable for the class GAM X .

In [START_REF] Ågotnes | Full and relative awareness: a decidable logic for reasoning about knowledge of unawareness[END_REF], it is proved that the satisfiability problem for the logic of general awareness is in PSPACE, even in the case in which every accessibility relation )

i is assumed to be reflexive. The proof relies on a tableau-based PSPACE satisfiability checking procedure. Ågotnes & Alechina's tableau-based method can be easily adapted to show that the satisfiability problem of the logic LGA interpreted over general awareness structures whose accessibility relations ) i are assumed to be serial is also in PSPACE. In the light of this observation, we get the following complexity result. Theorem 6.2 Let X ✓ {GC, BC}. Then, checking satisfiability of formulas in L LDAA (Atm, Agt) relative to the class NDAM X (resp. MABA X ) is a PSPACE-complete problem.

Proof Theorem 6.1 guarantees that the translation tr 2 provides a polynomialtime reduction of the satisfiability problem for formulas in L LDAA relative to the class NDAM X (resp. MABA X ) to the satisfiability problem of formulas in L LGA relative to the class GAM X . Since the latter problem is in PSPACE, it follows that the former problem is also in PSPACE. PSPACE-hardness follows from known PSPACE-hardness results for multimodal logic K n , KD n and KT n [START_REF] Halpern | A guide to completeness and complexity for modal logics of knowledge and belief[END_REF]. ⇤

LPA LDAA LGA

Polynomial embedding Polynomial embedding LGA. In the following section we discuss the relationship between the three frameworks and justify the two translations tr 1 and tr 2 from a conceptual perspective.

Discussion

In this section, we provide an intuitive explanation of the two embeddings of LPA into LDAA and of LDAA into LGA given in Sections 5 and 6. Moreover, we elucidate some important di↵erences between the three frameworks in relating explicit belief to implicit belief and awareness. 1 outlines the properties of the concepts of awareness, explicit belief and implicit belief in the three frameworks. In LPA and LGA the concepts of awareness and implicit belief are primitive and the concept of explicit belief is defined from them. On the contrary, in LDAA the only primitive concept is explicit belief, while awareness and implicit belief are computed from it. Moreover, LPA and LDAA only consider propositional awareness, while LGA is conceptually richer as it can easily combine general awareness with propositional awareness, by means of the special atoms aw (i,p). We recall that propositional awareness captures a 'relevance-based' form of awareness, whereas general awareness captures an 'accessibility-based' form. The former corresponds to an agent's mental vocabulary, the propositions that are relevant for him in a given situation and about which the agent is thinking. General awareness corresponds to the facts whose truth is accessible to the agent, for which the agent can instantly assess whether they are true. Being generally aware of a fact implies no cost of time and computation for inferring whether the fact is true.

Conceptual justification of the translations Table

LPA

LGA LDAA We have shown that (i) the LPA notions of propositional awareness and im-plicit belief are directly mapped into the LDAA notions of propositional awareness and implicit belief, and (ii) the LDAA notions of propositional awareness and implicit belief are directly mapped into the LGA notions of propositional awareness and implicit belief. As for explicit belief, there is no direct correspondence between LPA, LGA and LDAA as it has di↵erent meanings and properties in the three frameworks. In particular, the LPA notion of explicit belief is mapped into the combination of propositional awareness and implicit belief in LDAA, and the LDAA notion is mapped into the combination of explicit belief and propositional awareness in LGA.

Awareness

LGA defines explicit belief from general awareness and implicit belief. Like LDAA, LGA views explicit belief as a belief available in the agent's mind and instantly accessible to him. In particular, according to the LGA and LDAA interpretation, having an explicit belief ↵ means being able to instantly ascertain that ↵ is true. It presupposes that the agent to be modeled is resourcebounded and is not logical omniscient, since not all facts that the agent can deduce from his explicit (instantly accessible) beliefs are instantly accessible to him. Indeed, deduction and, more generally inference, takes time so that not all deducible facts are instantly accessible to the agent. Therefore, according to

LGA, an agent's explicit beliefs are not necessarily closed under deduction. 4In LPA explicit belief is defined from propositional awareness together with implicit belief and is viewed as an agent's relevant belief, as a belief which is built from the agent's vocabulary. In LPA the agent's explicit beliefs are deductively closed within the scope of his propositional awareness (i.e., with respect to his actual vocabulary). Specifically, in LPA, all facts that are deducible from the agent's explicit beliefs and whose atoms are parts of the agent's vocabulary are explicitly believed by the agent. For instance, LPA satisfies closure under logical consequence within the scope of the agent's vocabulary: if is a logical consequence of the facts ' 1 , . . . , ' k , the agent explicitly believes each of these facts and the atoms that does not share with these facts are all included in the agent's vocabulary, then the agent explicitly believes as well. That is, the following rule of inference preserves validity in LPA (while it does not in LGA):

(' 1 ^. . . ^'k ) ! (X i ' 1 ^. . . ^Xi ' k ^Vp2Atm( )\Atm({'1,...,' k }) A i p) ! X i (1)
This form of local deductive closure for explicit belief should be kept distinct from global deductive closure for implicit belief which is shared altogether by LPA, LGA and LDAA.

Given the conceptual similarity between LDAA-explicit belief and LGA-explicit belief, one would expect the former to directly map into the latter. But, in LDAA propositional awareness is computed from explicit belief. In other words, in LDAA relevance is grounded on accessibility: what is relevant for an agent (i.e., the agent's actual vocabulary) is computed from the beliefs that are instantly accessible to him. The latter is not the case in LGA in which explicit belief is defined from implicit belief and general awareness, but there is no connection between explicit belief and propositional awareness represented by the special atoms aw (i,p). In LGA an agent can have propositions in his vocabulary that do not appear in any of his explicit beliefs. In formal terms, it might be the case that (M, s) |= aw (i,p) for some pointed GAM (M, s) but p 6 2 Atm(') for every ' such that (M, s) |= X i '. In this sense, LDAA-explicit belief is stronger than LGA-explicit belief. This explains why in Section 6 LDAA-explicit belief is translated into LGA-explicit belief plus the fact that all propositions in the belief are part of the agent's propositional awareness.

The concept of explicit belief Let us explain in more detail how explicit belief relates to awareness and implicit belief in the three frameworks.

In LPA and LGA explicit belief is defined in terms of awareness and implicit belief. Therefore, the following formula is valid for the class PAM (resp.

GAM):

X i ' $ (B i ' ^Ai '). (2)
This means that explicit belief is coextensive with the intersection of implicit belief and awareness, as highlighted in Figure 3a. In LDAA only the left-to-right direction of the equivalence holds (i.e., explicit belief implies implicit belief and awareness). Specifically, the following formula is valid for the class MABA:

4 i ↵ ! (2 i ↵ ^ i ↵). (3)
But the formula (2 i ↵ ^ i ↵) ! 4 i ↵ is not valid for the class MABA. To show the latter, in the light of Theorem 3.1, it su ces to exhibit a NDAM which invalidates the previous formula. Consider the pointed NDAM (M, w 1 ) such that M = (W, D, A, N , V) with

W = {w 1 , w 2 }, D(i, w 1 ) = D(i, w 2 ) = {p 1 , p 1 ! p 2 }, N (i, w 1 ) = N (i, w 2 ) = {w 2 }, V(p 1 ) = {w 1 , w 2 }, V(p 2 ) = {w 2 }, D(j, w k ) =
; for every j 6 = i and k 2 {1, 2}, N (j, w k ) = W for every j 6 = i and k 2 {1, 2}, V(q) = ; for every q 6 2 {p 1 , p 2 }.

Clearly, we have (M, w 1 ) |= 2 i p 2 ^ i p 2 but (M, w 1 ) |= ¬4 i p 2 . This means that in LDAA there are facts that are implicitly believed by an agent and of which the agent is propositionally aware, but that are not explicitly believed by him. Such facts are represented by the grey zone in Figure 3b.

This di↵erence between LDAA and the competing frameworks LPA and LGA is due to their diverging conceptions of the relationship between explicit belief and awareness. As we have emphasized above, LPA is a theory of relevancebased explicit belief and awareness, whereas LGA is a theory of accessibilitybased explicit belief and awareness. LDAA is a theory of accessibility-based explicit belief and relevance-based awareness, in which the notion of relevance for awareness is grounded on the notion of accessibility for explicit belief. Given this interpretation, in LDAA it makes perfect sense to assume that an agent can implicitly believe ↵ and be propositionally aware of ↵ without explictly believing ↵, simply because it has not yet inferred ↵ from his explicit beliefs. For example, suppose an agent explicitly believes each premise in {p 1 , p 2 , (p 2 ^p3 ) ! p 4 , p 1 ! p 3 }. Atom p 4 is part of the agent's vocabulary and the agent is thinking about it since it is included in one of his explicit beliefs thereby being relevant for him. 5 It is deducible from the agent's explicit beliefs through a sequence of two inference steps. For this reason the agent implicitly believes that p 4 . But since the agent has not deduced it yet, he does not believe it explicitly.

Being aware requires having an explicit belief Before concluding, we would like to shed further light on the connection between awareness and explicit belief in the three frameworks. LDAA satisfies the following two properties: (P1) if an agent is propositionally aware of an atom p, then he has an explicit belief about some formula involving p, (P2) if an agent has some explicit belief about the atom p, then he is propositionally aware of p.

LPA satisfies them too, while LGA does not. In particular, for every MABA (S, Cxt) the following holds: if (S, Cxt) |= i p then there exists ↵ such that p 2 Atm(↵) and (S,

Cxt) |= 4 i ↵, (4)
and for every pointed PAM (M, s), the following holds:

if (M, s) |= A i p then there exists ' such that p 2 Atm(') and (M, s) |= X i '.

We have ( 5) since both B i (p _ ¬p) and

A i p ! A i (p _ ¬p) are valid in the class PAM. Therefore, (M, w) |= A i p implies (M, s) |= X i (p _ ¬p).
We have (4) since in LDAA propositional awareness is computed from explicit belief. This excludes situations in which the agent thinks about a concept or a proposition without having available in his mind an explicit belief about it. More generally, in LDAA it is assumed that mere thinking and imagining are subordinate to the epistemic activity. Moreover, the following LDAA-formula is valid for the class MABA:

4 i ↵ ! i p if p 2 Atm(↵), (6)
and the following LPA-formula is valid for the class PAM:

X i ' ! A i p if p 2 Atm('). (7)
The validity [START_REF] Daniel | Précis of the intentional stance[END_REF] excludes situations in which an agent has some belief about p active in his mind and, at the same time, he does not think about p. Such situations are not possible since in LDAA having an explicit about a proposition p makes p relevant for the agent and induces the agent to think about it.

Dynamic Extensions

This section focuses on some extensions of the logic LDAA capturing di↵erent types of belief dynamics and awareness dynamics in a multi-agent setting.

The logics in the LDA family introduced in [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF] allow us to model common ground change and private belief base change. These properties are inherited altogether by the LDAA logics naturally. For private belief base change, the LDAA setting retains the virtue of the LDA setting by o↵ering a "parsimonious" account of private informative actions whereby duplication of the original epistemic model in the style of Gerbrandy & Groeneveld [START_REF] Gerbrandy | Reasoning about information change[END_REF] is not needed. We only need to add a piece of information to an agent's belief base, while keeping the other agents' belief bases unchanged, and then recompute the agent's doxastic accessibility relation. The novelty of LDAA compared to LDA is the account of awareness dynamics. In LDAA, the latter depends on belief base dynamics, since an agent's awareness is grounded on the agent's belief base. This distiguishes the LDAA approach from existing approaches to awareness change such as [START_REF] Van Benthem | The dynamics of awareness[END_REF] in which the notion of awareness is taken as a primitive and its dynamics are independent of belief dynamics.

In the rest of this section, we first investigate the extension of LDAA by public announcements. Then, we present the extension of LDAA by private belief base expansion. Complexity results for these extensions are provided.

Public Announcements

In order to represent how public announcements influence the agents' common ground, we extend the language L LDAA (Atm, Agt) by modal operators of the form ['!], thereby obtaining the following language L LDAA PA (Atm, Agt):

' ::= ↵ | ¬' | ' 1 ^'2 | 2 i ' | i ' | ['!]
, where i ranges over Agt, ↵ ranges over L 0 , and LDAA PA stands for "Logic of Doxastic Attitudes with Awareness and Public Announcements".

For simplicity, we write L LDAA PA instead of L LDAA PA (Atm, Agt). The formula ['!] is read " holds after the public announcement of '". Like in standard public announcement logic PAL [START_REF] Plaza | Logics of public communications[END_REF], public announcements are assumed to be truthful, i.e., an announcement is executable if and only if the formula to be announced is true. As usual, h'!i is the abbreviation of ¬['!]¬ , which means "the public announcement of ' is executable and will hold after the public announcement". We generalize the function computing the atoms occurring in a formula in the expected way: where Cxt '! = {S 0 2 Cxt : (S 0 , Cxt) |= '}. The intuition is that is the consequence of the public announcement of ' if and only if, if ' is true, then is going to be true after restricting the agents' common ground to be the states satisfying '.

The semantics so defined guarantees that the agents' implicit beliefs are changed, as a consequence of a public announcement, whilst their explicit beliefs and awareness remain intact. This corresponds to the concept of "implicit observation" in the sense of van Benthem & Velásquez-Quesada [START_REF] Van Benthem | The dynamics of awareness[END_REF]. It is implicit because, although it removes worlds thereby a↵ecting the agents' implicit beliefs, it does not modify their explicit beliefs in the preserved ones. This concept of implicit observation is useful for AI applications in which multiple artificial agents interact in a multi-agent system. Each agent is identified with its private belief base and share with the other agents a common body of information (the common ground). For example, two autonomous vehicles 1 and 2 can share some driving rules prescribing that a vehicle must stop whenever the tra c light is red (i.e., red ! oughtStop) and a vehicle is allowed to continue whenever the tra c light is green (i.e., green ! allowContinue). These two rules are parts of the agents' common ground and should be kept distinct from the agents' private information determined by their visibility conditions. For example, suppose agent 1 is in front of the tra c light so that he can see that it is red, whilst agent 2 is far from it and cannot see its colour. This means that agent 1 has the proposition red in its belief base, whilst agent 2 does not have it. Suppose a new rule is publicly announced by an external agent (e.g., the system designer) prescribing that a vehicle must slow down whenever the tra c light flashes orange (i.e., flashOrange ! OughtSlowDown). We can imagine the system is centralized so that agents 1 and 2 correctly perceive the external agent's message and have common knowledge of this. As a consequence, the new rule is added to the common ground thereby modifying their implicit beliefs. We can represent this scenario by the MABA (S, Cxt)

with S = (B 1 , B 2 , A 1 , A 2 , V ) such that B 1 = A 1 = V = {red }, B 2 = A 2 = ;
and Cxt = {S 0 2 S : S 0 |= (red ! oughtStop) ^(green ! allowContinue)}. The result of the public announcement (flashOrange ! OughtSlowDown)! is the new MABA (S, Cxt (flashOrange!OughtSlowDown)! ) such that:

Cxt (flashOrange!OughtSlowDown)! ={S 0 2 S : S 0 |= (red ! oughtStop)( green ! allowContinue)( flashOrange ! OughtSlowDown)}.
Note that the definition of public announcement is compatible with the class MABA {BC} given the following fact: if (S, Cxt) |= ' and (S, Cxt) 2 MABA {BC} , then S 2 Cxt '! and (S 0 , S 0 ) 2 R i for every S 0 2 Cxt '! . However, public announcements may not preserve the property of global consistency for the reason that, restricting the common ground to the '-situations could empty an agent's set of doxastically accessible states. Consequently, the semantics for L LDAA PA is compatible with the classes MABA and MABA {BC} , but incompatible with the class MABA {GC} . Like in PAL, we have reduction principles for the dynamic operators ['!].

Proposition 8.1 The following formulas are valid relative to the class MABA:

['!]p $ (' ! p) ['!]¬ $ (' ! ¬['!] ) ['!]( 1 ^ 2 ) $ (['!] 1 ^['!] 2 ) ['!]2 i $ (' ! 2 i ['!] ) ['!]4 i ↵ $ (' ! 4 i ↵) ['!] i $ (' ! i )
Proof The first three validities are proved in the same way as in PAL. The proof of the fourth validity is analogous to the proof of the corresponding validity in the proof of [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF]Proposition 6]. The fifth and sixth validities are clear since public announcements do not a↵ect the agents' belief bases. ⇤

The first four validities are standard reduction principles of PAL. The fifth and the sixth are reduction principles for explicit belief and awareness, respectively. They highlight that an agent's explicit beliefs and awareness are not a↵ected by public announcements.

With the equivalences in Proposition 8.1, we are able to find for every formula of the language L LDAA PA an equivalent formula of the language L LDAA by way of a mapping red LDAA PA . The function red LDAA PA iteratively applies the equivalences of Proposition 8.1, so that every operator ['!] is moved inside the formula and finally eliminated by the first equivalence of Proposition 8.1.

Definition 8.2

The mapping red LDAA PA is inductively defined as follows:

1

.red LDAA PA (p) = p 2.red LDAA PA (4 i ↵) = 4 i red LDAA PA (↵) 3.red LDAA PA (¬') = ¬red LDAA PA (') 4.red LDAA PA (' ^ ) = red LDAA PA (') ^red LDAA PA ( ) 5.red LDAA PA (2 i ') = 2 i red LDAA PA (') 6.red LDAA PA ( j ') = p2Atm(') j p 7.red LDAA PA (['!]p) = red LDAA PA (' ! p) 8.red LDAA PA (['!]¬ ) = red LDAA PA (' ! ¬ ['!] ) 9.red LDAA PA ['!]( 1 ^ 2 ) = red LDAA PA (['!] 1 ^['!] 2 ) 10.red LDAA PA (['!]2 i ) = red LDAA PA (' ! 2 i ['!] ) 11.red LDAA PA (['!]4 i ↵) = red LDAA PA (' ! 4 i ↵) 12.red LDAA PA (['!] i ) = red LDAA PA (' ! i ) 13.red LDAA PA (['!][ !] ) = red LDAA PA ['!]red LDAA PA ([ !] )
Note that the last item in the definition of red LDAA PA is necessary for the case of iteration of public announcements.

↵]¬ ) = red LDAA PBE (¬[+ i ↵] ) 9.red LDAA PBE [+ i ↵]( 1 ^ 2 ) = red LDAA PBE ([+ i ↵] 1 ^[+ i ↵] 2 ) 10.red LDAA PBE ([+ i ↵]2 j ') = red LDAA PBE (2 j ') if i 6 = j red LDAA PBE ([+ i ↵]2 i ') = red LDAA PBE 2 i (↵ ! ') 11.red LDAA PBE ([+ i ↵]4 j ) = red LDAA PBE (4 j ) if i 6 = j or ↵ 6 = red LDAA PBE ([+ i ↵]4 i ↵) = > 12.red LDAA PBE ([+ i ↵] j ') = red LDAA PBE ( j ') if i 6 = j red LDAA PBE ([+ i ↵] i ') = red LDAA PBE 0 @ p2Atm(')\Atm(↵) i p 1 A otherwise 13.red LDAA PBE ([+ i ↵] [+ j ]') = red LDAA PBE [+ i ↵]red LDAA PBE ([+ j ]')
The following proposition is proved by induction on the structure of ' in a way similar to Proposition 8.2. Proposition 8.4 Let ' 2 L LDAA PBE . Then, ' $ red LDAA PBE (') is valid with respect to the class MABA.

The fact that checking satisfiability for formulas in L LDAA PBE is in PSPACE follows from (i) the fact that satisfiability checking for formulas in L LDAA is in PSPACE (Theorem 6.2) and (ii) the fact that red LDAA PBE provides an e↵ective procedure for reducing a formula ' in L LDAA PBE into an equivalent formula red LDAA PBE (') in L LDAA whose size is polynomial in the size of '. PSPACEhardness follows from the fact that the language L LDAA PBE is a conservative extension of L LDAA (i.e., every valid formula of the latter is also a valid formula of the former).

Discussion

In this section, we are going to focus on some conceptual aspects of the logic LDAA PBE, namely, how becoming aware of a proposition requires expanding the belief base with a formula about this proposition and how to represent "explicit" public announcement in opposition to "implicit" public announcement, as defined in Section 8.1.

Becoming aware requires acquiring an explicit belief LDAA PBE captures the subtle connection between awareness and explicit belief from a dynamic perspective. This is the main novelty compared to the extension of the logic LDA by private belief expansion presented in [START_REF] Lorini | Rethinking epistemic logic with belief bases[END_REF] which does not contemplate awareness.

The following two properties are the dynamic counterparts of the static properties P1 and P2 discussed in Section 7:

(P3) an agent cannot become propositionally aware of an atom p, unless he expands his belief base with a formula involving p, (P4) if an agent expands his belief base with some information about the atom p, then he becomes propositionally aware of p.

LDAA PBE satisfies both properties. Indeed, the following two formulas are valid for the class MABA:

¬ ¬ i p ^[+ i ↵] i p if p 6 2 Atm(↵), (8)
[+ i ↵] i p if p 2 Atm(↵). (9)
The previous two properties P3 and P4 are justified on the same grounds as properties P1 and P2. Since in LDAA PBE, an agent's propositional awareness is computed from his belief base, there is no way to become propositionally aware of an atom p without adding to the belief base a new piece of information about p. Conversely, adding to the belief base a new piece of information about p makes the agent propositionally aware of p.

It is worth noting that such dynamic properties are not satisfied by LGA. Indeed, as highlighted in [START_REF] Van Benthem | The dynamics of awareness[END_REF], in LGA awareness dynamics and explicit belief dynamics are not necessarily related: an agent can become aware of a formula without changing his explicit beliefs. 6k-level "explicit" public announcement As we emphasized in Section 8.1, public announcement is analogous to the notion of "implicit observation" studied in [START_REF] Van Benthem | The dynamics of awareness[END_REF]: an implicit observation only modifies the agents' common ground, and consequently their implicit beliefs, without a↵ecting their explicit beliefs and awareness. In LDAA PBE we can represent a notion of k-level "explicit" public announcement that directly operates on the agents' belief bases and generates common belief up to a certain finite level k of both explicit and implicit type.

In order to define k-level "explicit" public announcement in LDAA PBE, we first need to define explicit shared belief, denoted by the symbol ESB:

ESB ↵ def = î2Agt 4 i ↵.
Then, we need to define explicit mutual belief in an inductive way, for k 0:

EMB 0 ↵ def = ↵, EMB k+1 ↵ def = ESB EMB k ↵.
From explicit mutual belief we can define k-level explicit common belief for k 0, denoted by the symbol ECB k , as the conjunction of all mutual beliefs between level 1 and level k + 1:

ECB k ↵ def = 1hk+1 EMB h ↵.
Notice that 0-level explicit common belief (i.e., ECB 0 ↵) is the same as explicit shared belief (i.e., ESB ↵).

We have everything we need to define the k-level "explicit" public announcement operator, denoted by the symbol [!! k ↵]: . . . [+ (n) EMB k ↵]', where is any permutation of the set of agents Agt = {1, . . . , n}, by virtue of the fact that in LDAA PBE the order of execution of some private belief expansion operations does not matter. The latter is a consequence of the fact that a single private belief expansion operation merely consists in adding a piece of information to an agent's belief base, while keeping the other agents' belief bases unchanged. Therefore, its position in a sequence of private belief expansion operations is irrelevant. 7 In other words, k-level explicit public announcement of ↵ just consists in all agents expanding their belief bases with the information that ↵ is mutual belief, for every level between 0 and k.

[!! k ↵]'
It is easy to verify that k-level explicit public announcement of ↵ generates k-level explicit common belief of ↵, k-level implicit common belief of ↵ and (k 1)-level implicit common belief about shared awareness of ↵. Indeed, the following three formulas are valid in LDAA PBE:

[!! k ↵]ECB k ↵, [!! k ↵]ICB k ↵, [!! k ↵]ICB k 1 î2Agt i ↵ if k > 0,
where the k-level implicit common belief operator ICB k is defined as follows:

ICB k ↵ def = 1hk+1 IMB h ↵,
after having defined implicit mutual belief (i.e., IMB k ) from implicit shared belief (i.e., ISB) in the following way:

ISB ↵ def = î2Agt 2 i ↵, IMB 0 ↵ def = ↵, IMB k+1 ↵ def = ISB IMB k ↵.
The LDAA PBE framework cannot handle unbounded explicit public announcement since its underlying language is finitary and defining it as an abbrevation would require an infinitary language. We leave for future investigation an extension of the LDAA PBE framework by a primitive notion of unbounded explicit public announcement whose e↵ect is to expand the agents' belief bases with the information that ↵ is mutual belief, for any level k 0.

Conclusion and perspectives

We have provided a novel investigation of propositional awareness and of its relationship with explicit and implicit belief. In our approach, explicit belief is the only primitive concept, and awareness and implicit belief are grounded on it. Specifically, an agent's awareness set and set of doxastic alternatives are directly computed from the agent's belief base. The main results of the paper are an axiomatics for our logic of awareness, explicit and implicit belief, a polynomial embedding of the logic of propositional awareness into our logic, and a polynomial embedding of our logic into the logic of general awareness. By the latter embedding, we obtained a complexity result for our logic, namely, that its satisfiability checking problem is PSPACE-complete, the same complexity as standard multimodal logic K n . We also investigated some dynamic aspects of our logical setting, by extending it with the notions of public announcement and private belief expansion. We have provided complexity results for these extensions. Directions of future research are manifold. We would like to briefly discuss some of them before concluding.

Introspection Future work will be devoted to explore more properties of awareness typically discussed in the literature, such as awareness/unawareness introspection. A simple way to obtain introspection over epistemic attitudes consists in strengthening the epistemic accessibility relation between two states S = (B 1 , . . . , B n , A 1 , . . . , A n , V ) and S 0 = (B 0 1 , . . . , B 0 n , A 0 1 , . . . , A 0 n , V 0 ) as follows:

(S, S 0 ) 2 R i if and only if (i)8↵ 2 B i , S 0 |= ↵, and (ii)B i = B 0 i . Item (i) corresponds to the condition given in Definition 3.4, while item (ii) requires that a state S 0 is considered possible by an agent at a state S only if the agent has the same belief base in the two states. In other words, the two states are epistemically equivalent for agent i. This variant of the epistemic accessibility relation which is used for interpreting the implicit belief operator 2 i makes the following six formulas valid:

4 i ↵ ! 2 i 4 i ↵, (10)
¬4 i ↵ ! 2 i ¬4 i ↵, (11)
i ' ! 2 i i ', (12)
¬ i ' ! 2 i ¬ i ', (13)
2 i ' ! 2 i 2 i ', (14)
¬2 i ' ! 2 i ¬2 i '. (15)
They capture, respectively, positive and negative introspection over explicit belief, awareness and implicit belief. We plan to study the axiomatic properties of this variant of the logic LDAA with introspection over epistemic attitudes.

Awareness of agents

We also plan to extend our logical setting by the notion of awareness of agents and to compare it with the notion defined in [START_REF] Hans Van Ditmarsch | Awareness and forgetting of facts and agents[END_REF][START_REF] Hans Van Ditmarsch | Becoming aware of propositional variables[END_REF][START_REF] Hans Van Ditmarsch | Semantics for knowledge and change of awareness[END_REF]. Like propositional awareness, awareness of agents will be computed from belief bases. Formally, let i,j be a modal operator indicating that agent i is aware of agent j. We interpret it as follows with the help of our belief base semantics: (S, Cxt) |= i,j () there exists ↵ 2 L 0 such that j appears in ↵ and (S, Cxt) |= 4 i ↵. This means agent i is aware of agent j if agent i has a formula in his belief base mentioning agent j. We conjecture that the following principle together with the principles of the logic LDAA is su cient to completely axiomatize this extension by the notion of agent awareness:

4 i ↵ ! i,j if j appears in ↵.
Bisimulation Last but not least, we plan to define a notion of bisimulation for our belief base semantics and to compare it with the notion of awareness bisimulation for the logic of propositional awareness defined in [START_REF] Hans Van Ditmarsch | Implicit, explicit and speculative knowledge[END_REF].

Lemma 3 . 1

 31 Let ' 2 ⌃ and let w 2 W . Then, (M, w) |= ' if and only if

Figure 1 :

 1 Figure 1: Relations between semantics for the language L LDAA . An arrow means that satisfiability relative to the first class of structures implies satisfiability relative to the second class of structures. Full arrows correspond to the results stated in Lemmas 3.2, 3.3 and 3.4. Dotted arrows denote relations that follow straightforwardly given the inclusion between classes of structures.

Theorem 4 . 1

 41 Let X ✓ {D 2i , T 2i }. Then, the logic LDAA X is sound and complete for the class QNDAM {cf (x):x2X} .The following is a corollary of Theorem 3.1 and Theorem 4.1.

Corollary

Figure 2 :Figure 2

 22 Figure 2: EmbeddingsFigure 2 summarizes the connection between our logic LDAA and the awareness logics LPA and LGA we established in Theorems 5.1 and 6.1. It highlights

Figure 3 :

 3 Figure 3: Relationship between awareness, explicit and implicit belief

  Atm(['!] ) = Atm(') [ Atm( ) Moreover, we add the following clause to the definition of the satisfaction relation between MABAs and formulas. Definition 8.1 Let (S, Cxt) be a MABA. Then, (S, Cxt) |= ['!] () if (S, Cxt) |= ' then (S, Cxt '! ) |= ,

Theorem 8 . 2

 82 Checking satisfiability of formulas in L LDAA PBE relative to the class MABA is PSPACE-complete.

def= [+ ( 1 )

 1 EMB 0 ↵] . . . [+ (n) EMB 0 ↵] . . . [+ (1) EMB k ↵]

  According to the previous definition, a state is considered possible by an agent if it satisfies all his explicit beliefs.

Definition 3.4 For any i 2 Agt, R i is the binary relation on S such that for any S = (B 1 , . . . , B n , A 1 , . . . , A n , V ), S 0 = (B 0 1 , . . . , B 0 n , A 0 1 , . . . , A 0 n , V 0 ) 2 S, (S, S 0 ) 2 R i if and only if 8↵ 2 B i , S 0 |= ↵.

  Definition 3.6 The MABA (S, Cxt) satisfies global consistency (GC) if and only if, for every i 2 Agt and for every S 0 2 ({S} [ Cxt), there exists S 00 2 Cxt such that (S 0 , S 00 ) 2 R

i . Definition 3.7 The MABA (S, Cxt) satisfies belief correctness (BC) if and only if S 2 Cxt and, for every i 2 Agt and for every S 0 2 Cxt, (S 0 , S 0 ) 2 R i . It is worth noting that (S, Cxt) satisfies belief correctness if and only if S 2 Cxt and for all S 0

  by the axiom AGPP, By the definition of the canonical model, the latter is equivalent to the fact that, 8p 2 Atm( ), p 2 A LDAAX (i, w). The latter is equivalent toAtm( ) ✓ A LDAAX (i, w), which means (M LDAAX , w) |=The last step consists in proving that the LDAA X -canonical model belongs to the appropriate model class for the logic LDAA X . Let X ✓ {D 2i , T 2i }. Then, M LDAAX 2 QNDAM {cf (x):x2X} .Proof Firstly, we need to prove that M LDAAX satisfies Condition (C1 ⇤ ) and (C2 ⇤ ) in Definition 3.11. For Condition (C1 ⇤ ), we have to prove that if ↵ 2 D LDAAX (i, w) then Atm(↵) ✓ A LDAAX (i, w). Suppose ↵ 2 D LDAAX (i, w). Thus, 4

	⇤	i	by our semantics.
	Proposition 4.2

i 2 w i↵ 8p 2 Atm( ), i p 2 w. i ↵ 2 w. Hence, by the axiom Int 4i, i , i ↵ 2 w. By the axiom AGPP, it follows that, 8p 2 Atm(↵), i p 2 w. Then, by the definition of

  0 , w) |= A i . Let us consider the case ' = B i . Suppose (M, w) |= tr 1 (B i ). By the induction hypothesis, we have || || M 0 = ||tr 1 ( )|| M . By the function tr 1 , (M, w) |= tr 1 (B i ) means (M, w) |= 2 i tr 1 ( ). By the semantics of NDAM, the latter is equivalent to N (i, w) ✓ ||tr 1 ( )|| M . By the definition of )(i, w) and the fact || || M 0 = ||tr 1 ( )|| M , the latter is equivalent to

  w) and 8p 2 Atm(↵), p 2 A(i, w). By definition of M 0 , the latter implies tr 2 (↵) 2 ⇢(i, w) and w 2 ⇡ aw (i,p) for all p 2 Atm(↵).

	(M 0	The latter is equivalent to (i) (M 0	, w) |= A	i tr 2 (↵) and
				M 0 .
	Thus, by the definition of ), it follows that ) (i, w) ✓ ||tr 2 (↵)|| means that (ii) (M 0 i tr 2 (↵). The previous items (i) and (ii) together M 0 . The latter , w) |= B imply that (M 0 , w) |= X

, w) |= aw (i,p) for all p 2 Atm(↵). Moreover, (M, w) |= 4 i ↵ implies N (i, w) ✓ ||↵|| M . By induction hypothesis, we have ||↵|| M = ||tr 2 (↵)|| i tr 2 (↵) ^Vp2Atm(↵) aw (i,p). (() Suppose (M 0 , w) |= X i tr 2 (↵) ^Vp2Atm(↵) aw (i,p). The latter implies that (M 0 , w) |= A i tr 2 (↵). Hence, by definition of M 0 , ↵ 2 D(i, w) which is equivalent to (M, w) |= 4 i ↵. Finally, let us prove the case ' = 2 i . By induction hypothesis, we have || || M = ||tr 2 ( )|| M 0 . (M, w) |= 2 i means that N (i, w) ✓ || || M . By definition of ) and || || M = ||tr 2 ( )|| M 0 , the latter is equivalent to ) (i, w) ✓ ||tr 2 ( )|| M 0 which in turn is equivalent to (M 0 , w) |= B i tr 2 ( ). Thus, (M 0

  , tr 2 (↵) 2 ⇢(i, s) and 8p 2 Atm, s 2 ⇡ aw (i,p) . By definition of D, the latter is equivalent to ↵ 2 D(i, s) which in turn is equivalent to (M 0

	Let us finally prove the case ' = 2	i ↵. i . By induction hypothesis, we have , s) |= 4
	||tr 2 ( )|| which in turn means that )(i, s) ✓ ||tr 2 ( )|| M = || || M 0 . (M, s) |= tr 2 (2 i ) means that (M, s) |= B M . By definition of N (i, s) and i tr 2 ( ) || || M = ||tr 2 ( )|| M 0 , the latter is equivalent to N (i, s) ✓ || || M 0 which in turn is equivalent to (M 0 i . , s) |= 2 Thus, (M 0
			tr 2 (')
	if and only if (M 0	, s) |= '. The atomic case, boolean cases and case ' =

i are straightforward and we do not need to prove them.

Let us prove the case

' = 4 i ↵. (M, s) |= tr 2 (4 i ↵) is equivalent to (M, s) |= X i tr 2 (↵) ^Vp2Atm(↵) aw (i,p

). The latter is equivalent to )(i, s) ✓ ||tr 2 (↵)|| M

Table 1 :

 1 Concepts of awareness, explicit belief and implicit belief in LPA, LGA and LDAA

		Primitive	yes	yes	no
			relevance-	accessibility-	relevance-
		Types	based	based (primarily),	based
				relevance-based (via
				special atoms aw (i,p))
		Primitive	no	no	yes
		Types	relevance-	accessibility-	accessibility-
	Explicit belief		based	based	based
		Deductively	locally	no	no
		closed
		Primitive	yes	yes	no
	Implicit belief	Deductively	globally	globally	globally
		closed

  Proposition 8.2 Let ' 2 L LDAA PA and X ✓ {BC}. Then, ' $ red LDAA PA (') is valid with respect to the class MABA X .Proof The proposition is proved inductively on the structure of '. The atomic case, the boolean cases and the cases for the operators 4The fact that checking satisfiability for formulas in L LDAA PA is decidable follows from the decidability of satisfiability checking for formulas in L LDAADefinition 8.4 The mapping red LDAA PBE is inductively defined as follows:

	1.red LDAA PBE (p)		= p
	2.red LDAA PBE (4 3.red LDAA PBE (¬') j ↵) 4.red LDAA PBE (' ^ ) 5.red LDAA PBE (2 j ') 6.red LDAA PBE ( j ')	j red LDAA PBE (↵) = ¬red LDAA PBE (') = 4 = red LDAA PBE (') ^red LDAA PBE ( ) = 2 j red LDAA PBE (') p2Atm(') = j p
	7.red LDAA PBE ([+	i ↵]p)	= red LDAA PBE (p)
	8.red LDAA PBE ([+	i
			i , 2	i and	i
	are evident. The case for the public announcement operator ['!] is provable via
	the valid equivalences in Proposition 8.1.	⇤

Because

i ' bears the meaning that ' can be inferred from i's explicit beliefs,

i ' should be read "¬' cannot be inferred from agent i's explicit beliefs", which is equivalent to "' is consistent with agent i's explicit beliefs".

Note that if we defined the translation sending explicit beliefs of LPA into explicit beliefs of LDAA, satisfiability would be preserved only in the direction from LDAA to LPA. For the other direction, a formula of the form X i B i ' in L LPA cannot be translated into L LDAA with this alternative translation.

See[START_REF] Sillari | Models of awareness[END_REF], for more details on the di↵erent interpretations of the notion of awareness.

Explicit belief in the sense of LGA and LDAA can be conceived as a belief which is active in the agent's mind and is under the focus of his attention. The latter interpretation is in line with some existing cognitive theories of epistemic states[START_REF] Kahneman | Variants of uncertainty[END_REF][START_REF] Lorini | The cognitive structure of surprise: looking for basic principles[END_REF].

See[START_REF] Balbiani | The dynamics of epistemic attitudes in resource-bounded agents[END_REF][START_REF] Fernando | Explicit and implicit knowledge in neighbourhood models[END_REF] for an epistemic logic in which inference steps conceived as mental actions are explicitly modeled.

van Benthem & Velásquez-Quesada[START_REF] Van Benthem | The dynamics of awareness[END_REF] defines the "consider" operation which consists in extending an agent's awareness set with a new formula. This operation does not necessarily modify the agent's explicit beliefs, since in LGA explicit belief is defined from awareness and implicit belief. Therefore, explicit belief change may require that awareness change and implicit belief change are synchronously executed.

Note that the order of execution would have been relevant, if we assumed that private belief expansion operations have executability preconditions. For example, suppose agent 1 can learn that p (i.e., + 1 p is executable) if and only if agent 2 already believes that p (i.e., 4 2 p is true), while agent 2 can learn that p (i.e., + 2 p is executable) if and only if p is actually true. Therefore, if p is indeed true and none of them explicitly believes that p, it is possible for 1 to learn that p after 2 has learnt that p. On the contrary, it is not possible for 1 to learn that p before 2 learns that p.

Acknowledgements

Emiliano Lorini is supported by the ANR project CoPains ("Cognitive Planning in Persuasive Multimodal Communication") and by the ANR-3IA Artificial and Natural Intelligence Toulouse Institute (ANITI). Pengfei Song is supported by the key project of National Social Science Foundation of China (No. 16AZX017).

The rest of this section is devoted to prove completeness for the logics in the LDAA family.

We first prove completeness of each logic LDAA X . To this aim, let us define the following correspondence function between axioms and semantic properties:

As usual, we have the following property for maximally consistent sets (MCSs). Proposition 4.1 Let be a LDAA X -MCS with X ✓ {D 2i , T 2i }. Then,

• if ', ' ! 2 then 2 ,

The following is the Lindenbaum's lemma for our logics. Its proof is standard (cf. Lemma 4.17 in [START_REF] Blackburn | Modal Logic[END_REF]) and we omit it. Lemma 4.1 Let be a set of formulas being LDAA X -consistent with X ✓ {D 2i , T 2i }, then there exists a LDAA X -MCS 0 such that ✓ 0 .

To prove completeness with respect to the class QNDAM X , we construct a canonical model as follows.

The following existence lemma is necessary for the proof of completeness. The proof is again standard (cf. Lemma 4.20 in [START_REF] Blackburn | Modal Logic[END_REF]) and we omit it.

The following is the truth lemma for our logics.

(Theorem 6.2) and the fact that red LDAA PA provides an e↵ective procedure for reducing a formula ' in L LDAA PA into an equivalent formula red LDAA PA (') in L LDAA .

Theorem 8.1 Let X ✓ {BC}. Then, checking satisfiability of formulas in L LDAA PA relative to the class MABA X is decidable.

Private Belief Expansion

This section presents a second dynamic extension of the LDAA logics by private belief base expansion. Concretely, we extend the language L LDAA (Atm, Agt) by operators of the form [+ i ↵], thereby obtaining the language L LDAA PBE (Atm, Agt) defined by the following grammar:

, where i ranges over Agt, ↵ ranges over L 0 , and LDAA PBE stands for "Logic of Doxastic Attitudes with Awareness and Private Belief Expansion".

As in Section 2, we write L LDAA PBE instead of L LDAA PBE (Atm, Agt). The formula [+ i ↵] ' has to be read "' holds after agent i has expanded his belief base with ↵".

Like in the extension by public announcement, we need to generalize the function computing the atoms occurring in a formula: V +i↵ = V, and for all j 2 Agt:

).

The informative event + i ↵ just consists in agent i privately learning that ↵ by adding ↵ to his belief base, while the other agents' belief bases are not changed. Note that agent i's awareness set is indirectly a↵ected by the informative event, since agent i's awareness is computed from his new belief base.

Unlike public announcement, private belief base expansion does not necessarily preserve belief correctness (BC) or global consistency (GC) of the original belief base. Therefore, in the rest of this section we focus on the most general model class MABA.

As for public announcement, we have reduction principles for the dynamic operators [+ i ↵]. They are listed in the following proposition. (We omit the proof since it is entirely standard.) Proposition 8. [START_REF] Balbiani | The dynamics of epistemic attitudes in resource-bounded agents[END_REF] The following formulas are valid relative to the class MABA:

It is worth to pay attention to the last two reduction principles for awareness: by expanding his belief base with the input formula ↵, agent i simply adds to his awareness set the atomic propositions occurring in ↵. As indicated by the fourth reduction principle, agent i will be able to deduce that ' after expanding his belief base with ↵ if, before the belief expansion, agent i is able to deduce that ↵ implies '. The sixth and seventh reduction principles just state that, by privately expanding his belief base with ↵, agent i adds ↵ to his belief base, while all other agents keep their belief bases unchanged.

Analogously to the extension with public announcement, the valid equivalences in the previous proposition allow us to transform every formula of the language L LDAA PBE into an equivalent formula of L LDAA with no occurrence of dynamic operators. The transformation is obtained via the following mapping red LDAA PBE .