Showing 1–50 of 53 results for author: Fernández-Duque, D

Logics of polyhedral reachability

Authors: Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia, David Fernández-Duque, David Gabelaia

Abstract: Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modali… ▽ More Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modality. Recently, a language with an Until-like spatial modality has been introduced, with demonstrated applicability to the analysis of 3D meshes via model checking. In this paper, we exhibit an axiom system for this logic, and show that it is complete with respect to polyhedral semantics. The proof consists of two major steps: First, we show that this logic, which is built over Grzegorczyk's system $\mathsf{Grz}$, has the finite model property. Subsequently, we show that every formula satisfied in a finite poset is also satisfied in a polyhedral model, thereby establishing polyhedral completeness. △ Less

Submitted 23 June, 2024; originally announced June 2024.

Comments: 17 pages, 1 figure, Advances in Modal Logics Conference

MSC Class: 03B45 (Primary) 03B70 (Secondary) ACM Class: F.4

Constructive S4 modal logics with the finite birelational frame property

Authors: Philippe Balbiani, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was recently shown that $\mathsf{IS4}$ has the finite frame property and thus the finite model property. In this paper, we prove that $\mathsf{CS4}$ also enjoys the finit… ▽ More The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was recently shown that $\mathsf{IS4}$ has the finite frame property and thus the finite model property. In this paper, we prove that $\mathsf{CS4}$ also enjoys the finite frame property. Additionally, we investigate the following three logics closely related to $\mathsf{IS4}$. The logic $\mathsf{GS4}$ is obtained by adding the Gödel--Dummett axiom to $\mathsf{IS4}$; it is both a superintuitionistic and a fuzzy logic and has previously been given a real-valued semantics. We provide an alternative birelational semantics and prove strong completeness with respect to this semantics. The extension $\mathsf{GS4^c}$ of $\mathsf{GS4}$ corresponds to requiring a crisp accessibility relation on the real-valued semantics. We give a birelational semantics corresponding to an extra confluence condition on the $\mathsf{GS4}$ birelational semantics and prove strong completeness. Neither of these two logics have the finite model property with respect to their real-valued semantics, but we prove that they have the finite frame property for their birelational semantics. Establishing the finite birelational frame property immediately establishes decidability, which was previously open for these two logics. Our proofs yield NEXPTIME upper bounds. The logic $\mathsf{S4I}$ is obtained from $\mathsf{IS4}$ by reversing the roles of the modal and intuitionistic relations in the birelational semantics. We also prove the finite frame property, and thereby decidability, for $\mathsf{S4I}$ △ Less

Submitted 15 March, 2024; v1 submitted 29 February, 2024; originally announced March 2024.

Comments: arXiv admin note: substantial text overlap with arXiv:2104.15053

Gödel-Dummett linear temporal logic

Authors: Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two… ▽ More We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This Gödel temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that Gödel temporal logic is PSPACE-complete. We also provide a deductive calculus for Gödel temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus. △ Less

Submitted 27 June, 2023; originally announced June 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2205.00574, arXiv:2205.05182

The universal tangle for spatial reasoning

Authors: David Fernández-Duque, Konstantinos Papafilippou

Abstract: The topological $μ$-calculus has gathered attention in recent years as a powerful framework for representation of spatial knowledge. In particular, spatial relations can be represented over finite structures in the guise of weakly transitive wK4 frames. In this paper we show that the topological $μ$-calculus is equivalent to a simple fragment based on a variant of the `tangle' operator. Similar re… ▽ More The topological $μ$-calculus has gathered attention in recent years as a powerful framework for representation of spatial knowledge. In particular, spatial relations can be represented over finite structures in the guise of weakly transitive wK4 frames. In this paper we show that the topological $μ$-calculus is equivalent to a simple fragment based on a variant of the `tangle' operator. Similar results were proven for transitive frames by Dawar and Otto, using modal characterisation theorems for the corresponding classes of frames. However, since these theorems are not available in our setting, which has the upshot of providing a more explicit translation and upper bounds on formula size. △ Less

Submitted 27 July, 2023; v1 submitted 6 April, 2023; originally announced April 2023.

Comments: 20 pages

MSC Class: 03B45 (Primary) 03B70 (Secondary) ACM Class: F.4.1; I.2.4

Metric fixed point theory and partial impredicativity

Authors: David Fernández-Duque, Paul Shafer, Henry Towsner, Keita Yokoyama

Abstract: We show that the Priess-Crampe & Ribenboim fixed point theorem is provable in $\mathsf{RCA}_0$. Furthermore, we show that Caristi's fixed point theorem for both Baire and Borel functions is equivalent to the transfinite leftmost path principle, which falls strictly between $\mathsf{ATR}_0$ and $Π^1_1\mbox{-}\mathsf{CA}_0$. We also exhibit several weakenings of Caristi's theorem that are equivalent… ▽ More We show that the Priess-Crampe & Ribenboim fixed point theorem is provable in $\mathsf{RCA}_0$. Furthermore, we show that Caristi's fixed point theorem for both Baire and Borel functions is equivalent to the transfinite leftmost path principle, which falls strictly between $\mathsf{ATR}_0$ and $Π^1_1\mbox{-}\mathsf{CA}_0$. We also exhibit several weakenings of Caristi's theorem that are equivalent to $\mathsf{WKL}_0$ and to $\mathsf{ACA}_0$. △ Less

Submitted 17 February, 2023; originally announced February 2023.

Dynamic Tangled Derivative Logic of Metric Spaces

Authors: David Fernández-Duque, Yoàv Montacute

Abstract: 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 majori… ▽ More 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. △ Less

Submitted 24 January, 2023; originally announced January 2023.

Comments: arXiv admin note: text overlap with arXiv:2107.10349

A Gödel Calculus for Linear Temporal Logic

