Labelled Natural Deduction for Public Announcement Logic with Common Knowledge
Muhammad Farhan Mohd Nasir, Wan Ainun Mior Othman, Kok Bin Wong · Mathematics · 2020
Public announcement logic is a logic that studies epistemic updates. In this paper, we propose a sound and complete labelled natural deduction system for public announcement logic with the common knowledge operator (PAC). The completeness of the proposed system is proved indirectly through a Hilbert calculus for PAC known to be complete and sound. We conclude with several discussions regarding the system including some problems of the system in attaining normalisation and subformula property.