Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is Σ^1_1-hard
Original version
R. Verbrugge (Ed.): Theoretical Aspects of Rationality and Knowledge 2023 (TARK 2023) EPTCS 379, 2023, pp. 260-271. http://dx.doi.org/10.4204/EPTCS.379.21Abstract
Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an extension of Public Announcement Logic with common knowledge modality and quantifiers over announcements. We show that the satisfiability problem of APALC on S5-models, as well as that of two other related logics with quantification and common knowledge, is Σ1 1-hard. This implies that neither the validities nor the satisfiable formulas of APALC are recursively enumerable. Which, in turn, implies that APALC is not finitely axiomatisable.