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

2017/07/25 by Louwe B. Kuijer · 6 citations
Computer Science · Mathematics · #Advanced Algebra and Logic #Algorithm #Arrow #Artificial intelligence #Computer science #Discrete mathematics #Encoding (memory) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Operator (biology) #Programming language #Recursively enumerable language #Theoretical computer science #Turing machine #cs.LO

paper · pdf · doi:10.4204/eptcs.251.27

published in Electronic Proceedings in Theoretical Computer Science 251, 373-381 (Open Publishing Association) · In Proceedings TARK 2017, arXiv:1707.08250

openalex publication_date 2017/07/25 · arxiv created 2017/07/27 · arxiv updated 2017/07/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06

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.

Citations

• Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge
• On Computable Numbers, with an Application to the Entscheidungsproblem
• The Undecidability of Arbitrary Arrow Update Logic