Searcharxiv⌕ Search

arXiv subjects

Joost J. Joosten

Publications and source records attributed to Joost J. Joosten.

At least 19 recordsLinked to original sources
arXiv2026

The Complexity of the Constructive Master Modality

We introduce the semantically-defined constructive master-modality logics $\sf CK^*$ and $\sf WK^*$, extending the basic constructive modal logic $\sf CK$ and the Wijesekera-style logic $\sf WK$ obtained by impossing infallibility. Using translations between our logics and fragments of $\sf PDL$, we show that both $\sf CK^*$ and $\sf WK^*$ are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celoni, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed $\sf CS4$ and $\sf WS4$ into the master-modality logics, showing that their validity problems are in EXPTIME.

cs.LO↗
arXiv2026

Ultrafilter Extensions for Veltman Semantics

In this paper, we present a first-order frame condition for interpretability logic and show that the condition is not modally definable. Yet, the frame condition holds both on ILM and on ILP frames and, hence, is of potential importance for the long-standing open problem about the interpretability logic of all reasonable arithmetical theories. In the light of the Goldblatt-Thomason Theorem, the modally inexpressible frame condition serves as motivation to develop ultrafilter extensions for interpretability logic. We develop the necessary algebraic tools to define these ultrafilter extensions and prove the main properties about both the tools and the ultrafilter extensions.

math.LO↗
arXiv2026

Completeness and Incompleteness for Expanding Gödel-Löb Logics

Expanding products of modal logics are bimodal logics obtained from the combination of a `horizontal component' logic and a `vertical component' logic, lying between the fusion and the Cartesian product of the two logics. Gabelaia et al. showed that expanding products are often decidable when the first component is Noetherian, although their methods are semantical and do not yield complete axiomatisations. They do, however, propose a candidate, dubbed the expanding commutator of the two logics and known to be complete in many `non-Noetherian' cases. In this paper, we consider various expanding products of modal logics whose vertical component is $\sf GL$. We show that the standard axiomatisation is complete when the horizontal component is either $ {\sf K4}$ or $ {\sf GL} $, but incomplete when it is ${\sf Grz}$ or any logic between ${\sf K4.3}$ and ${\sf Grz.3}$, thus yielding a partial solution to a question posed by Gabelaia et al. more than two decades ago.

math.LO↗
arXiv2026

Coherency through formalisations of Structured Natural Language, A case study on FRETish

Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.

cs.CL↗
arXiv2025

On the Contingency of Logic in Possible World Semantics

This paper investigates the contingency of logic within the framework of possible world semantics. Possible world semantics captures the meaning of necessitation, i.e., a statement is necessarily true if it holds in all possible worlds. Standard Kripkean semantics assumes that all possible worlds are governed by one single logic. We relax this assumption and introduce mixed models, in which different worlds may obey different logical systems. The paper provides a first case study where we mix classical propositional logic ($\mathsf{CPC}$) and intuitionistic propositional logic ($\mathsf{IPC}$) in the possible world semantics. We define the class of mixed models $\mathcal{M}\mathcal{M}(\mathsf{CPC}, \mathsf{IPC})$, together with a subclass of concrete mixed models ($\mathcal{CMM}$), and establish their semantic properties. Our main result shows that the set of formulas valid in $\mathcal{M}\mathcal{M}(\mathsf{CPC}, \mathsf{IPC})$ corresponds exactly to the intuitionistic modal logic $\mathsf{iK}$ extended with the Box Excluded Middle axiom ($\mathsf{iK} + \mathsf{bem}$). To demonstrate this, we prove soundness and completeness results linking $\mathcal{M}\mathcal{M}(\mathsf{CPC}, \mathsf{IPC})$ and $\mathcal{CMM}$, and birelational models for $\mathsf{iK} + \mathsf{bem}$.

math.LO↗
arXiv2025

Tree Rewriting Calculi for Strictly Positive Logics

