Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Inhabitants of Intuitionistic Implicational Theorems Read chapter Read first chapter

2018 | OriginalPaper | Chapter

APAL with Memory Is Better

Authors : Alexandru Baltag, Aybüke Özgün, Ana Lucia Vargas Sandoval

Published in: Logic, Language, Information, and Computation

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We introduce Arbitrary Public Announcement Logic with Memory (APALM), obtained by adding to the models a ‘memory’ of the initial states, representing the information before any communication took place (“the prior”), and adding to the syntax operators that can access this memory. We show that APALM is recursively axiomatizable (in contrast to the original Arbitrary Public Announcement Logic, for which the corresponding question is still open). We present a complete recursive axiomatization, that uses a natural finitary rule, we study this logic’s expressivity and the appropriate notion of bisimulation.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Deciding Open Definability via Subisomorphisms
next chapter Lindenbaum and Pair Extension Lemma in Infinitary Logics
Footnotes
1
BAPAL is a very weak version, allowing \(\square \varphi \) to quantify over only purely propositional announcements - no epistemic formulas.
 
2
APAL\(^+\) is known to be decidable, hence its validities must be r.e., but no recursive axiomatization is known. Also, note that APAL\(^+\) is still very weak, in that it quantifies only over positive epistemic announcements, thus not allowing public announcements of ignorance, which are precisely the ones driving the solution process in puzzles such as the Muddy Children.
 
3
This means that from any proof of a theorem from the axioms that uses the infinitary rule we can obtain a finitary proof of the same theorem, by using the finitary rule instead.
 
4
Here, by ‘strong’ version we mean one that allows quantification over a sufficiently wide range of announcements (sufficiently wide to avoid Liar-like circles) as intended by a similar restriction in the original APAL or in its group-restricted version GAL.
 
5
From an epistemic point of view, it would be more natural to replace U by an operator Ck that describes current common knowledge and quantifies only over currently possible states that are accessible by epistemic chains from the actual state. We chose to stick with U for simplicity and leave the addition of Ck to APAL for future work.
 
6
This restriction is necessary to produce a well-defined semantics that avoids Liar-like vicious circles. In standard APAL, the restriction is w.r.t. inductive construct \(\Diamond \varphi \). Thus, formulas of the form \(\langle \Diamond p\rangle \varphi \) are allowed in original APAL. APAL and APALM expressivities seem to be incomparable, and that would still be the case if we dropped the above restriction.
 
7
We use a slightly different version of this rule, which is easily seen to be equivalent to the original version in the presence of the usual PAL reduction axioms.
 
8
Cheryl’s Birthday problem was part of the 2015 Singapore and Asian Schools Math Olympiad, and became viral after it was posted on Facebook by Singapore TV presenter Kenneth Kong.
 
9
As a consequence, having such a rich memory of history would destroy some of the appealing features of the APAL operator (e.g. its S4 character: \(\square \varphi \rightarrow \square \square \varphi \)), and would force us to distinguish between “knowability via one communication step” \(\Diamond K\) versus “knowability via a finite communication sequence” \(\Diamond ^* K\), leading to an unnecessarily complex logic.
 
10
In such models, only the ‘prior’ and the ‘posterior’ information states are taken to be relevant, while all the intermediary steps are forgotten. As a consequence, all the evidence gathered in between the initial and the current state can be compressed into one set E, called “the evidence” (rather than keeping a growing tail-sequence of all past evidence sets). Similarly, in our logic, all the past communication is compressed in its end-result, namely in the set W of current possibilities, which plays the same role as the evidence set E in Bayesian models.
 
11
Moreover, this limited form of memory is enough to ‘simulate’ the yesterday operator \(Y\varphi \) by using context-dependent formulas. For instance, the dialogue in Cheryl’s birthday puzzle (Albert: “I don’t know when Cheryl’s birthday is, but I know that Bernard doesn’t know it either”; Bernard: “At first I didn’t know when Cheryl’s birthday is, but I know now”; Albert: “Now I also know”), can be simulated by the following sequence of announcements: first, the formula \(0\wedge \lnot K_a c\wedge K_a\lnot K_b c\) is announced (where 0 marks the fact that this is the first announcement), then \((\lnot K_b c)^0 \wedge K_b c\) is announced, and finally \(K_a c\) is announced. (Here, we encode e.g. ‘Albert knows Cheryl’s birthday’ as \(K_a c=\bigvee \{K_a(d\wedge m): d\in D, m\in M\}\), where D is the set of possible days and M is the set of possible months.).
 
12
In SSL, the set of admissible sets is sometimes, but not always, taken to be a topology. Here, it will be a Boolean algebra with epistemic operators.
 
13
The update operator \(\langle \theta \rangle \varphi \) is often denoted by \(\langle !\theta \rangle \varphi \) in Public Announcement Logic literature; we skip the exclamation sign, but we will use the notation \(\langle !\rangle \) for this modality and [!] for its dual when we do not want to specify the announcement formula \(\theta \) (so that ! functions as a placeholder for the content of the announcement).
 
