2012/07/21 by Fernández-Duque, David
#FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1207.5140
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 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.