We study strictly positive logics in the language $\mathscr{L}^+$, which constructs formulas from $\top$, propositional variables, conjunction, and diamond modalities. We begin with the base system $\bf K^+$, the strictly positive fragment of polymodal $\bf K$, and examine its extensions obtained by adding axioms such as monotonicity, transitivity, and the hierarchy-sensitive interaction axiom $(\sf J)$, which governs the interplay between modalities of different strengths. The strongest of these systems is the Reflection Calculus ($\bf RC$), which corresponds to the strictly positive fragment of polymodal $\bf GLP$. Our main contribution is a formulation of these logics as tree rewriting systems, establishing both adequacy and completeness through a correspondence between $\mathscr{L}^+$ formulas and inductively defined modal trees. We also provide a normalization of the rewriting process, which has exponential complexity when axiom $(\sf J)$ is absent; otherwise we provide a double-exponential bound. By introducing tree rewriting calculi as practical provability tools for strictly positive logics, we aim to deepen their proof-theoretic analysis and computational applications.

cs.LO↗
arXiv2025

Specification languages for computational laws versus basic legal principles

We speak of a \textit{computational law} when that law is intended to be enforced by software through an automated decision-making process. As digital technologies evolve to offer more solutions for public administrations, we see an ever-increasing number of computational laws. Traditionally, law is written in natural language. Computational laws, however, suffer various complications when written in natural language, such as underspecification and ambiguity which lead to a diversity of possible interpretations to be made by the coder. These could potentially result into an uneven application of the law. Thus, resorting to formal languages to write computational laws is tempting. However, writing laws in a formal language leads to further complications, for example, incomprehensibility for non-experts, lack of explicit motivation of the decisions made, or difficulties in retrieving the data leading to the outcome. In this paper, we investigate how certain legal principles fare in both scenarios: computational law written in natural language or written in formal language. We use a running example from the European Union's road transport regulation to showcase the tensions arising, and the benefits from each language.

cs.CY↗
arXiv2024

A tree rewriting system for the Reflection Calculus

The $Reflection$ $Calculus$ ($\mathcal{\mathbf{RC}}$) is the fragment of the polymodal logic $\mathcal{\mathbf{GLP}}$ in the language $L^+$ whose formulas are built up from $\top$ and propositional variables using conjunction and diamond modalities. $\mathcal{\mathbf{RC}}$ is complete with respect to the arithmetical interpretation that associates modalities with reflection principles and has various applications in proof theory, specifically ordinal analysis. We present ${\sf TRC}$, a tree rewriting system that is adequate and complete with respect to $\mathcal{\mathbf{RC}}$, designed to simulate $\mathcal{\mathbf{RC}}$ derivations. ${\sf TRC}$ is based on a given correspondence between formulas of $L^{+}$ and modal trees ${\sf Tree}^{\Diamond}$. Modal trees are presented as an inductive type allowing precise positioning and transformations which give rise to the formal definition of rewriting rules and facilitates formalization in proof assistants. Furthermore, we provide a rewrite normalization theorem for systematic rule application. The normalization of the rewriting process enhances proof search efficiency and facilitates implementation. By providing ${\sf TRC}$ as an efficient provability tool for $\mathcal{\mathbf{RC}}$, we aim to help on the study of various aspects of the logic such as the subformula property and rule admissibility.

math.LO↗
arXiv2024

Feferman Interpretability

We introduce a modal logic FIL for Feferman interpretability. In this logic both the provability modality and the interpretability modality can come with a label. This label indicates that in the arithmetical interpretation the axiom set of the underlying base theory is tweaked so as to mimic behaviour of finitely axiomatised theories. The theory with the tweaked axiom set will be extensionally the same as the original theory though this equality will in general not be provable. After providing the logic FIL and proving the arithmetical soundness, we set the logic to work to prove various interpretability principles to be sound in a large variety of (weak) arithmetical theories. In particular, we prove the two series of principles from [GJ20] to be arithmetically sound using FIL. Up to date, the arithmetical soundness of these series had only been proven using the techniques of definable cuts.

math.LO↗
arXiv2024

Le Nozze di Giustizia. Interactions between Artificial Intelligence, Law, Logic, Language and Computation with some case studies in Traffic Regulations and Health Care

