Publications
My publications are also available on my Google Scholar profile.
Conference Papers
Proof Theory for Non-Contingency Logic
Abstract: Non-contingency logic (NCL) replaces the usual necessity operator of modal logic with an operator expressing that a proposition is necessarily true or necessarily false. Besides its intrinsic logical interest, NCL admits natural interpretations as knowing whether in epistemic logic and as decidability under the arithmetical interpretation of provability logic. Although the semantics of non-contingency logic have been extensively studied, its proof theory remains comparatively underdeveloped. In this paper, we develop a uniform proof-theoretic framework for NCL over a broad class of frame conditions. Our approach is based on generalized path conditions (GPCs), a grammar-theoretic formalism that uniformly captures many standard modal frame properties. For every finite set G of GPCs, we construct a corresponding labelled sequent calculus. All calculi share a common set of logical rules and differ only by a single structural rule generated from G, which captures the underlying frame conditions. We prove that these calculi are sound and complete with respect to their corresponding frame classes, thereby providing a uniform proof theory for a large family of non-contingency logics.
Joint paper with Yunsong Wang and Borja Sierra Miranda
Submitted to: National Conference on Modern Logic 2026
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Abstract: We introduce and investigate non-wellfounded and cyclic linear nested sequent calculi, and, as a case study, develop such systems for linear temporal logic (LTL). The paper addresses two central problems, which we call cycle recognition and unraveling. Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call saturation recurrence, which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.
Joint paper with Tim S. Lyon
Accepted at: Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification, 2026
A Sound and Complete Axiomatization of Intuitionistic Temporal Logic
Abstract: Intuitionistic linear temporal logic (iLTL) has been studied since at least the 1990s, with renewed interest in the last decade. It enjoys natural semantics over intuitionistic Kripke frames equipped with an order-preserving function representing the temporal dynamics, known as expanding models. This leads to a logic that is known to be decidable but whose axiomatisation has long remained open. We propose an extension of iLTL with the co-implication connective of Heyting–Brouwer logic and call it bi-intuitionistic linear temporal logic (biLTL). We establish that this extension is still decidable for the class of expanding models. We moreover give a sound and complete Hilbert-style calculus for it, the first for any logic extending iLTL. As a corollary, the topological semantics for intuitionistic propositional logic cannot be extended to a topological semantics for Heyting–Brouwer logic, which thus establishes co-implication as a distinctive feature of the Kripke semantics for bi-intuitionistic logic.
Joint paper with David Fernández-Duque and Brett McLean
International Conference on Principles of Knowledge Representation and Reasoning, 2024
Co-Algebraic Proof Translations for Non-Wellfounded Proofs
Abstract: Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz. In this paper, we provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instance of our method, we establish cut-elimination for a non-wellfounded system of the logic Grz. Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.
Joint paper with Borja Sierra-Miranda and Thomas Studer
Advances in Modal Logic, 2024
Intuitionistic Master Modality
Abstract: We present a cyclic sequent calculus for intuitionistic modal logic with the master modality. Formulas of the logic are evaluated over bi-relational Kripke models with three different frame conditions: functional frames, triangle confluent frames, and arbitrary frames. It is shown that the calculus is sound and complete for all three classes of models. This, in particular, proves that intuitionistic modal logic with the master modality cannot distinguish between arbitrary models and functional models. Soundness is established by a standard argument while completeness is proven via a detour to non-wellfounded proofs, using a proof-search argument that draws on analyticity of the calculus. The framework is robust in the sense that it can be naturally adapted to account for various frame conditions, such as serial models, reflexive models or S4 models, as well as for a polymodal extension that can be interpreted as intuitionistic common knowledge.
Joint paper with Lide Grotenhuis, Bahareh Afshari and Graham E. Leigh
Advances in Modal Logic, 2024
Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic
Abstract: We introduce ill-founded sequent calculi for two intuitionistic linear-time temporal logics. Both logics are based on the language of intuitionistic propositional logic with next and until operators and are evaluated on dynamic Kripke models wherein the intuitionistic and temporal accessibility relations are assumed to satisfy one of two natural confluence properties: forward confluence in one case, and both forward and backward confluence in the other. The presented sequent calculi are cut-free and incorporate a simple form of formula nesting. Soundness of the calculi is shown by a standard argument and completeness via proof search.
Joint paper with Lide Grotenhuis, Bahareh Afshari and Graham E. Leigh
Automated Reasoning with Analytic Tableaux and Related Methods, 2023
A Family of Decidable Bi-Intuitionistic Modal Logics
Abstract: We investigate intuitionistic logics extended with both the co-implication connective of Hilbert–Brouwer logic and with diamond and box modalities. We use a Kripke semantics based on frames with two forth confluence conditions on the modal relation with respect to the intuitionistic relation. We give sound and strongly complete axiomatisations for entailment on this class of frames, and give similar axiomatisations for the subclasses of frames satisfying any combination of reflexivity, transitivity, and seriality. We then prove that all of these logics are decidable, by proving that they have the finite frame property.
Joint paper with David Fernández-Duque and Brett McLean
International Conference on Principles of Knowledge Representation and Reasoning, 2023
An Analytic Proof System for Common Knowledge Logic over S5
Abstract: In this paper we present an analytic proof system for multi-modal logic with common knowledge over S5 (called S5-CKL). The system is an annotated cyclic calculus manipulating two-sided Gentzen sequents and extending a known system for multi-modal S5. First a direct argument is used to show that the system is sound. Using a canonical model construction, we then show that the system is analytically complete. In particular, the use of the cut-rule is restricted to analytic cuts. Exploiting this analyticity, we then reduce the provability problem of a given sequent to the problem of solving a certain parity game. As a consequence we obtain an optimal decision procedure for proof search and thereby for the validity problem of S5-CKL.
Joint paper with Jan Rooduijn
Advances in Modal Logic, 2022
ArXiv Pre-Prints
Intuitionistic Common Knowledge
Abstract: We study an intuitionistic version of common knowledge logic (CK), called ICK, introduced by Jäger and Marti. ICK extends intuitionistic propositional logic by multiple box modalities interpreted as knowledge operators for various agents and a common knowledge operator. Formulae are interpreted over birelational Kripke models satisfying a simple interaction principle between the intuitionistic order and the modal accessibility relations. Furthermore, we consider the restriction to reflexive, S4 and S5 models. We present axiomatizations as well as analytic cyclic sequent calculi for all considered logics and prove them to be sound and complete. Furthermore, we establish the finite model property and decidability, show that proof-search in the cyclic calculi can be automated, provide a translation of CK over S5 into ICK over S5 and establish that the proof-search and validity problems of all considered logics can be solved in exponential time.
ArXiv pre-print, 2026
PhD Thesis
Intuitionistic Dynamic Logic
Abstract: This thesis develops the mathematical theory of intuitionistic dynamic logics - extensions of intuitionistic propositional logic with modalities and fixed point operators. Such systems provide formal tools for reasoning about change, such as encountered in mathematical systems evolving over time or in the knowledge state of an agent after an information update. We investigate five intuitionistic dynamic logics: intuitionistic master modality, intuitionistic common knowledge logic, intuitionistic linear temporal logic, bi-intuitionistic modal logic and bi-intuitionistic linear temporal logic. On the proof theoretic side we develop sound and complete Hilbert-style axiomatizations as well as non-wellfounded and cyclic sequent calculi. On the semantic side we study these logics over various classes of dynamic models, which are birelational Kripke models satisfying confluence and frame conditions. We establish expressivity results, the finite model property, decidability, as well as complexity bounds. The main contributions are threefold. First, we develop analytic cyclic sequent calculi for intuitionistic master modality and common knowledge logic, where completeness is obtained by a robust proof search argument. Second, we obtain the finite model property and decidability for bi-intuitionistic modal logic via an intricate combinatorial analysis of dynamic models. Third, we develop a sound and complete axiomatization for intuitionistic linear temporal logic featuring the temporal operators next, eventually and henceforth, thereby providing a positive answer to the long-standing open question concerning the existence of a finite axiomatization.
PhD Thesis
Department of Mathematics, Ghent University, 2025
Supervisors: Thomas Studer, David Fernández-Duque, Andreas Weiermann