Arbitrary Arrow Update Logic with Common Knowledge is neither RE nor co-RE

TL;DR

This paper demonstrates that the logic AAULC, which models information updates with common knowledge, has a non-recursively enumerable set of valid and satisfiable formulas, indicating it lacks a recursive axiomatization.

Contribution

It proves that AAULC's valid and satisfiable formulas are not recursively enumerable by encoding Turing machine executions within the logic.

Findings

Neither valid nor satisfiable formulas of AAULC are recursively enumerable

AAULC does not admit a recursive axiomatization

Encoding Turing machines in AAULC shows its computational complexity

Abstract

Arbitrary Arrow Update Logic with Common Knowledge (AAULC) is a dynamic epistemic logic with (i) an arrow update operator, which represents a particular type of information change and (ii) an arbitrary arrow update operator, which quantifies over arrow updates. By encoding the execution of a Turing machine in AAULC, we show that neither the valid formulas nor the satisfiable formulas of AAULC are recursively enumerable. In particular, it follows that AAULC does not have a recursive axiomatization.