Dynamical systems provide rigorous models of movement or evolution over time. Due to their abstract nature, they may be naturally employed for representing e.g. physical, biological, or financial phenomena. Specifically in the context of Computer Science, computational processes, machine learning algorithms, and multi-agent systems may be regarded as dynamical systems. This has sparked interest in designing formal specification languages for dynamical systems which could potentially be employed for automated or computer-assisted deduction, leading to the introduction of dynamic topological logic (DTL). When space is continuous but time is discrete, it is known that a sound and complete deductive calculus for DTL exists. However, discrete spaces are not uncommon in CS applications , and in this setting, whether such a calculus exists even in principle has been an open question for more than two decades. More precisely, it was unknown whether the DTL of Alexandrov spaces is computably enumerable. In this paper, we use model search techniques to provide an affirmative answer.

In this paper we present a topological epistemic logic, with modalities for knowledge (modelled as the universal modality), knowability (represented by the topological interior operator), and unknowability of the actual world. The last notion has a non-self-referential reading (modelled by Cantor derivative: the set of limit points of a given set) and a self-referential one (modelled by Cantor's perfect core of a given set: its largest subset without isolated points, where x is isolated iff { x } is open). We completely axiomatize this logic, showing that it is decidable and pspace -complete, and we apply it to the analysis of a famous epistemic puzzle: the Surprise Exam Paradox.

Dynamical systems are abstract models of interaction between space and time. They are often used in fields such as physics and engineering to understand complex processes, but due to their general nature, they have found applications for studying computational processes, interaction in multi-agent systems, machine learning algorithms and other computer science related phenomena. In the vast majority of applications, a dynamical system consists of the action of a continuous `transition function' on a metric space. In this work, we consider decidable formal systems for reasoning about such structures. Spatial logics can be traced back to the 1940's, but our work follows a more dynamic turn that these logics have taken due to two recent developments: the study of the topological mu-calculus, and the the integration of linear temporal logic with logics based on the Cantor derivative. In this paper, we combine dynamic topological logics based on the Cantor derivative and the `next point in time' operators with an expressively complete fixed point operator to produce a combination of the topological mu-calculus with linear temporal logic. We show that the resulting logics are decidable and have a natural axiomatisation. Moreover, we prove that these logics are complete for interpretations on the Cantor space, the rational numbers, and subspaces thereof.

Intuitionistic linear temporal logic (iLTL) has been studied extensively, especially in the last decade. It enjoys natural semantics over intuitionistic Kripke frames equipped with an order-preserving function representing the temporal dynamics, known as 'expanding models'. This leads to a logic that is known to be decidable but whose axiomatisation has long remained open. We propose an extension of iLTL with the co-implication connective of Hilbert–Brouwer logic and call it 'bi-intuitionistic linear temporal logic' (biLTL). We establish that this extension is still decidable for the class of expanding models. We moreover give a sound and complete Hilbert-style calculus for it, the first for any logic extending iLTL. As a corollary, the topological semantics for intuitionistic propositional logic cannot be extended to a topological semantics for Hilbert-Brouwer logic, which thus establishes co-implication as a distinctive feature of the Kripke semantics for bi-intuitionistic logic.

Hardy functions are defined by transfinite recursion and provide upper bounds for the growth rate of the provably total computable functions in various formal theories, making them an essential ingredient in many proofs of independence. Their definition is contingent on a choice of fundamental sequences, which approximate limits in a ‘canonical’ way. In order to ensure that these functions behave as expected, including the aforementioned unprovability results, these fundamental sequences must enjoy certain regularity properties. In this article, we prove that Buchholz's system of fundamental sequences for the ϑ function enjoys such conditions, including the Bachmann property. We partially extend these results to variants of the ϑ function, including a version without addition for countable ordinals. We conclude that the Hardy functions based on these notation systems enjoy natural monotonicity properties and majorize all functions defined by primitive recursion along the Bachmann Howard ordinal.

Abstract The Baire algebra of a topological space X is the quotient of the algebra of all subsets of X modulo the meager sets. We show that this Boolean algebra can be endowed with a natural closure operator, resulting in a closure algebra which we denote $\mathbf {Baire}(X)$ . We identify the modal logic of such algebras to be the well-known system $\mathsf {S5}$ , and prove soundness and strong completeness for the cases where X is crowded and either completely metrizable and continuum-sized or locally compact Hausdorff. We also show that every extension of $\mathsf {S5}$ is the modal logic of a subalgebra of $\mathbf {Baire}(X)$ , and that soundness and strong completeness also holds in the language with the universal modality.

Abstract Modal logic enjoys topological semantics that may be traced back to McKinsey and Tarski, and the classification of topological spaces via modal axioms is a lively area of research. In the past two decades, there has been interest in extending topological modal logic to the language of the mu-calculus, but previously no class of topological spaces was known to be mu-calculus definable that was not already modally definable. In this paper, we show that the full mu-calculus is indeed more expressive than standard modal logic, in the sense that there are classes of topological spaces (and weakly transitive Kripke frames), which are mu-definable but not modally definable. The classes we exhibit satisfy a modally definable property outside of their perfect core, and thus we dub them imperfect spaces. We show that the mu-calculus is sound and complete for these classes. Our examples are minimal in the sense that they use a single instance of a greatest fixed point, and we show that least fixed points alone do not suffice to define any class of spaces that is not already modally definable.

Dynamical systems are general models of change or movement over time with a broad area of applicability to many branches of science, including computer science and AI. Dynamic topological logic (DTL) is a formal framework for symbolic reasoning about dynamical systems. DTL can express various liveness and reachability conditions on such systems, but has the drawback that the only known axiomatisation requires an extended language. In this paper, we consider dynamic topological logic restricted to the class of scattered spaces. Scattered spaces appear in the context of computational logic as they provide semantics for provability and enjoy definable fixed points. We exhibit the first sound and complete dynamic topological logic in the original language of DTL. In particular, we show that the version of DTL based on the class of scattered spaces is finitely axiomatisable, and that the natural axiomatisation is sound and complete.

We investigate intuitionistic logics extended both with the co-implication connective of Hilbert-Brouwer logic and with diamond and box modalities. We use a Kripke semantics based on frames with two 'forth' confluence conditions on the modal relation with respect to the intuitionistic relation. We give sound and strongly complete axiomatisations for entailment on this class of frames, and give similar axiomatisations for the subclasses of frames satisfying any combination of reflexivity, transitivity, and seriality. We then prove that all of these logics are decidable, by proving that they have the finite frame property.

The µ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto’s modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor’s perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key ‘test case’ for an expressively complete fragment of the µ-calculus.

We study the topological μ-calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability, and finite model property over general topological spaces, as well as overT0andTDspaces. We also investigate the relational μ-calculus, providing general completeness results for all natural fragments of the μ-calculus over many different classes of relational frames. Unlike most other such proofs for μ-calculi, ours is model theoretic, making an innovative use of a known method from modal logic (the ‘final’ submodel of the canonical model), which has the twin advantages of great generality and essential simplicity.

Topological semantics for modal logic based on the Cantor derivative operator gives rise to derivative logics, also referred to as $d$-logics. Unlike logics based on the topological closure operator, $d$-logics have not previously been studied in the framework of dynamical systems, which are pairs $(X,f)$ consisting of a topological space $X$ equipped with a continuous function $f\colon X\to X$. We introduce the logics $\bf{wK4C}$, $\bf{K4C}$ and $\bf{GLC}$ and show that they all have the finite Kripke model property and are sound and complete with respect to the $d$-semantics in this dynamical setting. In particular, we prove that $\bf{wK4C}$ is the $d$-logic of all dynamic topological systems, $\bf{K4C}$ is the $d$-logic of all $T_D$ dynamic topological systems, and $\bf{GLC}$ is the $d$-logic of all dynamic topological systems based on a scattered space. We also prove a general result for the case where $f$ is a homeomorphism, which in particular yields soundness and completeness for the corresponding systems $\bf{wK4H}$, $\bf{K4H}$ and $\bf{GLH}$. The main contribution of this work is the foundation of a general proof method for finite model property and completeness of dynamic topological $d$-logics. Furthermore, our result for $\bf{GLC}$ constitutes the first step towards a proof of completeness for the trimodal topo-temporal language with respect to a finite axiomatisation -- something known to be impossible over the class of all spaces.

Abstract The language of linear temporal logic can be interpreted on the class of dynamic topological systems, giving rise to the intuitionistic temporal logic ${\sf ITL}^{\sf c}_{\Diamond \forall }$ , recently shown to be decidable by Fernández-Duque. In this article we axiomatize this logic, some fragments, and prove completeness for several familiar spaces.

Abstract Japaridze’s provability logic ${\operatorname {GLP}}$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano arithmetic (${\operatorname {PA}}$) and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies (${\operatorname {EWD}}$) principle, a natural combinatorial statement independent of ${\operatorname {PA}}$. Recently, Beklemishev and Pakhomov have studied notions of provability corresponding to transfinite modalities in ${\operatorname {GLP}}$. We show that indeed the natural transfinite extension of ${\operatorname {GLP}}$ is sound for this interpretation and yields independent combinatorial principles for the second-order theory ${\operatorname {ACA}}$ of arithmetical comprehension with full induction. We also provide restricted versions of ${\operatorname {EWD}}$ related to the fragments ${\operatorname {I\varSigma }}_n$ of PA. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.

The logics CS4 and IS4 are intuitionistic variants of the modal logic S4. Whether the finite model property holds for each of these logics has been a long-standing open problem. In this paper we introduce two logics closely related to IS4: GS4, obtained by adding the Gödel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that CS4, GS4, and S4I all enjoy the finite model property.

We study the topological μ-calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability and FMP over general topological spaces, as well as over T0 and TD spaces. We also investigate relational μ-calculus, providing general completeness results for all natural fragments of μ-calculus over many different classes of relational frames. Unlike most other such proofs for μ-calculus, ours is modeltheoretic, making an innovative use of a known Modal Logic method (-the 'final' submodel of the canonical model), that has the twin advantages of great generality and essential simplicity.

Abstract The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible to extend functional programming languages with new features via type theory, while from the semantics perspective, several logics for reasoning about dynamical systems and several semantics for logic programming have their roots in this framework. We consider several axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. We provide two distinct interpretations of “henceforth”, both of which are natural intuitionistic variants of the classical one. We completely establish the order relation between the semantically defined logics based on both interpretations of “henceforth” and, using our soundness results, show that the axiomatically defined logics enjoy the same order relations.

We consider intuitionistic variants of linear temporal logic with “next,” “until,” and “release” based on expanding posets : partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic that we denote ITL e , and by imposing additional constraints, we obtain the logics ITL p of persistent posets and ITL ht of here-and-there temporal logic, both of which have been considered in the literature. We prove that ITL e has the effective finite model property and hence is decidable, while ITL p does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the “until” and “release” operators are not definable in terms of each other, even over the class of persistent posets.

Evidence logics model agents' belief revision process as they incorporate and aggregate information obtained from multiple sources. This information is captured using neighbourhood structures, where individual neighbourhoods represent pieces of evidence. In this paper we propose an extended framework which allows one to explicitly quantify either the number of evidence sets, or effort, needed to justify a given proposition, provide a complete deductive calculus and a proof of decidability, and show how existing frameworks can be embedded into ours.

We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.

A dynamical system is a pair $(X,f)$, where $X$ is a topological space and $f\colon X\to X$ is continuous. Kremer observed that the language of propositional linear temporal logic can be interpreted over the class of dynamical systems, giving rise to a natural intuitionistic temporal logic. We introduce a variant of Kremer's logic, which we denote ${\sf ITL^c}$, and show that it is decidable. We also show that minimality and Poincar\'e recurrence are both expressible in the language of ${\sf ITL^c}$, thus providing a decidable logic expressive enough to reason about non-trivial asymptotic behavior in dynamical systems.

We introduce the logic ITL^e, an intuitionistic temporal logic based on structures (W,R,S), where R is used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITL^e are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a 'persistent' version of the logic, ITL^p, whose models are similar to Cartesian products. We prove that, unlike ITL^e, ITL^p does not have the finite model property.

In the Russian cards problem, Alice, Bob and Cath draw a, b and c cards, respectively, from a publicly known deck. Alice and Bob must then communicate their cards to each other without Cath learning who holds a single card. Solutions in the literature provide weak security, where Alice and Bob’s exchanges do not allow Cath to know with certainty who holds each card that is not hers, or perfect security, where Cath learns no probabilistic information about who holds any given card. We propose an intermediate notion, which we call $$\varepsilon $$ -strong security, where the probabilities perceived by Cath may only change by a factor of $$\varepsilon $$ . We then show that strategies based on affine or projective geometries yield $$\varepsilon $$ -strong safety for arbitrarily small $$\varepsilon $$ and appropriately chosen values of a, b, c.

Abstract Given a scattered space $\mathfrak{X} = \left( {X,\tau } \right)$ and an ordinal λ, we define a topology $\tau _{ + \lambda } $ in such a way that τ+0 = τ and, when $\mathfrak{X}$ is an ordinal with the initial segment topology, the resulting sequence {τ+λ}λ∈Ord coincides with the family of topologies $\left\{ {\mathcal{I}_\lambda } \right\}_{\lambda \in Ord} $ used by Icard, Joosten, and the second author to provide semantics for polymodal provability logics. We prove that given any scattered space $\mathfrak{X}$ of large-enough rank and any ordinal λ > 0, GL is strongly complete for τ+λ. The special case where $\mathfrak{X} = \omega ^\omega + 1$ and λ = 1 yields a strengthening of a theorem of Abashidze and Blass.

Abstract Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”. For a set of formulas Γ, define predicative oracle reflection for T over Γ (Pred–O–RFNΓ(T)) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then $$\forall \,\lambda < {\rm{\Lambda }}\,([\lambda |X]_T^{\rm{\Lambda }}\varphi \to \varphi ).$$ In particular, define predicative oracle consistency (Pred–O–Cons(T)) as Pred–O–RFN{0=1}(T). Our main result is as follows. Let ATR0 be the second-order theory of Arithmetical Transfinite Recursion, ${\rm{RCA}}_0^{\rm{*}}$ be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then, $${\rm{ATR}}_0 \equiv {\rm{RCA}}_0^{\rm{*}} + {\rm{Pred - O - Cons\ }}\left( {{\rm{RCA}}_0^{\rm{*}} } \right) \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - Cons\ }}\left( {{\rm{RCA}}_0^{\rm{*}} } \right) \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - RFN}}\,_{{\bf{\Pi }}_2^1 } \left( {{\rm{ACA}}} \right).$$ We may even replace ${\rm{RCA}}_0^{\rm{*}}$ by the weaker ECA0, the second-order analogue of Elementary Arithmetic. Thus we characterize ATR0, a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles.

