Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is $\Sigma^1_1$-hard

TL;DR

This paper proves that the satisfiability problem for Arbitrary Public Announcement Logic with Common Knowledge is highly complex, non-recursively enumerable, and not finitely axiomatisable, indicating significant computational and theoretical challenges.

Contribution

It establishes the $ ext{Sigma}^1_1$-hardness of APALC satisfiability, showing its extreme computational complexity and non-axiomatizability.

Findings

Satisfiability of APALC is $ ext{Sigma}^1_1$-hard.

APALC is not recursively enumerable.

APALC cannot be finitely axiomatised.

Abstract

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 $\Sigma^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.