Abstract
The paper develops an interface between syntax-based logical models of awareness and dynamic epistemic logic. The framework is shown to be able to accommodate a variety of notions of awareness and knowledge, as well as their dynamics. This, it is argued, offers a natural formal environment for the analysis of epistemic phenomena typical of multi-agent information exchange, such as how agents become aware of relevant details, how they perform inferences and how they share their information within a group. Technically, the logics presented are all simple refinements of the logic of public announcements.
Similar content being viewed by others
Notes
Note how there is no mention of the other syntactic component a formula might involve: agents. This work assumes that every agent is ‘available’ to each other in the sense that every agent can talk about any other agent. This assumption may be lifted (see for instance van Ditmarsch and French 2009) but such generalisation will not be pursued here.
It is worthwhile to highlight that the principle of replacement of equivalents does not hold for the \(\,^{av(i)}\) and \(\,^{ack(i)}\) operators. First, the validity of both \(\,^{av(i)}\varphi _1\) and \(\varphi _{1} \leftrightarrow \varphi _{2}\) does not entail the validity of \(\,^{av(i)}\varphi _2\), as \(\varphi _{1}\) and \(\varphi _{2}\) might involve different atomic propositions and the \(\mathsf {PA}\)-sets do not have any closure property. Second, and similarly, the validity of both \(\,^{ack(i)}\varphi _1\) and \(\varphi _{1} \leftrightarrow \varphi _{2}\) does not entail the validity of \(\,^{ack(i)}\varphi _2\), as \(\mathsf {AC}\)-sets do not have any closure property. In fact, for axiomatisation’s purposes, formulas of the form \(\,^{av(i)}\varphi \) and \(\,^{ack(i)}\varphi \) can be understood as special atomic propositions, with the former behaving as described by the axioms in the lower half of Table 1, and with the latter having no special behaviour at all.
All the notions are formalised in terms of the basic concepts defined and axiomatised earlier in this section. A direct axiomatisation of these derived concepts is left for future work (but cf. with axiomatisations of similar notions as in, e.g., van Ditmarsch et al. 2013).
However, they do need to know implicitly every validity: for example, she might be unaware of \(p\), a situation in which she does not know \(p \vee \lnot p\) implicitly.
This includes validities, as the agent might not have acknowledged them as true.
A more detailed comparison between the works is provided in Sect. 3.3.
But note that the two definitions coincide, i.e., \(\Box _i{(\varphi \wedge \,^{ack(i)}\varphi )} \leftrightarrow (\Box _i{\varphi } \wedge \,^{ack(i)}\varphi )\) is valid, when the accessibility relations are reflexive and preserve \(\mathsf {AC}_i\)-sets.
In fact, van Ditmarsch and French (2009) presents an even stronger notion of two states being equivalent when they satisfy the same modal formulae.
There are other ways of taking seriously the idea of an agent making the announcement. For example, one can consider the notion of trust among agents (Holliday 2010).
Still, as noticed before, this does not imply that the agent keeps track of these justifications.
References
Areces, C., & ten Cate, B. (2006). Hybrid logics. In P. Blackburn, J. van Benthem, & F. Wolter (Eds.), Handbook of modal logic, studies in logic and practical reasoning (Vol. 3). Amsterdam: Elsevier Science Inc.
Artëmov, S. N., & Nogina, E. (2005). Introducing justification into epistemic logic. Journal of Logic and Computation, 15(6), 1059–1073. doi:10.1093/logcom/exi053.
Baltag, A., Moss, L.S., & Solecki. S. (1999). The logic of public announcements, common knowledge and private suspicions. In Technical Report SEN-R9922, CWI, Amsterdam.
Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic. New York: Cambridge University Press.
Chellas, B. F. (1980). Modal logic: An introduction. Cambridge: Cambridge University Press.
Duc, H. N. (1997). Reasoning about rational, but not logically omniscient, agents. Journal of Logic and Computation, 7(5), 633–648.
Dung, P. M. (1995). On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77(2), 321–358.
Fagin, R., & Halpern, J. Y. (1988). Belief, awareness, and limited reasoning. Artificial Intelligence, 34(1), 39–76. doi:10.1016/0004-3702(87)90003-8.
Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995). Reasoning about knowledge. Cambridge: The MIT Press.
Gerbrandy, J., & Groeneveld, W. (1997). Reasoning about information change. Journal of Logic, Language, and Information, 6(2), 147–196.
Grossi, D., Lorini, E., & Schwarzentruber, F. (2013). Ceteris paribus structure in logics of game forms. In Proceedings of TARK’13.
Grossi, D., & Pigozzi, G. (2014). Judgment aggregation: A primer., Synthesis lectures on artificial intelligence and machine learning San Rafael: Morgan and Claypool.
Halpern, J. (2001). Alternative semantics for unawareness. Games and Economic Behavior, 37, 321–339.
Halpern, J., & Rêgo, L. (2008). Interactive unawareness revisited. Games and Economic Behavior, 62(1), 232–262.
Hamami, Y. (2010). The interrogative model of inquiry meets dynamic epistemic logics. Master’s thesis. ILLC, Universiteit van Amsterdam, Amsterdam, The Netherlands, ILLC Master of Logic Thesis Series MoL-2010-04.
Heifetz, A., Meier, M., & Schipper, B. (2006). Interactive unawareness. Journal of Economic Theory, 130(1), 78–94.
Hill, B. (2010). Awareness dynamics. Journal of Philosophical Logic, 39(2), 113–137.
Hintikka, J. (1962). Knowledge and belief. Ithaca: Cornell University Press.
Holliday, W.H. (2010). Trust and the dynamics of testimony. In L. Kurzen, D. Grossi, F.R. Velázquez-Quesada (eds) Logic and Interactive RAtionality. Seminar’s yearbook 2009, ILLC (pp. 118–142). Universiteit van Amsterdam, Amsterdam, The Netherlands.
Holliday, W. H., & Icard, T. F. (2010). Moorean phenomena in epistemic logic. In L. Beklemishev, V. Goranko, & V. Shehtman (Eds.), Advances in modal logic (pp. 178–199). London: College Publications.
Jago, M. (2009). Epistemic logic for rule-based agents. Journal of Logic, Language and Information, 18(1), 131–158. doi:10.1007/s10849-008-9071-8.
List, C., Puppe, C. (2009). Judgment aggregation: A survey. In Oxford handbook of rational and social choice. Oxford: Oxford University Press.
Meyer, J. J. C., & van Der Hoek, W. (1995). Epistemic logic for AI and computer science. New York: Cambridge University Press.
Modica, S., & Rustichini, A. (1994). Awareness and partitional information structures. Theory and Decisions, 37, 107–124.
Modica, S., & Rustichini, A. (1999). Unawareness and partitional information structures. Games and Economic Behavior, 27, 265–298.
Plaza, J. A. (1989). Logics of public communications. In M. L. Emrich, M. S. Pfeifer, M. Hadzikadic, & Z. W. Ras (Eds.), Proceedings of the 4th international symposium on methodologies for intelligent systems (pp. 201–216), Tennessee: Oak Ridge National Laboratory, ORNL/DSRD-24.
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic proof theory, 2nd edn. No. 43 in Cambridge tracts in theoretical computer science. Cambridge, U.K.: Cambridge University Press.
van Benthem, J. (2008). Merging observation and access in dynamic logic. Journal of Logic Studies, 1(1), 1–17.
van Benthem, J., & Velázquez-Quesada, F. R. (2010). The dynamics of awareness. Synthese (Knowledge, Rationality and Action), 177(Supplement 1), 5–27. doi:10.1007/s11229-010-9764-9.
van Benthem, J. (2011). Logical dynamics of information and interaction. Cambridge: Cambridge University Press.
van Benthem, J., & Minică, S. (2012). Toward a dynamic logic of questions. Journal of Philosophical Logic, 41(4), 633–669. doi:10.1007/s10992-012-9233-7.
van Ditmarsch, H., & French, T. (2009). Awareness and forgetting of facts and agents. In Proceedings of the 2009 IEEE/WIC/ACM International joint conference on web intelligence and intelligent agent technologies (WI-IAT 2009), Milan.
van Ditmarsch, H.P., French, T., Velázquez-Quesada, F.R., & Wang, Y. (2013). Knowledge, awareness, and bisimulation. In Schipper BC (Ed.). TARK (pp 61–70).
van Ditmarsch, H., van der Hoek, W., & Kooi, B. (2007). Dynamic epistemic logic (Vol. 337)., Synthese library Dordrecht: Springer.
van Ditmarsch, H., & French, T. (2011). Becoming aware of propositional variables. In M. Banerjee & A. Seth (Eds.), ICLA (pp. 204–218)., Lecture notes in computer science New Delhi: Springer. doi:10.1007/978-3-642-18026-2-17.
Velázquez-Quesada, F.R. (2013). Public announcements for non-omniscient agents. In Lodaya K (Ed.). Lecture notes in computer science (Vol. 7750, pp. 220–232). doi:10.1007/978-3-642-36039-8_20
Velázquez-Quesada, F. R. (2009). Inference and update. Synthese (Knowledge, Rationality and Action), 169(2), 283–300. doi:10.1007/s11229-009-9556-2.
Velázquez-Quesada, F. R. (2014). Dynamic epistemic logic for implicit and explicit beliefs. Journal of Logic, Language and Information, 23(2), 107–140. doi:10.1007/s10849-014-9193-0.
Wang, Y., & Cao, Q. (2013). On axiomatizations of public announcement logic. Synthese, 190(Supplement 1), 103–134. doi:10.1007/s11229-012-0233-5.
Acknowledgments
The authors would like to express their gratitude to two anonymous reviewers for their comments and observations, which have helped to improve this paper.
Author information
Authors and Affiliations
Corresponding author
Appendix
Appendix
Proof of Theorem 1 (sketch)
Soundness is proved by showing that axioms are valid and rules preserve validity. Completeness is proved by showing that every L-consistent set of \(\mathcal {L}\)-formulas is satisfiable in a pointed \(\mathbf{M}_K\)-model. For the latter, construct the standard modal canonical model \(M^c\) and, for each maximal L-consistent set of formulas \(w\), define the propositional availability and acknowledgement set functions in the following way:
With these definitions, it is easy to show that the new type of formulas also satisfy the Truth Lemma, that is,
For the first case, availability of formulas, an induction aided by the axioms describing their behaviour does the work. The second case, that for acknowledgement formulas, is straightforward.
Thus, any L-consistent set of formulas \(\Sigma \) can be extended into a maximal L-consistent set \(\Sigma ^*\) that is satisfiable in \((M^c, \Sigma ^*)\). Moreover, by standard results on canonicity and modal correspondence (Chapter 4 of Blackburn et al. 2001), axioms T, 4 and 5 make the accessibility relations of the canonical model equivalence relations. Then completeness follows. \(\square \)
Proof of Proposition 2
For the validity of the formula, suppose \((M, w) \models {{\text {Imp}}_i}(\varphi \rightarrow \psi ) \wedge {{\text {Imp}}_i}(\varphi )\). Then \((M, w) \models \Box _i{(\varphi \rightarrow \psi )} \wedge \Box _i{\varphi }\) and hence \((M, w) \models \Box _i{\psi }\). But \((M, w) \models \Box _i{\,^{av(i)}(\varphi \rightarrow \psi )}\) holds too, so \((M, w) \models \Box _i{\,^{av(i)}\psi }\). Therefore, \((M, w) \models {{\text {Imp}}_i}(\psi )\).
For the validity of the rule, take any pointed semantic model \((M, w)\). Since \(\varphi \) is a validity, \((M, w) \models \Box _i{\varphi }\). From \((M, w) \models {{\text {Ao}}_i}{(\varphi )}\) it follows that \((M, w) \models \Box _i{\,^{av(i)}\varphi }\). Hence \((M, w) \models \Box _i{\varphi } \wedge \Box _i{\,^{av(i)}\varphi }\), that is, \((M, w) \models {{\text {Imp}}_i}(\varphi )\). \(\square \)
Proof of Proposition 3
Suppose \({{\text {Ao}}_i}{(\varphi )}\) holds at some world in a given model. From Proposition 1 it follows that the agent is aware of all atoms in \(\varphi \); from the same proposition it follows that she is also aware of every formula built from such atoms. In particular, she is aware of \({{\text {Ao}}_i}{(\varphi )}\).
\(\square \)
Proof of Proposition 4
Suppose \(\lnot {{\text {Ao}}_i}{(\varphi )}\) holds at some world in a given model. From Proposition 1 it follows that the agent is not aware of at least one atom of \(\varphi \); then from the same proposition it follows that she cannot be aware of any formula involving such atom. In particular, she cannot be aware of \(\lnot {{\text {Ao}}_i}{(\varphi )}\).
\(\square \)
Proof of Proposition 7
By unfolding the definitions, the formula becomes
The first conjunct of the antecedent, the extra requirement and the K axiom yield the first conjunct of the consequent. Transitivity plus the first and second conjunct of the antecedent yield the second and third conjunct of the consequent, respectively. \(\square \)
Proof of Proposition 8
Suppose \(\lnot {{\text {Inh}}_i}(\varphi ) \wedge {{\text {At}}_i}{(\varphi )}\); then \(\lnot \Box _i{\varphi }\). This and euclideanity yields \(\Box _i{\lnot \Box _i{\varphi }}\), which implies \(\Box _i{\lnot (\Box _i{\,^{ack(i)}\varphi } \wedge \Box _i{\varphi })}\) or, shortening, \(\Box _i{\lnot {{\text {Inh}}_i}(\varphi )}\). Moreover, \(\lnot \Box _i{\varphi }\) and the extra requirement imply \(\Box _i{\,^{ack(i)}\lnot {{\text {Inh}}_i}(\varphi ))}\). These two pieces yield \({{\text {Inh}}_i}(\lnot {{\text {Inh}}_i}(\varphi ))\).
\(\square \)
Proof of Proposition 9
By unfolding the definitions, the formula becomes
By Proposition 1, the first conjunct of the antecedent implies the first one of the consequent; by transitivity, the first and second conjunct of the antecedent imply the second and third ones of the consequent. \(\square \)
Proof of Proposition 10
Suppose \(\lnot {{\text {Imp}}_i}(\varphi ) \wedge {{\text {Ao}}_i}{(\varphi )}\); then \(\Box _i{\,^{av(i)}\varphi }\) and \(\lnot \Box _i{\varphi }\). From the first and Proposition 1 it follows that \(\Box _i{\,^{av(i)}(\lnot {{\text {Imp}}_i}(\varphi ))}\). From the second and euclideanity it follows that \(\Box _i{\lnot \Box _i{\varphi }}\), which implies \(\Box _i{\lnot (\Box _i{\,^{av(i)}\varphi } \wedge \Box _i{\varphi })}\) or, shortening, \(\Box _i{\lnot {{\text {Imp}}}(\varphi )}\). These two pieces yield \({{\text {Imp}}_i}(\lnot {{\text {Imp}}_i}(\varphi ))\). \(\square \)
Proof of Proposition 11
By unfolding the definitions, the formula becomes
By Proposition 1, the first conjunct of the antecedent implies the first of the consequent. By transitivity, the first, second and third conjunct of the antecedent imply the second, third and fourth of the consequent, respectively. Finally, the extra condition, the K axiom and the third conjunct of the antecedent imply the fifth conjunct of the consequent. \(\square \)
Proof of Proposition 12
The antecedent of the implication implies \(\Box _i{\,^{av(i)}\varphi }\), \(\Box _i{\varphi }\) and \(\lnot \Box _i{\,^{ack(i)}\varphi }\). From the first it follows that \(\Box _i{\,^{av(i)}(\lnot {{\text {Exp}}_i}(\varphi ))}\) as before. From the first, second and third together with transitivity and euclideanity it follows that \(\Box _i{\Box _i{\,^{av(i)}\varphi }}\), \(\Box _i{\Box _i{\varphi }}\) and \(\Box _i{\lnot \Box _i{\,^{ack(i)}\varphi }}\), that is, \(\Box _i{\lnot (\Box _i{\,^{av(i)}\varphi } \wedge \Box _i{\varphi } \wedge \Box _i{\,^{ack(i)}\varphi })}\) or, shortening, \(\Box _i{\lnot {{\text {Exp}}_i}(\varphi )}\). The third and the further assumption implies \(\Box _i{\,^{ack(i)}\lnot {{\text {Exp}}_i}(\varphi )}\). These three pieces yield \({{\text {Exp}}_i}(\lnot {{\text {Exp}}_i}(\varphi ))\).
\(\square \)
Proof of Proposition 13
Similar to those of Propositions 9 and 10. \(\square \)
Proof of Proposition 15
Define \(\sim _{\mathsf {PA}_i(w)}\) as in Definition 6; the desired implication is proved by a simple induction on the complexity of \(\gamma \). The implication in the other direction does not hold because the fact that \(\gamma \)’s truth-value is uniform through \(\sim _{\mathsf {PA}_i(w)}\) does not imply that every atom in \(\gamma \) is in \(\mathsf {PA}_i(w)\). For a simple counter-example, take a model in which the truth-value of a given \(p\) is the same in all worlds, and pick an evaluation point \(w\) in which \(p \not \in \mathsf {PA}_i(w)\); the formula \(\left[ \sim _{\mathsf {PA}_i(w)}\right] p \vee \left[ \sim _{\mathsf {PA}_i(w)}\right] \lnot p\) holds at \(w\), but \(\,^{av(i)}p\) does not. \(\square \)
Proof of Proposition 17
Pick any pointed semantic model \((M, w)\). The first property is straightforward: the operation puts \(q\) in the \(\mathsf {PA}_j\)-set of every world in the model, so \(\,^{av(j)}q\) and hence \(\Box _j{\,^{av(j)}q}\) (i.e., \({{\text {Ao}}_j}{(q)}\)) becomes true everywhere.
For the second one, the three ingredients for explicit knowledge are verified. After the inference operation the agent is aware of \(\chi \) because the precondition of the operation says she was already aware of \(\eta \rightarrow \chi \) and the operation does not remove atoms from the propositional availability sets; thus, \(\Box _j{\,^{av(j)}\chi }\). Moreover, after the operation, \(\chi \) is in the \(\mathsf {AC}_j\)-set of every world that already had \(\eta \rightarrow \chi \) and \(\eta \), so in particular it is in every world \(R_j\)-accessible from \(w\) since the precondition of the operation requires that the implication and its antecedent were already there; thus, \(\Box _j{\,^{ack(j)}\chi }\). Finally, because of the precondition, \(\chi \) holds in every world \(R_j\)-accessible from \(w\) in the original model \(M\) (explicit knowledge is also implicit knowledge, which is closed under logical consequence). But the operation affects only the truth-value of formulas containing \(\,^{ack(j)}\chi \); hence, \(\chi \) itself cannot be affected and therefore it will still be true at every world \(R_j\)-accessible from \(w\) in the resulting model \(M_{{\overset{\eta \rightarrow \chi }{\hookrightarrow }_{j}}}\); thus, \(\Box _j{\chi }\). Therefore, \({{\text {Exp}}_j}(\chi )\) holds at \(w\) in \(M_{{\overset{\eta \rightarrow \chi }{\hookrightarrow }_{j}}}\).
The third property is also straightforward, and again the three ingredients are verified. The operation guarantees that, after it, \(\Box _i{(\,^{av(i)}\chi \wedge \,^{ack(i)}\chi )}\) will be true at \(w\). Moreover, the new model contains only worlds that satisfied \({{\text {Exp}}_j}(\chi )\) in the original model \(M\) and, by truthfulness, they all also satisfy \(\chi \) in \(M\). Now, propositional formulas depend just on the atomic valuation, which is not affected by the announcement operation; then the surviving worlds will still satisfy \(\chi \) in the resulting model \(M_{^{j}:\chi !}\). Hence, \(\Box _i{\chi }\) is true at \(w\) and therefore \({{\text {Exp}}_i}(\chi )\) is true at \(w\) in \(M_{^{j}:\chi !}\).
\(\square \)
Rights and permissions
About this article
Cite this article
Grossi, D., Velázquez-Quesada, F.R. Syntactic awareness in logical dynamics. Synthese 192, 4071–4105 (2015). https://doi.org/10.1007/s11229-015-0733-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11229-015-0733-1