Labelled Natural Deduction for Public Announcement Logic with Common Knowledge

Abstract

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.

Keywords

• public announcement logic
• common knowledge
• labelled natural deduction
• dynamic logic
• epistemic logic
• proof theory