Authors: Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show thi… ▽ More We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show this calculus to be sound and complete for the above-mentioned semantics. △ Less

Submitted 10 May, 2022; originally announced May 2022.

Comments: arXiv admin note: text overlap with arXiv:2205.00574

Journal ref: Principles of Knowledge Representation and Reasoning, Proceedings of the 19th International Conference (August 2022) 2-11

Time and Gödel: Fuzzy temporal reasoning in PSPACE

Authors: Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: We investigate a non-classical version of linear temporal logic whose propositional fragment is Gödel--Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics, a real-valued semantics and a bi-relational semantics, and show that these indeed define one and the same logic. Although this Gödel temporal logic do… ▽ More We investigate a non-classical version of linear temporal logic whose propositional fragment is Gödel--Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics, a real-valued semantics and a bi-relational semantics, and show that these indeed define one and the same logic. Although this Gödel temporal logic does not have any form of the finite model property for these two semantics, we show that every falsifiable formula is falsifiable on a finite quasimodel, which yields decidability of the logic. We then strengthen this result by showing that this Gödel temporal logic is PSPACE-complete. △ Less

Submitted 1 May, 2022; originally announced May 2022.

Journal ref: Workshop on Logic, Language, Information, and Computation (WoLLIC), proceedings of the 28th International Workshop (September 2022), pp. 18-35

Untangled: A Complete Dynamic Topological Logic

Authors: David Fernández-Duque, Yoàv Montacute

Abstract: Dynamic topological logic ($\mathbf{DTL}$) is a trimodal logic designed for reasoning about dynamic topological systems. It was shown by Fernández-Duque that the natural set of axioms for $\mathbf{DTL}$ is incomplete, but he provided a complete axiomatisation in an extended language. In this paper, we consider dynamic topological logic over scattered spaces, which are topological spaces where ever… ▽ More Dynamic topological logic ($\mathbf{DTL}$) is a trimodal logic designed for reasoning about dynamic topological systems. It was shown by Fernández-Duque that the natural set of axioms for $\mathbf{DTL}$ is incomplete, but he provided a complete axiomatisation in an extended language. In this paper, we consider dynamic topological logic over scattered spaces, which are topological spaces where every nonempty subspace has an isolated point. 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 trimodal language. In particular, we show that the version of $\mathbf{DTL}$ based on the class of scattered spaces is finitely axiomatisable over the original language, and that the natural axiomatisation is sound and complete. △ Less

Submitted 18 April, 2022; originally announced April 2022.

Fundamental sequences and fast-growing hierarchies for the Bachmann-Howard ordinal

Authors: David Fernández-Duque, Andreas Weiermann

Abstract: We prove that Buchholz's system of fundamental sequences for the $\vartheta$ function enjoys various regularity conditions, including the Bachmann property. We partially extend these results to variants of the $\vartheta$ function, including a version without addition for countable ordinals. We conclude that the Hardy functions based on these notation systems enjoy natural monotonicity properties… ▽ More We prove that Buchholz's system of fundamental sequences for the $\vartheta$ function enjoys various regularity conditions, including the Bachmann property. We partially extend these results to variants of the $\vartheta$ 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 $\vartheta(\varepsilon_{Ω+1})$. △ Less

Submitted 4 January, 2024; v1 submitted 15 March, 2022; originally announced March 2022.

Arithmetical and Hyperarithmetical Worm Battles

Authors: David Fernández-Duque, Joost J. Joosten, Fedor Pakhomov, Konstnatinos Papafilippou, Andreas Weiermann

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

Submitted 29 June, 2022; v1 submitted 14 December, 2021; originally announced December 2021.

Comments: 24 pages. Additions have been made for a proof of the equivalence on the variants corresponding to the fragments of $PA$

Fast Goodstein Walks

Authors: David Fernández-Duque, Andreas Weiermann

Abstract: We define a variant of the Goodstein process based on fast-growing functions and show that it terminates, but this fact is not provable in Kripke-Platek set theory or other theories of strength the Bachmann-Howard ordinal. We moreover show that this Goodstein process is of maximal length, so that any alternative Goodstein process based on the same fast-growing functions will also terminate. We define a variant of the Goodstein process based on fast-growing functions and show that it terminates, but this fact is not provable in Kripke-Platek set theory or other theories of strength the Bachmann-Howard ordinal. We moreover show that this Goodstein process is of maximal length, so that any alternative Goodstein process based on the same fast-growing functions will also terminate. △ Less

Submitted 14 May, 2022; v1 submitted 30 November, 2021; originally announced November 2021.

