Non-deterministic semantics for dynamic topological logic (Q1006607): Difference between revisions

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.