arXiv subjects

Sofía Santiago-Fernández

Publications and source records attributed to Sofía Santiago-Fernández.

4 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

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↗

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↗

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↗