Taming the `elsewhere': On expressivity of topological languages

Authors: David Fernández-Duque

Abstract: In topological modal logic, it is well known that the Cantor derivative is more expressive than the topological closure, and the `elsewhere,' or `difference,' operator is more expressive than the `somewhere' operator. In 2014, Kudinov and Shehtman asked whether the combination of closure and elsewhere becomes strictly more expressive when adding the Cantor derivative. In this paper we give an affi… ▽ More In topological modal logic, it is well known that the Cantor derivative is more expressive than the topological closure, and the `elsewhere,' or `difference,' operator is more expressive than the `somewhere' operator. In 2014, Kudinov and Shehtman asked whether the combination of closure and elsewhere becomes strictly more expressive when adding the Cantor derivative. In this paper we give an affirmative answer: in fact, the Cantor derivative alone can define properties of topological spaces not expressible with closure and elsewhere. To prove this, we develop a novel theory of morphisms which preserve formulas with the elsewhere operator. △ Less

Submitted 13 September, 2021; originally announced September 2021.

Dynamic Cantor Derivative Logic

Authors: David Fernández-Duque, Yoàv Montacute

Abstract: 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$. W… ▽ More 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. △ Less

Submitted 15 December, 2023; v1 submitted 21 July, 2021; originally announced July 2021.

Comments: Extended version of the paper in Computer Science Logic (CSL) 2022 Proceedings

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (December 18, 2023) lmcs:10042

The Topological Mu-Calculus: completeness and decidability

Authors: Alexandru Baltag, Nick Bezhanishvili, David Fernández-Duque

Abstract: 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 $T_0$ and $T_D$ 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 o… ▽ More 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 $T_0$ and $T_D$ 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 model-theoretic, 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. △ Less

Submitted 17 May, 2021; originally announced May 2021.

Some constructive variants of S4 with the finite model property

Authors: Philippe Balbiani, Martín Diéguez, David Fernández-Duque

Abstract: 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 Godel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that C… ▽ More 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 Godel-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. △ Less

Submitted 30 April, 2021; originally announced April 2021.

The Baire closure and its logic

Authors: Guram Bezhanishvili, David Fernández-Duque

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 ${\bf Baire}(X)$. We identify the modal logic of such algebras to be the well-known system $\sf S5$, and prove soundness and strong completeness for… ▽ More 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 ${\bf Baire}(X)$. We identify the modal logic of such algebras to be the well-known system $\sf 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 $\sf S5$ is the modal logic of a subalgebra of ${\bf Baire}(X)$, and that soundness and strong completeness also holds in the language with the universal modality. △ Less

Submitted 31 December, 2023; v1 submitted 6 February, 2021; originally announced February 2021.

Deducibility and Independence in Beklemishev's Autonomous Provability Calculus

Authors: David Fernández-Duque, Eduardo Hermo Reyes

Abstract: Beklemishev introduced an ordinal notation system for the Feferman-Schütte ordinal $Γ_0$ based on the autonomous expansion of provability algebras. In this paper we present the logic $\textbf{BC}$ (for Bracket Calculus). The language of $\textbf{BC}$ extends said ordinal notation system to a strictly positive modal language. Thus, unlike other provability logics, $\textbf{BC}$ is based on a self-c… ▽ More Beklemishev introduced an ordinal notation system for the Feferman-Schütte ordinal $Γ_0$ based on the autonomous expansion of provability algebras. In this paper we present the logic $\textbf{BC}$ (for Bracket Calculus). The language of $\textbf{BC}$ extends said ordinal notation system to a strictly positive modal language. Thus, unlike other provability logics, $\textbf{BC}$ is based on a self-contained signature that gives rise to an ordinal notation system instead of modalities indexed by some ordinal given a priori. The presented logic is proven to be equivalent to $\textbf{RC}_{Γ_0}$, that is, to the strictly positive fragment of $\textbf{GLP}_{Γ_0}$. We then define a combinatorial statement based on $\textbf{BC}$ and show it to be independent of the theory $\textbf{ATR}_0$ of Arithmetical Transfinite Recursion, a theory of second order arithmetic far more powerful than Peano Arithmetic. △ Less

Submitted 31 August, 2020; originally announced August 2020.

Intermediate Goodstein principles

Authors: David Fernández-Duque, Oriola Gjetaj, Andreas Weiermann

Abstract: The original Goodstein process proceeds by writing natural numbers in nested exponential $k$-normal form, then successively raising the base to $k+1$ and subtracting one from the end result. Such sequences always reach zero, but this fact is unprovable in Peano arithmetic. In this paper we instead consider notations for natural numbers based on the Ackermann function. We define three new Goodstein… ▽ More The original Goodstein process proceeds by writing natural numbers in nested exponential $k$-normal form, then successively raising the base to $k+1$ and subtracting one from the end result. Such sequences always reach zero, but this fact is unprovable in Peano arithmetic. In this paper we instead consider notations for natural numbers based on the Ackermann function. We define three new Goodstein processes, obtaining new independence results for $ {\sf ACA}_0$, ${\sf ACA}_0'$ and ${\sf ACA}_0^+$, theories of second order arithmetic related to the existence of Turing jumps. △ Less

Submitted 12 April, 2022; v1 submitted 20 April, 2020; originally announced April 2020.

A walk with Goodstein

Authors: David Fernández-Duque, Andreas Weiermann

Abstract: Goodstein's principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to grow very quickly, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we explore notions of optimality fo… ▽ More Goodstein's principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to grow very quickly, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we explore notions of optimality for such notation systems and apply them to the classical Goodstein process, to a weaker variant based on multiplication rather than exponentiation, and to a stronger variant based on the Ackermann function. In particular, we introduce the notion of base-change maximality, and show how it leads to far-reaching extensions of Goodstein's result. △ Less

Submitted 8 January, 2024; v1 submitted 20 April, 2020; originally announced April 2020.

Exploring the Jungle of Intuitionistic Temporal Logics

Authors: Joseph Boudou, Martín Diéguez, David Fernández-Duque, Philip Kremer

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 languages with new features via type theory, while from its semantical perspective several logics for reasoning about dynamical systems and… ▽ More 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 languages with new features via type theory, while from its semantical perspective several logics for reasoning about dynamical systems and several semantics for logic programming have their roots in this framework. In this paper 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. Our topological semantics features a new interpretation for the `henceforth' modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show that the seven logics obtained from the axiomatic systems are distinct. △ Less

Submitted 12 March, 2021; v1 submitted 30 December, 2019; originally announced December 2019.

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP). arXiv admin note: text overlap with arXiv:1803.05077

Journal ref: Theory and Practice of Logic Programming 21 (2021) 459-492

Intuitionistic Linear Temporal Logics

Authors: Philippe Balbiani, Joseph Boudou, Martín Diéguez, David Fernández-Duque

Abstract: 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 which we denote $\iltl$, and by imposing additional constraints we obtain the logics $\itlb$ of persistent posets and $\itlht$ of here-and-there temporal logic,… ▽ More 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 which we denote $\iltl$, and by imposing additional constraints we obtain the logics $\itlb$ of persistent posets and $\itlht$ of here-and-there temporal logic, both of which have been considered in the literature. We prove that $\iltl$ has the effective finite model property and hence is decidable, while $\itlb$ 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. △ Less

