Non-deterministic semantics for dynamic topological logic

DOI10.1016/J.APAL.2008.09.015MaRDI QIDQ1006607zbMATH OpenOpenAlexFDO

Authors David Fernández

Publication date 25 March 2009

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1611.06735

zbMATH Keywords

dynamic topological logicspatial logictemporal logictyped Kripke frames

Mathematics Subject Classification ID

Temporal logic (03B44) Modal logic (including the logic of norms) (03B45)

Abstract: Dynamic Topological Logic ($mathcalDTL$) is a combination of $mathcalS${em 4}, under its topological interpretation, and the temporal logic $mathcalLTL$ interpreted over the natural numbers. $mathcalDTL$ is used to reason about properties of dynamical systems based on topological spaces. Semantics are given by dynamic topological models, which are tuples $left<X,mathcalT,f,Vight>$, where $left<X,mathcalTight>$ is a topological space, $f$ a function on $X$ and $V$ a truth valuation assigning subsets of $X$ to propositional variables.

Review text

This paper belongs to a program of propositional dynamic topological logic DTL intended to bridge a gap between logic and mainstream mathematics. The models of DTL are dynamical systems \((X,T,f)\) consisting of a topological space \((X,T)\) and a continuous function \(f\) on this space. The atomic formulas (propositional variables) are interpreted by subsets of \(X\), the Boolean operations are standard, the modality \(\square\) is the topological interior. The temporal connective \(\circ\) is the ``next operator: the point \(x\) is in \(\circ A\) iff \(f(x)\) is in \(A\). The temporal connective \(*A\) is interpreted as ``always in the future, more precisely as the intersection of \(A, \circ A,\circ\circ A,\) etc. In this way the dual connective \(\#A=\widetilde*\widetilde A\) is interpreted as the orbit of \(A\). This paper proves that DTL (with continuous functions) is recursively enumerable. The proof uses essentially all tools accumulated up to now in this area. This seems to be one of the first (maybe the first) examples of an undecidable but axiomatizable interesting propositional system introduced by semantics and not by an axiom system. The problem of axiomatizing DTL is still open. Ordinary Kripke models turn out to be insufficient to obtain axiomatizability and decidability results. The author uses (what he calls) typed Kripke frames, i.e. frames with sufficiently saturated sets of formulas assigned to each world. The main Kripke-style object is a non-deterministic quasi-model \((W,R,t,g)\): a typed frame \((W,R,t)\) with a typing \(t\), plus a continuous relation (instead of a function) on worlds, \(g: W \to W\). These objects satisfy some coherence conditions which constitute one of the achievements of this work. To check the correspondence with the original semantics of dynamical systems, a transformation of a non-deterministic quasi-model into an equivalent dynamical system is defined. Limit models and a shift operator appear here. A hierarchy of finite frames is designed to get an analog of a finite-model property. Kruskal's lemma is applied to get an enumeration of unsatisfiable formulas of DTL.

Recommendations

• Dynamic topological logic interpreted over minimal systems
• Dynamic topological logic
• Dynamic topological logic of metric spaces

Cites work

• Dynamic Topological Completeness for
• Dynamic topological logic
• scientific article; zbMATH DE number 5295716 (Why is no real title available?)
• Modal logic
• On completeness of dynamic topological logic
• On dynamic topological and metric logics
• Propositional temporal logics: decidability and completeness
• The modal logic of continuous functions on the rational numbers
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(16)

• Dynamic topological S5
• A sound and complete axiomatization for dynamic topological logic
• Strict canonical constructive systems
• scientific article; zbMATH DE number 3943004 (Why is no real title available?)
• The intuitionistic temporal logic of dynamical systems
• Complete intuitionistic temporal logics for topological dynamics
• Completeness of a functional system for surjective functions
• Convergence, continuity, recurrence and Turing completeness in dynamic epistemic logic1
• Dynamic topological logic of metric spaces
• Time and Gödel: fuzzy temporal reasoning in PSPACE
• Gödel-Dummett linear temporal logic
• Dynamic topological logic
• On the modal definability of simulability by finite transitive models
• Tangled modal logic for topological dynamics
• Dynamic topological logic interpreted over minimal systems
• Non-deterministic semantics for logics with a consistency operator

This page was built for publication: Non-deterministic semantics for dynamic topological logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1006607)