Skip to main content
SpringerLink
Log in

The Proof Theory of Common Knowledge

  • Chapter
  • First Online:
Jaakko Hintikka on Knowledge and Game-Theoretical Semantics

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 12))

Abstract

Common knowledge of a proposition A can be characterized by the following infinitary conjunction: everybody knows A and everybody knows that everybody knows A and everybody knows that everybody knows that everybody knows A and so on. We present a survey of deductive systems for the logic of common knowledge. In particular, we present two different Hilbert-style axiomatizations and two infinitary cut-free sequent systems. Further we discuss the problem of syntactic cut-elimination for common knowledge. The paper concludes with a list of open problems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

References

  1. Abate P, Goré R, Widmann F (2007) Cut-free single-pass tableaux for the logic of common knowledge. In: Workshop on agents and deduction at TABLEAUX 2007

    Google Scholar 

  2. Alberucci L, Jäger G (2005) About cut elimination for logics of common knowledge. Ann Pure Appl Log 133:73–99

    Google Scholar 

  3. Antonakos E (2007) Justified and common knowledge: limited conservativity. In: Artemov SN, Nerode A (eds) Logical foundations of computer science, LFCS 2007. LNCS, vol 4514. Springer, pp 1–11

    Google Scholar 

  4. Antonakos E (2013) Explicit generic common knowledge. In: Artemov S, Nerode A (eds) Logical foundations of computer science. Lecture Notes in Computer Science, vol 7734. Springer, pp 16–28

    Google Scholar 

  5. Antonakos E (2016) Pairing traditional and generic common knowledge. In: Artemov S, Nerode A (eds) Logical foundations of computer science. Lecture Notes in Computer Science, vol 9537. Springer, pp 14–26

    Google Scholar 

  6. Artemov S (2001) Explicit provability and constructive semantics. Bull Symb Log 7(1):1–36

    Google Scholar 

  7. Artemov S (2006) Justified common knowledge. Theor Comput Sci 357(1):4–22

    Google Scholar 

  8. Aumann R (1976) Agreeing to disagree. Ann Stat 4(6):1236–1239

    Google Scholar 

  9. Barwise J (1988) Three views of common knowledge. In: Vardi M (ed) Proceedings of theoretical aspects of reasoning about knowledge. Morgan Kaufman, pp 365–379

    Google Scholar 

  10. Barwise J (1989) The situation in logic. In: CSLI lecture notes, vol 17

    Google Scholar 

  11. Brünnler K (2006) Deep sequent systems for modal logic. In: Governatori G, Hodkinson I, Venema Y (eds) Advances in modal logic, vol 6. College Publications, pp 107–119

    Google Scholar 

  12. Brünnler K, Lange M (2008) Cut-free sequent systems for temporal logics. J Log Algeb Program 76:216–225

    Google Scholar 

  13. Brünnler K, Studer T (2009) Syntactic cut-elimination for common knowledge. Ann Pure Appl Log 160:82–95. https://doi.org/10.1016/j.apal.2009.01.014

  14. Brünnler K, Studer T (2012) Syntactic cut-elimination for a fragment of the modal mu-calculus. Ann Pure Appl Log 163(12):1838–1853

    Google Scholar 

  15. Bucheli S (2012) Justification logics with common knowledge. PhD thesis, Universität Bern

    Google Scholar 

  16. Bucheli S, Kuznets R, Studer T (2010) Two ways to common knowledge. In: Bolander T, Braüner T (eds) Proceedings of the 6th workshop on methods for modalities (M4M–6 2009), Copenhagen, Denmark, 12–14 Nov 2009. Electronic Notes in Theoretical Computer Science. Elsevier, pp 83–98. https://doi.org/10.1016/j.entcs.2010.04.007

  17. Bucheli S, Kuznets R, Studer T (2011) Justifications for common knowledge. J Appl Non-Class Log 21(1):35–60. https://doi.org/10.3166/JANCL.21.35-60

  18. Buchholz W (1981) The \(\Omega _{\mu +1}\)-rule. In: Buchholz W, Feferman S, Pohlers W, Sieg W (eds) Iterated inductive definitions and subsystems of analysis: recent proof theoretic studies. Lecture Notes in Mathematics, vol 897. Springer, pp 189–233. https://doi.org/10.1007/BFb0091898

  19. Dax C, Hofmann M, Lange M (2006) A proof system for the linear time \(\mu \)-calculus. In: Proceedings of the 26th conference on foundations of software technology and theoretical computer science, FSTTCS’06. LNCS, vol 4337. Springer, pp 274–285

    Google Scholar 

  20. Fagin R, Halpern JY, Moses Y, Vardi MY (1995) Reasoning about knowledge. MIT Press

    Google Scholar 

  21. Fontaine G (2008) Continuous fragment of the mu-calculus. In: Kaminski M, Martini S (eds) Computer science logic. LNCS, vol 5213. Springer, pp 139–153. https://doi.org/10.1007/978-3-540-87531-4-12

  22. Goré R (2014) And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Demri S, Kapur D Weidenbach C (eds) Automated reasoning: 7th International Joint Conference, IJCAR 2014. Proceedings. Springer, pp 26–45. https://doi.org/10.1007/978-3-319-08587-6-3

  23. Grädel E, Thomas W, Wilke T (eds) (2002) Automata logics, and infinite games: a guide to current research. Springer. ISBN 3-540-00388-6

    Google Scholar 

  24. Gudzhinskas E (1982) Syntactical proof of the elimination theorem for von Wrights temporal logic. Math Logika Primenen 2:113–130

    Google Scholar 

  25. Halpern JY, Moses Y (1990) Knowledge and common knowledge in a distributed environment. J ACM 37(3):549–587

    Google Scholar 

  26. Hintikka J (1962). Knowledge and belief: an introduction to the logic of the two notions. Cornell University Press

    Google Scholar 

  27. Jäger G, Marti M (2015) Intuitionistic common knowledge or belief

    Google Scholar 

  28. Jäger G, Studer T (2011) A Buchholz rule for modal fixed point logics. Logica Universalis 5:1–19. https://doi.org/10.1007/s11787-010-0022-1

  29. Jäger G, Kretz M, Studer T (2007) Cut-free common knowledge. J Appl Log 5(4):681–689

    Google Scholar 

  30. Kashima R (1994) Cut-free sequent calculi for some tense logics. Studia Logica 53(1):119–136

    Google Scholar 

  31. Kokkinis I, Studer T (2016) Cyclic proofs for linear temporal logic. In: Probst D, Schuster P (eds) Concepts of proof in mathematics, philosophy, and computer science. Ontos mathematical logic, vol 6. De Gruyter

    Google Scholar 

  32. Kretz M, Studer T (2006) Deduction chains for common knowledge. J Appl Log 4:331–357

    Google Scholar 

  33. Kuznets R, Studer T (2012) Justifications, ontology, and conservativity. In: Bolander T, Braüner T, Ghilardi S, Moss L (eds) AiML 9. College Publications, pp 437–458

    Google Scholar 

  34. Kuznets R, Studer T (2013) Update as evidence: belief expansion. In: Artemov SN, Nerode A (eds) Logical foundations of computer science LFCS 13. LNCS, vol 7734. Springer, pp 266–279

    Google Scholar 

  35. Lange M, Stirling C (2001) Focus games for satisfiability and completeness of temporal logic. In: Proceedings of LICS

    Google Scholar 

  36. Leivant D (1981) A proof theoretic methodology for propositional dynamic logic. In: Proceedings of the international colloquium on formalization of programming concepts. LNCS. Springer, pp 356–373

    Google Scholar 

  37. Lewis D (1969) Convention: a philosophical study

    Google Scholar 

  38. Martin D (1975) Borel determinacy. Ann Math 102:363–371

    Google Scholar 

  39. McCarty J, Sato M, Hayashi T, Igarishi S (1978) On the model theory of knowledge. Technical report STAN-CS-78-657. Stanford University

    Google Scholar 

  40. Meyer J-J, van der Hoek W (1995) Epistemic logic for AI and computer science. Cambridge University Press

    Google Scholar 

  41. Mints G, Studer T (2012) Cut-elimination for the mu-calculus with one variable. In: Fixed points in computer science 2012. EPTCS, vol 77. Open Publishing Association, pp 47–54

    Google Scholar 

  42. Niwinski D, Walukiewicz I (1996) Games for the mu-calculus. Theor Comput Sci 163(1&2):99–116

    Google Scholar 

  43. Paech B (1989) Gentzen-systems for propositional temporal logics. In: Börger E, Büning HK, Richter MM (eds) CSL ’88: 2nd Workshop on Computer Science Logic, Proceedings. Springer, pp 240–253. https://doi.org/10.1007/BFb0026305

  44. Poggiolesi F, Hill B (2015) Common knowledge: a finitary calculus with a syntactic cut-elimination procedure. Logique et Analyse 58(230):136–159

    Google Scholar 

  45. Pohlers W (1989) Proof theory—an introduction. Springer

    Google Scholar 

  46. Pohlers W (1998) Subsystems of set theory and second order number theory. In: Buss S (ed) Handbook of proof theory. Elsevier, pp 209–335

    Google Scholar 

  47. Schelling T (1960) The strategy of conflict

    Google Scholar 

  48. Schiffer S (1972) Meaning

    Google Scholar 

  49. Schütte K (1977) Proof theory. Springer

    Google Scholar 

  50. Streett RS, Emerson EA (1989) An automata theoretic decision procedure for the propositional modal mu-calculus. Inf Comput 81:249–264

    Google Scholar 

  51. Studer T (2009) Common knowledge does not have the Beth property. Inf Process Lett 109:611–614

    Google Scholar 

  52. van Benthem J, van Eijck J, Kooi B (2005) Common knowledge in update logics. In: Proceedings of the 10th conference on theoretical aspects of rationality and knowledge, TARK ’05, pp 253–261. ISBN 981-05-3412-4

    Google Scholar 

  53. Wehbe R (2010) Annotated systems for common knowledge. PhD thesis, Universität Bern

    Google Scholar 

Download references

Acknowledgements

We would like to thank Rajeev Goré for many helpful comments. This research is supported by the SNSF project 153169.

Author information

Authors and Affiliations

  1. University of Bern, Neubrückstrasse 10, 3012, Bern, Switzerland

    Michel Marti & Thomas Studer

Authors
  1. Michel Marti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Studer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michel Marti .

Editor information

Editors and Affiliations

  1. LORIA, CNRS, Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Hans van Ditmarsch

  2. Department of Philosophy, University of Helsinki, Helsinki, Finland

    Gabriel Sandu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Marti, M., Studer, T. (2018). The Proof Theory of Common Knowledge. In: van Ditmarsch, H., Sandu, G. (eds) Jaakko Hintikka on Knowledge and Game-Theoretical Semantics. Outstanding Contributions to Logic, vol 12. Springer, Cham. https://doi.org/10.1007/978-3-319-62864-6_18

Download citation

Publish with us

Policies and ethics

Search

Navigation