BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

David Fernández-Duque

David Fernández-Duque appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
math.LOLogic in Computer ScienceCryptography and SecurityArtificial IntelligenceInformation Theorymath.ITSymbolic Computation

Catalog footprint

What is connected

28works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

28 published item(s)

preprint2025arXiv

The fractal Goodstein principle

The original Goodstein process is based on writing numbers in hereditary $b$-exponential normal form: that is, each number $n$ is written in some base $b\geq 2$ as $n=b^ea+r$, with $e$ and $r$ iteratively being written in hereditary $b$-exponential normal form. We define a new process which generalises the original by writing expressions in terms of a hierarchy of bases $B$, instead of a single base $b$. In particular, the `digit' $a$ may itself be written with respect to a smaller base $b'$. We show that this new process always terminates, but termination is independent of Kripke-Platek set theory, or other theories of Bachmann-Howard strength.

0 citations0 reviewsNo code linkedOpen access
preprint2024arXiv

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

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})$.

0 citations0 reviewsNo code linkedOpen access
preprint2023arXiv

The Baire closure and its logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Arithmetical and Hyperarithmetical Worm Battles

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Intermediate Goodstein principles

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

The many faces of omega-logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Untangled: A Complete Dynamic Topological Logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Deducibility and Independence in Beklemishev's Autonomous Provability Calculus

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Intuitionistic Linear Temporal Logics

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Non-deterministic Semantics for Dynamic Topological Logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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

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$.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Forgetting complex propositions

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} π]φ$, 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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Perfectly secure data aggregation via shifted projections

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$.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Strong Completeness of Provability Logic for Ordinal Spaces

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$.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

A colouring protocol for the generalized Russian cards problem

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Well-orders in the transfinite Japaridze algebra

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.}

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

A geometric protocol for cryptography with cards

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Evidence and plausibility in neighborhood structures

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

The omega-rule interpretation of transfinite provability logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

The polytopologies of transfinite provability logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Well-orders in the transfinite Japaridze algebra II: Turing progressions and their well-orders

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 class of "words," which are iterated consistency statements expressible within GLP. Well-ordered restrictions of these partial orders have been studied previously; in this paper we consider the unrestricted partial orders, which are no longer linear but remain well-founded. These unrestricted partial orders bear important repercussions on modal semantics for GLP and on Turing progressions.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Hyperations, Veblen progressions and transfinite iterations of ordinal functions

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Models of transfinite provability logic

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. Later, Icard defined a topological model for the same fragment 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 I(Θ,Λ) and a topological model T(Θ,Λ), and show that the closed fragment of GLP(Λ) is sound for both of these structures, as well as complete, provided Θis large enough.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Non-finite axiomatizability of Dynamic Topological Logic

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

On provability logics with linearly ordered modalities

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(Λ).

0 citations0 reviewsNo code linkedOpen access