7 papers
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…
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…
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…
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…
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…