arXiv subjects

Leonardo Pacheco

Publications and source records attributed to Leonardo Pacheco.

7 recordsLinked to original sources

arXiv2026

Modalities in non-classical variations of $\mathsf{S4}$

A classical result in modal logic states that $\mathsf{S4}$ has $14$ modalities, that is, every sequence of negations, boxes, and diamonds is equivalent to one in a set of $14$ such sequences. We study analogous results for the non-classical analogues $\mathsf{CS4}$, $\mathsf{IS4}$, $\mathsf{GS4}$, and $\mathsf{GS4^c}$ of $\mathsf{S4}$. First, we show that, while all these logics have finitely many $\{\Box,\Diamond\}$- and $\{\neg,\Box\}$-modalities, the logic $\mathsf{CS4}$ has infinitely many $\{\neg,\Diamond\}$-modalities. Second, we show that $\mathsf{IS4}$ and $\mathsf{GS4}$ have finitely many $\{\neg,\Diamond\}$-modalities, but they have infinitely many $\{\neg,\Box,\Diamond\}$-modalities. At last, we show that $\mathsf{GS4^c}$ has finitely many $\{\neg,\Box,\Diamond\}$-modalities.

math.LO↗

arXiv2026

Polytopological Semantics for Intuitionistic Modal Logics

We develop polytopological semantics for various constructive, intuitionistic, and Gödel--Dummett variations of $\mathsf{K4}$ and $\mathsf{S4}$. In our models, intuitionistic and modal operators are interpreted via various topologies over a single set, equipped with either the closure or derivative operators. We identify regularity conditions to ensure that spaces validate each of our target logics and prove that all the logics considered are sound and strongly complete with respect to their respective semantics.

math.LO↗

arXiv2026

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems

We study a variant of the modal $μ$-calculus based on the constructive modal logic $\mathsf{CK}$. We define game semantics for the constructive $μ$-calculus and prove its equivalence to the birelational Kripke semantics. We then use the game semantics to prove the soundness and completeness of a fully-labeled non-wellfounded proof system for it. At last, we briefly describe how to adapt the game semantics and proof system to the $μ$-calculus over other non-classical modal logics.

cs.LO↗

arXiv2025

The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics

The modal mu-calculus is obtained by adding least and greatest fixed-point operators to modal logic. Its alternation hierarchy classifies the mu-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The mu-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all n, there is a mu-formula with alternation depth n+1 which is not equivalent to any formula with alternation depth n. This does not always happen if we restrict the semantics. For example, every mu-formula is equivalent to a formula without fixed-point operators over S5 frames. We show that the multimodal mu-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the mu-calculus collapses to modal logic.

cs.LO↗

arXiv2024

Game semantics for the constructive $μ$-calculus

We define game semantics for the constructive $μ$-calculus and prove its equivalence to bi-relational semantics. As an application, we use the game semantics to prove that the $μ$-calculus collapses to modal logic over the modal logic $\mathsf{IS5}$. We then show the completeness of $\mathsf{IS5}$ extended with fixed-point operators.

math.LO↗

arXiv2024

Collapsing Constructive and Intuitionistic Modal Logics

We prove that the constructive and intuitionistic variants of the modal logic $\mathsf{KB}$ coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of $\mathsf{K}$ do not prove the same diamond-free formulas.

math.LO↗

arXiv2023

Determinacy and reflection principles in second-order arithmetic

It is known that several variations of the axiom of determinacy play important roles in the study of reverse mathematics, and the relation between the hierarchy of determinacy and comprehension are revealed by Tanaka, Nemoto, Montalbán, Shore, and others. We prove variations of a result by Kołodziejczyk and Michalewski relating determinacy of arbitrary boolean combinations of $Σ^0_2$ sets and reflection in second-order arithmetic. Specifically, we prove that: over $\mathsf{ACA}_0$, $Π^1_2$-$\mathsf{Ref}(\mathsf{ACA}_0)$ is equivalent to $\forall n.(Σ^0_1)_n$-$\mathsf{Det}^*_0$; $Π^1_3$-$\mathsf{Ref}(Π^1_1$-$\mathsf{CA}_0)$ is equivalent to $\forall n.(Σ^0_1)_n$-$\mathsf{Det}$; and $Π^1_3$-$\mathsf{Ref}(Π^1_2$-$\mathsf{CA}_0)$ is equivalent to $\forall n.(Σ^0_2)_n$-$\mathsf{Det}$. We also restate results by Montalbán and Shore to show that $Π^1_3$-$\mathsf{Ref}(\mathsf{Z}_2)$ is equivalent to $\forall n.(Σ^0_3)_n$-$\mathsf{Det}$ over $\mathsf{ACA}_0$.

math.LO↗