The coinductive formulation of common knowledge
We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rather than as a logical derivation system. We have two...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
2018
|
| Online Access: | https://eprints.nottingham.ac.uk/53576/ |
| _version_ | 1848798959658598400 |
|---|---|
| author | Baston, Colm Capretta, Venanzio |
| author_facet | Baston, Colm Capretta, Venanzio |
| author_sort | Baston, Colm |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rather than as a logical derivation system. We have two major new results. Firstly, the operator semantics is equivalent to the relational semantics: we discovered that this requires a new hypothesis of semantic entailment on operators, not known in previous literature. Secondly, the coinductive version of common knowledge is equivalent to the traditional transitive closure on the relational interpretation. All results are formalised in the proof assistants Agda and Coq. |
| first_indexed | 2025-11-14T20:28:03Z |
| format | Conference or Workshop Item |
| id | nottingham-53576 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T20:28:03Z |
| publishDate | 2018 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-535762018-08-31T10:13:23Z https://eprints.nottingham.ac.uk/53576/ The coinductive formulation of common knowledge Baston, Colm Capretta, Venanzio We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rather than as a logical derivation system. We have two major new results. Firstly, the operator semantics is equivalent to the relational semantics: we discovered that this requires a new hypothesis of semantic entailment on operators, not known in previous literature. Secondly, the coinductive version of common knowledge is equivalent to the traditional transitive closure on the relational interpretation. All results are formalised in the proof assistants Agda and Coq. 2018-07-04 Conference or Workshop Item PeerReviewed application/pdf en https://eprints.nottingham.ac.uk/53576/1/common_knowledge.pdf Baston, Colm and Capretta, Venanzio (2018) The coinductive formulation of common knowledge. In: ITP 2018 - Interactive Theorem Proving, 9-12 August 2018, Oxford, UK. https://link.springer.com/chapter/10.1007%2F978-3-319-94821-8_8 10.1007/978-3-319-94821-8_8 10.1007/978-3-319-94821-8_8 10.1007/978-3-319-94821-8_8 |
| spellingShingle | Baston, Colm Capretta, Venanzio The coinductive formulation of common knowledge |
| title | The coinductive formulation of common knowledge |
| title_full | The coinductive formulation of common knowledge |
| title_fullStr | The coinductive formulation of common knowledge |
| title_full_unstemmed | The coinductive formulation of common knowledge |
| title_short | The coinductive formulation of common knowledge |
| title_sort | coinductive formulation of common knowledge |
| url | https://eprints.nottingham.ac.uk/53576/ https://eprints.nottingham.ac.uk/53576/ https://eprints.nottingham.ac.uk/53576/ |