Non-finite axiomatizability of Dynamic Topological Logic

TL;DR

This paper proves that no finite axiomatization exists for any intermediate language between L and L* in dynamic topological logic, demonstrating the incompleteness of the KM proof system.

Contribution

It establishes the non-finite axiomatizability of all intermediate languages between L and L* in DTL, resolving a long-standing conjecture about the incompleteness of KM.

Findings

No finite axiomatization for any language between L and L*

The proof system KM is incomplete

Implications for the axiomatizability of dynamic topological logic

Abstract

Dynamic topological logic (DTL) is a polymodal logic designed for reasoning about {\em dynamic topological systems. These are pairs (X,f), where X is a topological space and f:X->X is continuous. DTL uses a language L which combines the topological S4 modality [] with temporal operators from linear temporal logic. Recently, I gave a sound and complete axiomatization DTL* for an extension of the logic to the language L*, where <> is allowed to act on finite sets of formulas and is interpreted as a tangled closure operator. No complete axiomatization is known over L, although one proof system, which we shall call $\mathsf{KM}$, was conjectured to be complete by Kremer and Mints. In this paper we show that, given any language L' between L and L*, the set of valid formulas of L' is not finitely axiomatizable. It follows, in particular, that KM is incomplete.