An important aim of this paper is to convey some basics of mathematical logic to the legal community working with Artificial Intelligence. After analysing what AI is, we decide to delimit ourselves to rule-based AI leaving Neural Networks and Machine Learning aside. Rule based AI allows for Formal methods which are described in a rudimentary form. We will then see how mathematical logic interacts with legal rule-based AI practice. We shall see how mathematical logic imposes limitations and complications to AI applications. We classify the limitations and interactions between mathematical logic and legal AI in three categories: logical, computational and mathematical. The examples to showcase the interactions will largely come from European traffic regulations. The paper closes off with some reflections on how and where AI could be used and on basic mechanisms that shape society.

cs.AI↗
arXiv2023

Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

We determine the strictly positive fragment $\mathsf{QPL}^+(\mathsf{HA})$ of the quantified provability logic $\mathsf{QPL}(\mathsf{HA})$ of Heyting Arithmetic. We show that $\mathsf{QPL}^+(\mathsf{HA})$ is decidable and that it coincides with $\mathsf{QPL}^+(\mathsf{PA})$, which is the strictly positive fragment of the quantified provability logic of of Peano Arithmetic. This positively resolves a previous conjecture of the authors. On our way to proving these results, we carve out the strictly positive fragment $\mathsf{PL}^+(\mathsf{HA})$ of the provability logic $\mathsf{PL}(\mathsf{HA})$ of Heyting Arithmetic, provide a simple axiomatization, and prove it to be sound and complete for two types of arithmetical interpretations. The simple fragments presented in this paper should be contrasted with a 2022 result by Mojtahedi, where an axiomatization for $\mathsf{PL}(\mathsf{HA})$ is provided. This axiomatization, although decidable, is of considerable complexity.

math.LO↗
arXiv2023

UTC Time, Formally Verified

FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet non-trivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some general-purpose solutions that were produced as by-products and may be used in other verification projects. These include a refinement package between proof-oriented MathComp numbers and computation-oriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through brute-force computation.

cs.SE↗
arXiv2023

Dialogues with algorithms

In this short paper we focus on human in the loop for rule-based software used for law enforcement. For example, one can think of software that computes fines like tachograph software, software that prepares evidence like DNA sequencing software or social profiling software to patrol in high-risk zones, among others. An important difference between a legal human agent and a software application lies in possible dialogues. A human agent can be interrogated to motivate her decisions. Often such dialogues with software are at the best extremely hard but mostly impossible. We observe that the absence of a dialogue can sincerely violate civil rights and legal principles like, for example, Transparency or Contestability. Thus, possible dialogues with legal algorithms are at the least highly desirable. Futuristic as this may sound, we observe that in various realms of formal methods, such dialogues are easily obtainable. However, this triggers the usual tension between the expressibility of the dialogue language and the feasibility of the corresponding computations.

cs.CY↗
arXiv2022

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.

math.LO↗
arXiv2022

Assuring and critical labels for relations between maximal consistent sets for interpretability logics

The notion of a critical successor [dJV90] has been central to almost all modal completeness proofs in interpretability logics. In this paper we shall work with an alternative notion, that of an assuring successor. As we shall see, this will enable more concisely formulated completeness proofs, both with respect to ordinary and generalised Veltman semantics. Due to their interesting theoretical properties, we will devote some space to the study of a particular kind of assuring labels, the so-called full labels and maximal labels.. After a general treatment of assuringness, we shall apply it to obtain certain completeness results. Namely, we give another proof of completeness of ILW w.r.t. ordinary semantics and of ILP w.r.t. generalised semantics.

math.LO↗
arXiv2021

An Escape from Vardanyan's Theorem

Vardanyan's Theorems state that $\mathsf{QPL}(\mathsf{PA})$ - the quantified provability logic of Peano Arithmetic - is $Π^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf{QRC}_1$ was previously introduced by the authors as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf{QRC}_1$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf{QRC}_1$ is the strictly positive fragment of $\mathsf{QGL}$ and a fragment of $\mathsf{QPL}(\mathsf{PA})$.

math.LO↗