4 citations · 10 across the 10 of their papers we have counts for
13 papers
Fast Goodstein Walks
David Fernández-Duque, Andreas Weiermann
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 theorie…
Taming the `elsewhere': On expressivity of topological languages
David Fernández-Duque
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 expr…
Dynamic Cantor Derivative Logic
David Fernández-Duque, Yoàv Montacute
Topological semantics for modal logic based on the Cantor derivative operator gives rise to derivative logics, also referred to as -logics. Unlike logics based on the topologica…
The Topological Mu-Calculus: completeness and decidability
Alexandru Baltag, Nick Bezhanishvili, David Fernández-Duque
We study the topological -calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability and FMP over general topological spaces, as well a…
Some constructive variants of S4 with the finite model property
Philippe Balbiani, Martín Diéguez, David Fernández-Duque
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…
The Baire closure and its logic
Guram Bezhanishvili, David Fernández-Duque
The Baire algebra of a topological space is the quotient of the algebra of all subsets of modulo the meager sets. We show that this Boolean algebra can be endowed with a na…
Deducibility and Independence in Beklemishev's Autonomous Provability Calculus
David Fernández-Duque, Eduardo Hermo Reyes
Beklemishev introduced an ordinal notation system for the Feferman-Schütte ordinal based on the autonomous expansion of provability algebras. In this paper we present the log…
A walk with Goodstein
David Fernández-Duque, Andreas Weiermann
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 a…
Intuitionistic Linear Temporal Logics
Philippe Balbiani, Joseph Boudou, Martín Diéguez +1
We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transiti…
Exploring the Jungle of Intuitionistic Temporal Logics
Joseph Boudou, Martín Diéguez, David Fernández-Duque +1
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…
Predicatively unprovable termination of the Ackermannian Goodstein process
Toshiyasu Arai, David Fernández-Duque, Stanley Wainer +1
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 v…
Ekeland's variational principle in weak and strong systems of arithmetic
David Fernández-Duque, Paul Shafer, Keita Yokoyama
We analyze Ekeland's variational principle in the context of reverse mathematics. We find that that the full variational principle is equivalent to -, a strong t…
Well-orders in the transfinite Japaridze algebra II: Turing progressions and their well-orders
David Fernández-Duque, Joost J. Joosten
We study transfinite extensions of Japaridze's provability logic GLP and the well-founded relations that naturally occur within them. Every ordinal induces a partial order over the…