14
The standard notion requires only that formulas are more complex than their subformulas, while we also need that \(\Diamond \varphi \) is more complex than \(\langle \theta \rangle \varphi \). To the best of our knowledge, such a complexity measure was first introduced in [3] for the original APAL language from [2]. Similar measures have later been introduced for topological versions of APAL in [22, 23].
 
15
The “freshness” of the variable \(p\in P\) in the rule \([!]\square \)-intro ensures that it represents any ‘generic’ announcement.
 
16
A more direct soundness proof on APALM models is in principle possible, but would require at least as much work as our detour. Unlike in standard EL, PAL or DEL, the meaning of an APALM formula depends, not only on the valuation of the atoms occurring in it, but also on the family \(\mathcal {A}\) of all sets definable by \(\mathcal {L}_{-\Diamond }\)-formulas. The move from models to pseudo-models makes explicit this dependence on the family \(\mathcal {A}\), while also relaxing the demands on \(\mathcal {A}\) (which is no longer required to be exactly the family of \(\mathcal {L}_{-\Diamond }\)-definable sets), and thus makes the soundness proof both simpler and more transparent. Since we will need pseudo-models for our completeness proof anyway, we see no added value in trying to give a more direct proof.
 
17
A total bisimulation between epistemic models \((W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )\) and \((W', \sim '_1, \ldots , \sim '_n, \Vert \cdot \Vert ')\) is an epistemic bisimulation relation (satisfying the usual valuation and back-and-forth conditions from Modal Logic) \(B\subseteq W \times W'\), such that: for every \(s\in W\) there exists some \(s'\in W'\) with \(s B s'\); and dually, for every \(s'\in W'\) there exists some \(s\in W\) with \(s B s'\).
 
Literature
1.
Ågotnes, T., Balbiani, P., van Ditmarsch, H., Seban, P.: Group announcement logic. J. Appl. Log. 8, 62–81 (2010)MathSciNetCrossRef
2.
Balbiani, P., Baltag, A., van Ditmarsch, H., Herzig, A., Hoshi, T., de Lima, T.: ‘Knowable’ as ‘known after an announcement’. Rev. Symb. Log. 1, 305–334 (2008)MathSciNetCrossRef
3.
Balbiani, P., van Ditmarsch, H.: A simple proof of the completeness of APAL. Stud. Log. 8(1), 65–78 (2015)
4.
5.
6.
7.
8.
Bjorndahl, A., Özgün, A.: Topological subset space models for belief. In: Proceedings of the 16th TARK. EPTCS, vol. 251, pp. 88–101. Open Publishing Association (2017)
9.
Bolander, T., Andersen, M.B.: Epistemic planning for single-and multi-agent systems. J. Appl. Non-Class. Log. 21, 9–34 (2011)MathSciNetCrossRef
10.
Dabrowski, A., Moss, L.S., Parikh, R.: Topological reasoning and the logic of knowledge. Ann. Pure Appl. Log. 78, 73–110 (1996)MathSciNetCrossRef
11.
12.
McCarthy, J.: Formalization of two puzzles involving knowledge. In: Formalizing Common Sense: Papers by John McCarthy, (Original 1978–81). Ablex Publishing Corporation (1990)
13.
Moss, L.S., Parikh, R.: Topological reasoning and the logic of knowledge. In: Proceedings of the 4th TARK, pp. 95–105. Morgan Kaufmann (1992)
14.
15.
van Benthem, J.: One is a Lonely Number: On the Logic of Communication. Lecture Notes in Logic, pp. 96–129. Cambridge University Press, Cambridge (2002)MATH
16.
17.
18.
19.
20.
van Ditmarsch, H., French, T., Pinchinat, S.: Future event logic-axioms and complexity. Adv. Modal Log. 8, 77–99 (2010)MathSciNetMATH
21.
22.
van Ditmarsch, H., Knight, S., Özgün, A.: Announcement as effort on topological spaces. In: Proceedings of the 15th TARK, pp. 95–102 (2015)
23.
van Ditmarsch, H., Knight, S., Özgün, A.: Announcement as effort on topological spaces–Extended version. Synthese, 1–43 (2015)
24.
van Ditmarsch, H., van der Hoek, W., Kuijer, L.B.: Fully arbitrary public announcements. Adv. Modal Log. 11, 252–267 (2016)MathSciNetMATH
25.
Wang, Y.N., Ågotnes, T.: Multi-agent subset space logic. In: Proceedings of the 23rd IJCAI, pp. 1155–1161. IJCAI/AAAI (2013)
26.
Metadata
Title
APAL with Memory Is Better
Authors
Alexandru Baltag
Aybüke Özgün
Ana Lucia Vargas Sandoval
Copyright Year
2018
Publisher
Springer Berlin Heidelberg
Book
Logic, Language, Information, and Computation

Print ISBN: 978-3-662-57668-7

Electronic ISBN: 978-3-662-57669-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-662-57669-4_6

Premium Partner

    Image Credits