International audience

Dynamic topological logic (DTL) is a polymodal logic designed for reasoning about 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, we 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 in the language L, although one proof system, which we shall call KM, was conjectured to be complete by Kremer and Mints. In this article, we show that given any language L' such that L ⊆ L' ⊆ L * , the set of valid formulas of L' is not finitely axiomatizable. It follows, in particular, that KM is incomplete.

Abstract For any ordinal Λ, we can define a polymodal logic GLPΛ, with a modality [ξ] for each ξ < Λ. These represent provability predicates of increasing strength. Although GLPΛ has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities, denoted . Later, Icard defined a topological model for which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary Λ. More generally, for each Θ, Λ we build a Kripke model and a topological model , and show that is sound for both of these structures, as well as complete, provided Θ is large enough.

Abstract Dynamic Topological Logic is a modal framework for reasoning about dynamical systems, that is, pairs 〈X, f〉 where X is a topological space and f: X → X a continuous function. In this paper we consider the case where X is a metric space. We first show that any formula which can be satisfied on an arbitrary dynamic topological system can be satisfied on one based on a metric space; in fact, this space can be taken to be countable and have no isolated points. Since any metric space with these properties is homeomorphic to the set of rational numbers, it follows that any satisfiable formula can be satisfied on a system based on ℚ. We then show that the situation changes when considering complete metric spaces, by exhibiting a formula which is not valid in general but is valid on the class of systems based on a complete metric space. While we do not attempt to give a full characterization of the set of valid formulas on this class we do give a relative completeness result; any formula which is satisfiable on a dynamical system based on a complete metric space is also satisfied on one based on the Cantor space.