Submitted 30 December, 2019; originally announced December 2019.

Comments: arXiv admin note: text overlap with arXiv:1704.02847, arXiv:1803.05078

Complete Intuitionistic Temporal Logics in Topological Dynamics

Authors: Joseph Boudou, Martín Diéguez, David Fernández-Duque

Abstract: The language of linear temporal logic can be interpreted over 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. The language of linear temporal logic can be interpreted over 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. △ Less

Submitted 2 October, 2019; originally announced October 2019.

Predicatively unprovable termination of the Ackermannian Goodstein process

Authors: Toshiyasu Arai, David Fernández-Duque, Stanley Wainer, Andreas Weiermann

Abstract: The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means. The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means. △ Less

Submitted 31 May, 2019; originally announced June 2019.

Ekeland's variational principle in weak and strong systems of arithmetic

Authors: David Fernández-Duque, Paul Shafer, Keita Yokoyama

Abstract: We analyze Ekeland's variational principle in the context of reverse mathematics. We find that that the full variational principle is equivalent to $Π^1_1$-${\sf CA}_0$, a strong theory of second-order arithmetic, while natural restrictions (e.g.~to compact spaces or continuous functions) yield statements equivalent to weak König's lemma (${\sf WKL}_0$) and to arithmetical comprehension (… ▽ More We analyze Ekeland's variational principle in the context of reverse mathematics. We find that that the full variational principle is equivalent to $Π^1_1$-${\sf CA}_0$, a strong theory of second-order arithmetic, while natural restrictions (e.g.~to compact spaces or continuous functions) yield statements equivalent to weak König's lemma (${\sf WKL}_0$) and to arithmetical comprehension (${\sf ACA}_0$). We also find that the localized version of Ekeland's variational principle is equivalent to $Π^1_1$-${\sf CA}_0$ even when restricting to continuous functions. This is a rare example of a statement about continuous functions having great logical strength. △ Less

Submitted 15 September, 2020; v1 submitted 11 February, 2019; originally announced February 2019.

Frame-validity games and lower bounds on the complexity of modal axioms

Authors: Philippe Balbiani, David Fernández-Duque, Andreas Herzig, Petar Iliev

Abstract: We introduce frame-equivalence games tailored for reasoning about the size, modal depth, number of occurrences of symbols and number of different propositional variables of modal formulae defining a given frame-property. Using these games, we prove lower bounds on the above measures for a number of well-known modal axioms; what is more, for some of the axioms, we show that they are optimal among t… ▽ More We introduce frame-equivalence games tailored for reasoning about the size, modal depth, number of occurrences of symbols and number of different propositional variables of modal formulae defining a given frame-property. Using these games, we prove lower bounds on the above measures for a number of well-known modal axioms; what is more, for some of the axioms, we show that they are optimal among the formulae defining the respective class of frames. △ Less

Submitted 15 August, 2018; originally announced August 2018.

An intuitionistic axiomatization of `eventually'

Authors: Martín Diéguez, David Fernández-Duque

Abstract: Boudou and the authors have recently introduced the intuitionistic temporal logic $\sf ITL^e$ and shown it to be decidable. In this article we show that the `henceforth'-free fragment of this logic is complete for the class of non-deterministic quasimodels introduced by Fernández-Duque. From this and results of Boudou, Romero and the authors, we conclude that this fragment is also complete for the… ▽ More Boudou and the authors have recently introduced the intuitionistic temporal logic $\sf ITL^e$ and shown it to be decidable. In this article we show that the `henceforth'-free fragment of this logic is complete for the class of non-deterministic quasimodels introduced by Fernández-Duque. From this and results of Boudou, Romero and the authors, we conclude that this fragment is also complete for the standard semantics of $\sf ITL^e$ over the class of expanding posets. △ Less

Submitted 9 April, 2018; originally announced April 2018.

Bisimulations for intuitionistic temporal logics

Authors: Philippe Balbiani, Joseph Boudou, Marín Diéguez, David Fernández-Duque

Abstract: We introduce bisimulations for the logic $ITL^e$ with `next', `until' and `release', an intuitionistic temporal logic based on structures equipped with a partial order used to interpret intuitionistic implication and a monotone function used to interpret the temporal modalities. Our main results are that `eventually', which is definable in terms of `until', cannot be defined in terms of `next' and… ▽ More We introduce bisimulations for the logic $ITL^e$ with `next', `until' and `release', an intuitionistic temporal logic based on structures equipped with a partial order used to interpret intuitionistic implication and a monotone function used to interpret the temporal modalities. Our main results are that `eventually', which is definable in terms of `until', cannot be defined in terms of `next' and `henceforth', and similarly that `henceforth', definable in terms of `release', cannot be defined in terms of `next' and `until', even over the smaller class of here-and-there models. △ Less

Submitted 13 March, 2018; originally announced March 2018.

Axiomatic systems and topological semantics for intuitionistic temporal logic

Authors: Joseph Boudou, Martín Diéguez, David Fernández-Duque, Fabián Romero

Abstract: We propose four 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. Our topological semantics features a new interpretation for the `henceforth' modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show tha… ▽ More We propose four 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. Our topological semantics features a new interpretation for the `henceforth' modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show that the four logics obtained from the axiomatic systems are distinct. Finally, we show that when the language is restricted to the `henceforth'-free fragment, the set of valid formulas for the relational and topological semantics coincide. △ Less

Submitted 13 March, 2018; originally announced March 2018.

Succinctness in subsystems of the spatial mu-calculus

Authors: David Fernández-Duque, Petar Iliev

Abstract: In this paper we systematically explore questions of succinctness in modal logics employed in spatial reasoning. We show that the closure operator, despite being less expressive, is exponentially more succinct than the limit-point operator, and that the $μ$-calculus is exponentially more succinct than the equally-expressive tangled limit operator. These results hold for any class of spaces contain… ▽ More In this paper we systematically explore questions of succinctness in modal logics employed in spatial reasoning. We show that the closure operator, despite being less expressive, is exponentially more succinct than the limit-point operator, and that the $μ$-calculus is exponentially more succinct than the equally-expressive tangled limit operator. These results hold for any class of spaces containing at least one crowded metric space or containing all spaces based on ordinals below $ω^ω$, with the usual limit operator. We also show that these results continue to hold even if we enrich the less succinct language with the universal modality. △ Less

Submitted 12 August, 2017; originally announced August 2017.

A Decidable Intuitionistic Temporal Logic

Authors: Joseph Boudou, Martín Diéguez, David Fernández-Duque

Abstract: We introduce the logic $\sf ITL^e$, an intuitionistic temporal logic based on structures $(W,\preccurlyeq,S)$, where $\preccurlyeq$ is used to interpret intuitionistic implication and $S$ is a $\preccurlyeq$-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for $\sf ITL^e$ are decidable. We prove this by showing that the logic… ▽ More We introduce the logic $\sf ITL^e$, an intuitionistic temporal logic based on structures $(W,\preccurlyeq,S)$, where $\preccurlyeq$ is used to interpret intuitionistic implication and $S$ is a $\preccurlyeq$-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for $\sf 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, $\sf ITL^p$, whose models are similar to Cartesian products. We prove that, unlike $\sf ITL^e$, $\sf ITL^p$ does not have the finite model property. △ Less

Submitted 10 April, 2017; originally announced April 2017.

Exploring the bidimensional space: A dynamic logic point of view

Authors: Philippe Balbiani, David Fernández-Duque, Emiliano Lorini

Abstract: We present a family of logics for reasoning about agents' positions and motion in the plane which have several potential applications in the area of multi-agent systems (MAS), such as multi-agent planning and robotics. The most general logic includes (i) atomic formulas for representing the truth of a given fact or the presence of a given agent at a certain position of the plane, (ii) atomic progr… ▽ More We present a family of logics for reasoning about agents' positions and motion in the plane which have several potential applications in the area of multi-agent systems (MAS), such as multi-agent planning and robotics. The most general logic includes (i) atomic formulas for representing the truth of a given fact or the presence of a given agent at a certain position of the plane, (ii) atomic programs corresponding to the four basic orientations in the plane (up, down, left, right) as well as the four program constructs of propositional dynamic logic (sequential composition, nondeterministic composition, iteration and test). As this logic is not computably enumerable, we study some interesting decidable and axiomatizable fragments of it. We also present a decidable extension of the iteration-free fragment of the logic by special programs representing motion of agents in the plane. △ Less

Submitted 6 February, 2017; originally announced February 2017.

The intuitionistic temporal logic of dynamical systems

Authors: David Fernández-Duque

Abstract: 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 a… ▽ More 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é 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. △ Less

Submitted 19 July, 2018; v1 submitted 21 November, 2016; originally announced November 2016.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 3 (July 20, 2018) lmcs:3280

Non-deterministic Semantics for Dynamic Topological Logic

Authors: David Fernández-Duque

Abstract: Dynamic Topological Logic ($\mathcal{DTL}$) is a combination of $\mathcal{S}${\em 4}, under its topological interpretation, and the temporal logic $\mathcal{LTL}$ interpreted over the natural numbers. $\mathcal{DTL}$ is used to reason about properties of dynamical systems based on topological spaces. Semantics are given by dynamic topological models, which are tuples… ▽ More Dynamic Topological Logic ($\mathcal{DTL}$) is a combination of $\mathcal{S}${\em 4}, under its topological interpretation, and the temporal logic $\mathcal{LTL}$ interpreted over the natural numbers. $\mathcal{DTL}$ 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,\mathcal{T},f,V\right >$, where $\left <X,\mathcal{T}\right >$ is a topological space, $f$ a function on $X$ and $V$ a truth valuation assigning subsets of $X$ to propositional variables. △ Less

Submitted 21 November, 2016; originally announced November 2016.

Worms and Spiders: Reflection calculi and ordinal notation systems

Authors: David Fernández-Duque

Abstract: We give a general overview of ordinal notation systems arising from reflection calculi, and extend the to represent impredicative ordinals up to those representable using Buchholz-style collapsing functions. We give a general overview of ordinal notation systems arising from reflection calculi, and extend the to represent impredicative ordinals up to those representable using Buchholz-style collapsing functions. △ Less

Submitted 3 October, 2017; v1 submitted 28 May, 2016; originally announced May 2016.

Strong Completeness of Provability Logic for Ordinal Spaces

Authors: Juan P. Aguilera, David Fernández-Duque

Abstract: Abashidze and Blass independently proved that the modal logic $\sf{GL}$ is complete for its topological interpretation over any ordinal greater than or equal to $ω^ω$ equipped with the interval topology. Icard later introduced a family of topologies $\mathcal I_λ$ for $λ< ω$, with the purpose of providing semantics for Japaridze's polymodal logic $\sf{GLP}$ $_ω$. Icard's construction was later ext… ▽ More Abashidze and Blass independently proved that the modal logic $\sf{GL}$ is complete for its topological interpretation over any ordinal greater than or equal to $ω^ω$ equipped with the interval topology. Icard later introduced a family of topologies $\mathcal I_λ$ for $λ< ω$, with the purpose of providing semantics for Japaridze's polymodal logic $\sf{GLP}$ $_ω$. Icard's construction was later extended by Joosten and the second author to arbitrary ordinals $λ\geq ω$. We further generalize Icard topologies in this article. Given a scattered space $\mathfrak X = (X, τ)$ and an ordinal $λ$, we define a topology $τ_{+λ}$ in such a way that $τ_{+0}$ is the original topology $τ$ and $τ_{+λ}$ coincides with $\mathcal I_λ$ when $\mathfrak X$ is an ordinal endowed with the left topology. We then prove that, given any scattered space $\mathfrak X$ and any ordinal $λ>0$ such that the rank of $(X, τ)$ is large enough, $\sf{GL}$ is strongly complete for $τ_{+λ}$. One obtains the original Abashidze-Blass theorem as a consequence of the special case where $\mathfrak X=ω^ω$ and $λ=1$. △ Less

Submitted 18 November, 2015; originally announced November 2015.

Comments: 24 pages

The many faces of omega-logic

Authors: David Fernández-Duque

Abstract: We consider several formalizations in the language of second-order arithmetic of "The formula $φ$ is a theorem of $ω$-logic", including some which have been studied in the literature and a new variant defined via a least fixed point. We analyze the provability of relations between these different formalizations in standard theories of reverse mathematics. With this, we study the strength of variou… ▽ More We consider several formalizations in the language of second-order arithmetic of "The formula $φ$ is a theorem of $ω$-logic", including some which have been studied in the literature and a new variant defined via a least fixed point. We analyze the provability of relations between these different formalizations in standard theories of reverse mathematics. With this, we study the strength of various reflection principles arising from these notions of provability, surveying known results and establishing some new equivalences, including a characterization of $Π^1_1$-${\sf CA}_0$ in terms of our fixed-point formalization of $ω$-logic. △ Less

Submitted 22 March, 2022; v1 submitted 15 September, 2015; originally announced September 2015.

Forgetting complex propositions

Authors: David Fernández-Duque, Ángel Nepomuceno-Fernández, Enrique Sarrión-Morrillo, Fernando Soler-Toscano, Fernando R. Velázquez-Quesada

Abstract: This paper uses possible-world semantics to model the changes that may occur in an agent's knowledge as she loses information. This builds on previous work in which the agent may forget the truth-value of an atomic proposition, to a more general case where she may forget the truth-value of a propositional formula. The generalization poses some challenges, since in order to forget whether a complex… ▽ More This paper uses possible-world semantics to model the changes that may occur in an agent's knowledge as she loses information. This builds on previous work in which the agent may forget the truth-value of an atomic proposition, to a more general case where she may forget the truth-value of a propositional formula. The generalization poses some challenges, since in order to forget whether a complex proposition $π$ is the case, the agent must also lose information about the propositional atoms that appear in it, and there is no unambiguous way to go about this. We resolve this situation by considering expressions of the form $[\boldsymbol{\ddagger} π]\varphi$, which quantify over all possible (but minimal) ways of forgetting whether $π$. Propositional atoms are modified non-deterministically, although uniformly, in all possible worlds. We then represent this within action model logic in order to give a sound and complete axiomatization for a logic with knowledge and forgetting. Finally, some variants are discussed, such as when an agent forgets $π$ (rather than forgets whether $π$) and when the modification of atomic facts is done non-uniformly throughout the model. △ Less

Submitted 4 July, 2015; originally announced July 2015.

A case study in almost-perfect security for unconditionally secure communication

Authors: Esteban Landerreche, David Fernández-Duque

Abstract: 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 Cath does not know with certainty who holds each card that is not hers, or perfect security, where Cath learns no… ▽ More 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 Cath does not 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 from Alice and Bob's exchange. 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 a mild variant of the so-called geometric strategy gives $\varepsilon$-strong safety for arbitrarily small $\varepsilon$ and appropriately chosen values of $a,b,c$. △ Less

Submitted 21 June, 2015; v1 submitted 12 June, 2015; originally announced June 2015.

Perfectly secure data aggregation via shifted projections

Authors: David Fernández-Duque

Abstract: We study a general scenario where confidential information is distributed among a group of agents who wish to share it in such a way that the data becomes common knowledge among them but an eavesdropper intercepting their communications would be unable to obtain any of said data. The information is modelled as a deck of cards dealt among the agents, so that after the information is exchanged, all… ▽ More We study a general scenario where confidential information is distributed among a group of agents who wish to share it in such a way that the data becomes common knowledge among them but an eavesdropper intercepting their communications would be unable to obtain any of said data. The information is modelled as a deck of cards dealt among the agents, so that after the information is exchanged, all of the communicating agents must know the entire deal, but the eavesdropper must remain ignorant about who holds each card. Valentin Goranko and the author previously set up this scenario as the secure aggregation of distributed information problem and constructed weakly safe protocols, where given any card $c$, the eavesdropper does not know with certainty which agent holds $c$. Here we present a perfectly safe protocol, which does not alter the eavesdropper's perceived probability that any given agent holds $c$. In our protocol, one of the communicating agents holds a larger portion of the cards than the rest, but we show how for infinitely many values of $a$, the number of cards may be chosen so that each of the $m$ agents holds more than $a$ cards and less than $2m^2a$. △ Less

Submitted 1 July, 2015; v1 submitted 11 May, 2015; originally announced May 2015.

Secure aggregation of distributed information: How a team of agents can safely share secrets in front of a spy

Authors: David Fernández-Duque, Valentin Goranko

Abstract: We consider the generic problem of Secure Aggregation of Distributed Information (SADI), where several agents acting as a team have information distributed among them, modeled by means of a publicly known deck of cards distributed among the agents, so that each of them knows only her cards. The agents have to exchange and aggregate the information about how the cards are distributed among them by… ▽ More We consider the generic problem of Secure Aggregation of Distributed Information (SADI), where several agents acting as a team have information distributed among them, modeled by means of a publicly known deck of cards distributed among the agents, so that each of them knows only her cards. The agents have to exchange and aggregate the information about how the cards are distributed among them by means of public announcements over insecure communication channels, intercepted by an adversary "eavesdropper", in such a way that the adversary does not learn who holds any of the cards. We present a combinatorial construction of protocols that provides a direct solution of a class of SADI problems and develop a technique of iterated reduction of SADI problems to smaller ones which are eventually solvable directly. We show that our methods provide a solution to a large class of SADI problems, including all SADI problems with sufficiently large size and sufficiently balanced card distributions. △ Less

Submitted 28 April, 2015; v1 submitted 28 July, 2014; originally announced July 2014.

Evidence and plausibility in neighborhood structures

Authors: Johan van Benthem, David Fernández-Duque, Eric Pacuit

Abstract: The intuitive notion of evidence has both semantic and syntactic features. In this paper, we develop an {\em evidence logic} for epistemic agents faced with possibly contradictory evidence from different sources. The logic is based on a neighborhood semantics, where a neighborhood $N$ indicates that the agent has reason to believe that the true state of the world lies in $N$. Further notions of re… ▽ More The intuitive notion of evidence has both semantic and syntactic features. In this paper, we develop an {\em evidence logic} for epistemic agents faced with possibly contradictory evidence from different sources. The logic is based on a neighborhood semantics, where a neighborhood $N$ indicates that the agent has reason to believe that the true state of the world lies in $N$. Further notions of relative plausibility between worlds and beliefs based on the latter ordering are then defined in terms of this evidence structure, yielding our intended models for evidence-based beliefs. In addition, we also consider a second more general flavor, where belief and plausibility are modeled using additional primitive relations, and we prove a representation theorem showing that each such general model is a $p$-morphic image of an intended one. This semantics invites a number of natural special cases, depending on how uniform we make the evidence sets, and how coherent their total structure. We give a structural study of the resulting `uniform' and `flat' models. Our main result are sound and complete axiomatizations for the logics of all four major model classes with respect to the modal language of evidence, belief and safe belief. We conclude with an outlook toward logics for the dynamics of changing evidence, and the resulting language extensions and connections with logics of plausibility change. △ Less

Submitted 4 July, 2013; originally announced July 2013.

The omega-rule interpretation of transfinite provability logic

Authors: David Fernández-Duque, Joost J. Joosten

Abstract: In this paper we consider transfinite provability logics where for each ordinal in some recursive well-order we have a corresponding modal provability operator. The modality [xi] will be interpreted as "provable in ACA_0 together with at most xi nested applications of the omega rule". We show how to formalize this in in second order number theory. Next we prove both soundness and completeness unde… ▽ More In this paper we consider transfinite provability logics where for each ordinal in some recursive well-order we have a corresponding modal provability operator. The modality [xi] will be interpreted as "provable in ACA_0 together with at most xi nested applications of the omega rule". We show how to formalize this in in second order number theory. Next we prove both soundness and completeness under this interpretation. We conclude by showing how one can lower the base theory ACA_0 to theories below RCA_0. △ Less

Submitted 21 February, 2013; originally announced February 2013.

MSC Class: 03F45; 03F15

A geometric protocol for cryptography with cards

Authors: Andrés Cordón-Franco, Hans van Ditmarsch, David Fernández-Duque, Fernando Soler-Toscano

Abstract: In the generalized Russian cards problem, the three players Alice, Bob and Cath draw a,b and c cards, respectively, from a deck of a+b+c cards. Players only know their own cards and what the deck of cards is. Alice and Bob are then required to communicate their hand of cards to each other by way of public messages. The communication is said to be safe if Cath does not learn the ownership of any sp… ▽ More In the generalized Russian cards problem, the three players Alice, Bob and Cath draw a,b and c cards, respectively, from a deck of a+b+c cards. Players only know their own cards and what the deck of cards is. Alice and Bob are then required to communicate their hand of cards to each other by way of public messages. The communication is said to be safe if Cath does not learn the ownership of any specific card; in this paper we consider a strengthened notion of safety introduced by Swanson and Stinson which we call k-safety. An elegant solution by Atkinson views the cards as points in a finite projective plane. We propose a general solution in the spirit of Atkinson's, although based on finite vector spaces rather than projective planes, and call it the `geometric protocol'. Given arbitrary c,k>0, this protocol gives an informative and k-safe solution to the generalized Russian cards problem for infinitely many values of (a,b,c) with b=O(ac). This improves on the collection of parameters for which solutions are known. In particular, it is the first solution which guarantees $k$-safety when Cath has more than one card. △ Less

Submitted 24 January, 2013; v1 submitted 17 January, 2013; originally announced January 2013.

Well-orders in the transfinite Japaridze algebra

Authors: David Fernández-Duque, Joost J. Joosten

Abstract: This paper studies the transfinite propositional provability logics $\glp_Λ$ and their corresponding algebras. These logics have for each ordinal $ξ< Λ$ a modality $\la α\ra$. We will focus on the closed fragment of $\glp_Λ$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la ξ_n\ra \ldots \la ξ_1 \ra \top$. Beklemish… ▽ More This paper studies the transfinite propositional provability logics $\glp_Λ$ and their corresponding algebras. These logics have for each ordinal $ξ< Λ$ a modality $\la α\ra$. We will focus on the closed fragment of $\glp_Λ$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la ξ_n\ra \ldots \la ξ_1 \ra \top$. Beklemishev has defined well-orderings $<_ξ$ on worms whose modalities are all at least $ξ$ and presented a calculus to compute the respective order-types. In the current paper we present a generalization of the original $<_ξ$ orderings and provide a calculus for the corresponding generalized order-types $o_ξ$. Our calculus is based on so-called {\em hyperations} which are transfinite iterations of normal functions. Finally, we give two different characterizations of those sequences of ordinals which are of the form $\la {\formerOmega}_ξ(A) \ra_{ξ\in \ord}$ for some worm $A$. One of these characterizations is in terms of a second kind of transfinite iteration called {\em cohyperation.} △ Less

Submitted 17 January, 2014; v1 submitted 14 December, 2012; originally announced December 2012.

Comments: Corrected a minor but confusing omission in the relation between Veblen progressions and hyperations

On provability logics with linearly ordered modalities

Authors: Lev D. Beklemishev, David Fernández-Duque, Joost J. Joosten

Abstract: We introduce the logics GLP(Λ), a generalization of Japaridze's polymodal provability logic GLP(ω) where Λis any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP(ω) yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP(Λ) and the decidability o… ▽ More We introduce the logics GLP(Λ), a generalization of Japaridze's polymodal provability logic GLP(ω) where Λis any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP(ω) yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP(Λ) and the decidability of GLP(Λ) for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment of GLP(Λ). △ Less

Submitted 17 October, 2012; originally announced October 2012.

The polytopologies of transfinite provability logic

Authors: David Fernández-Duque

Abstract: Provability logics are modal or polymodal systems designed for modeling the behavior of Gödel's provability predicate in arithmetical theories and its natural extensions. If Λis any ordinal, the Gödel-Löb calculus GLP(Λ) contains one modality [λ] for each λ<Λ, representing provability predicates of increasing strength. GLP(Λ) has no Kripke models, but Beklemishev and Gabelaia recently proved that… ▽ More Provability logics are modal or polymodal systems designed for modeling the behavior of Gödel's provability predicate in arithmetical theories and its natural extensions. If Λis any ordinal, the Gödel-Löb calculus GLP(Λ) contains one modality [λ] for each λ<Λ, representing provability predicates of increasing strength. GLP(Λ) has no Kripke models, but Beklemishev and Gabelaia recently proved that GLP(ω) is complete for its class of topological models. In this paper we generalize Beklemishev and Gabelaia's result to GLP(Λ) for arbitrary Λ. We also introduce provability ambiances, which are topological models where valuations of formulas are restricted. With this we show completeness of GLP(Λ) for the class of provability ambiances based on Icard polytopologies. △ Less

Submitted 4 July, 2013; v1 submitted 27 July, 2012; originally announced July 2012.

A colouring protocol for the generalized Russian cards problem

Authors: Andrés Cordón-Franco, Hans van Ditmarsch, David Fernández-Duque, Fernando Soler-Toscano

Abstract: In the generalized Russian cards problem, Alice, Bob and Cath draw $a$, $b$ and $c$ cards, respectively, from a deck of size $a+b+c$. Alice and Bob must then communicate their entire hand to each other, without Cath learning the owner of a single card she does not hold. Unlike many traditional problems in cryptography, however, they are not allowed to encode or hide the messages they exchange from… ▽ More In the generalized Russian cards problem, Alice, Bob and Cath draw $a$, $b$ and $c$ cards, respectively, from a deck of size $a+b+c$. Alice and Bob must then communicate their entire hand to each other, without Cath learning the owner of a single card she does not hold. Unlike many traditional problems in cryptography, however, they are not allowed to encode or hide the messages they exchange from Cath. The problem is then to find methods through which they can achieve this. We propose a general four-step solution based on finite vector spaces, and call it the "colouring protocol", as it involves colourings of lines. Our main results show that the colouring protocol may be used to solve the generalized Russian cards problem in cases where $a$ is a power of a prime, $c=O(a^2)$ and $b=O(c^2)$. This improves substantially on the set of parameters for which solutions are known to exist; in particular, it had not been shown previously that the problem could be solved in cases where the eavesdropper has more cards than one of the communicating players. △ Less

Submitted 26 March, 2014; v1 submitted 22 July, 2012; originally announced July 2012.

Journal ref: Andrés Cordón-Franco, Hans P. van Ditmarsch, David Fernández-Duque, Fernando Soler-Toscano: A colouring protocol for the generalized Russian cards problem. Theoretical Computer Science 495: 81-95 (2013)

Non-finite axiomatizability of Dynamic Topological Logic

Authors: David Fernández-Duque

Abstract: 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… ▽ More 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 $\mathsf{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. △ Less

Submitted 21 July, 2012; originally announced July 2012.

Comments: arXiv admin note: text overlap with arXiv:1201.5162 by other authors

Hyperations, Veblen progressions and transfinite iterations of ordinal functions

Authors: David Fernández-Duque, Joost J. Joosten

Abstract: In this paper we introduce hyperations and cohyperations, which are forms of transfinite iteration of ordinal functions. Hyperations are iterations of normal functions. Unlike iteration by pointwise convergence, hyperation preserves normality. The hyperation of a normal function f is a sequence of normal functions so that f^0= id, f^1 = f and for all ordinals α, βwe have that f^(α+ β) = f^αf^β.… ▽ More In this paper we introduce hyperations and cohyperations, which are forms of transfinite iteration of ordinal functions. Hyperations are iterations of normal functions. Unlike iteration by pointwise convergence, hyperation preserves normality. The hyperation of a normal function f is a sequence of normal functions so that f^0= id, f^1 = f and for all ordinals α, βwe have that f^(α+ β) = f^αf^β. These conditions do not determine f^αuniquely; in addition, we require that the functions be minimal in an appropriate sense. We study hyperations systematically and show that they are a natural refinement of Veblen progressions. Next, we define cohyperations, very similar to hyperations except that they are left-additive: given α, β, f^(α+ β)= f^βf^α. Cohyperations iterate initial functions which are functions that map initial segments to initial segments. We systematically study cohyperations and see how they can be employed to define left inverses to hyperations. Hyperations provide an alternative presentation of Veblen progressions and can be useful where a more fine-grained analysis of such sequences is called for. They are very amenable to algebraic manipulation and hence are convenient to work with. Cohyperations, meanwhile, give a novel way to describe slowly increasing functions as often appear, for example, in proof theory. △ Less

Submitted 9 May, 2012; originally announced May 2012.