Dynamic topological logic interpreted over minimal systems
type: Item
instance of: scholarly article
title: Dynamic topological logic interpreted over minimal systems
zbMATH Open document ID: 1243.03027
published in: Journal of Philosophical Logic
publication date: 2012-03-23T00:00:00Z
review text: This investigation of a propositional logical system has a chance to be interesting to mainstream mathematicians. Dynamic topological logic studies dynamic topological systems in a modal-temporal propositional language with connectives \(\square\) (interior of a set), \(\circ\) (next) and \(*\) (always in future). A dynamic system is minimal if no proper subset of the carrier space is invariant (under a continuous function interpreting the \(\circ\) connective). The author proves that the logic \(\mathrm {DTL}_\mathcal{M}\) of minimal systems in this language is decidable. This is established via a kind of finite model property using Kruskal's lemma. Since this lemma has complexity far exceeding one of the first-order arithmetic, \(\mathrm {DTL}_\mathcal{M}\) may turn out to be the first example of a useful propositional system with impredicative complexity. On the negative side, \(\mathrm {DTL}_\mathcal{M}\) in not Kripke-complete, since the unit circle under the action of an irrations rotation refutes the formula \({*}\square\, p\to \square {*}p\), which is valid for dynamic systems based on Aleksandrov spaces. The main part of the paper is taken up by the completeness proof for systems of Kripke models called here nondeterministic quasimodels. A non-primitive recursive lower complexity bound is established by embedding DTL with finite iterations into \(\mathrm {DTL}_\mathcal{M}\). Although decidability implies axiomatizability, no familiar-style recursive axiomatization for \(\mathrm {DTL}_\mathcal{M}\) is known. The general propositional logic DTL of dynamic topological systems was proved by the author to be recursively enumerable, but no familiar-style recursive axiomatization is known either. However, the author proves that the schema \(\exists \square\phi\to \forall\neg*\neg\phi\) axiomatizes \(\mathrm {DTL}_\mathcal{M}\) over DTL.
reviewed by: G. E. Mints
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 37B10
zbMATH DE Number: 6018335
zbMATH Keywords: dynamic topological logic
zbMATH Keywords: logic of dynamic systems
zbMATH Keywords: spatial logic
zbMATH Keywords: temporal logic
zbMATH Keywords: multimodal logic
zbMATH Keywords: topological dynamics
author: David Fernández-Duque
MaRDI profile type: Publication
full work available at URL: s10992-010-9160-4
OpenAlex ID: W2053300126
Wikidata QID: Q58883310
cites work: Handbook of Spatial Logics
cites work: Q3135846
cites work: Q5767704
cites work: Dynamic Topological Completeness for
cites work: Non-deterministic semantics for dynamic topological logic
cites work: Non-primitive recursive decidability of products of modal logics with expanding domains
cites work: Q3509059
cites work: On dynamic topological and metric logics
cites work: The modal logic of continuous functions on Cantor space
cites work: Dynamic topological S5
cites work: The modal logic of continuous functions on the rational numbers
cites work: Dynamic topological logic
cites work: Propositional logic of continuous transformations in Cantor space
cites work: Der Aussagenkalkül und die Topologie
DOI: 10.1007/S10992-010-9160-4
description: scientific article; zbMATH DE number 6018335