Abstract Dynamic Topological Logic ( ) is a multimodal system for reasoning about dynamical systems. It is defined semantically and, as such, most of the work done in the field has been model-theoretic. In particular, the problem of finding a complete axiomatization for the full language of over the class of all dynamical systems has proven to be quite elusive. Here we propose to enrich the language to include a polyadic topological modality, originally introduced by Dawar and Otto in a different context. We then provide a sound axiomatization for over this extended language, and prove that it is complete. The polyadic modality is used in an essential way in our proof.

We consider an extension of the propositional modal logic S4 which allows ⋄ to act not only on isolated formulas, but also on sets of formulas. The interpretation of ⋄Γ is then given by the tangled closure of the valuations of formulas in Γ, which over finite transitive, reflexive models indicates the existence of a cluster satisfying Γ. This extension has been shown to be more expressive than the basic modal language: for example, it is equivalent to the bisimulation-invariant fragment of FOL over finite S4 models, whereas the basic modal language is weaker. However, previous analyses of this logic have been entirely semantic, and no proof system was available. In this paper we present a sound proof system for the polyadic S4 and prove that it is complete. The axiomatization is fairly standard, adding only the fixpoint axioms of the tangled closure to the usual S4 axioms. The proof proceeds by explicitly constructing a finite model from a consistent set of formulas.

It is known that both S4 and the Intuitionistic prepositional calculus Int are P-SPACE complete. This guarantees that there is a polynomial translation from each system into the other. However, no sound and faithful polynomial translation from S4 into Int is commonly known. The problem of finding one was suggested by Dana Scott during a very informal gathering of logicians in February 2005 at UCLA. Grigori Mints then brought it to my attention, and in this paper I present a solution. It is based on Kripke semantics and describes model-checking for S4 using formulas of Int. A simple translation from Int into S4, the Gödel-Tarski translation, is wellknown; given a formula φ of Int, one obtains by prefixing □ to every subformula. For example, . That the translation is sound and faithful can be seen by considering topological semantics, which assign open sets both to □-formulas of S4 and arbitrary formulas of Int; the interpretation of φ and turn out to be identical. See Tarski's paper [6] for details. Gödel's original paper can be found in [3]. In [2], Friedman and Flagg present a kind of inverse to Gödel-Tarski. Given a formula φ of S4 and a finite set of formulas Γ of Int, for each ε ∈ Γ one gets an intuitionistic formula given recursively by