arXiv subjects

Tenyo Takahashi

Publications and source records attributed to Tenyo Takahashi.

7 recordsLinked to original sources

arXiv2026

Non-elementary modal logics, assuming P $\neq$ NP

A modal logic is elementary if it is sound and complete with respect to an elementary class of Kripke frames. We prove that if a finitely axiomatizable modal logic L is elementary, then the validity problem for L, which asks whether a given finite Kripke frame validates L, is in P. This allows us to transfer complexity results in graph theory to the study of elementarity of modal logics. As an application, we construct infinitely many finitely axiomatizable K4-stable logics that are not elementary, assuming P $\neq$ NP. This result provides a conditional negative answer to an open question in [Bezhanishvili et al., 2018] for K4-stable logics.

math.LO↗

arXiv2026

Most properties are undecidable even in $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$

We investigate decidability of properties in the lattice $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$ of extensions of the Grzegorczyk tense logic $\mathsf{Grz}_t$ and the lattice $\mathop{\mathsf{NExt}} \mathsf{S4}_t$ of reflexive and transitive tense logics, with applications to the lattice $\mathop{\mathsf{Ext}} \mathsf{biIPC}$ of bi-superintuitionistic logics. We prove that a broad class of properties is undecidable in $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$, including tabularity, Kripke completeness, the finite model property, and decidability, which also yields their undecidability in $\mathop{\mathsf{NExt}} \mathsf{S4}_t$. We also construct infinitely many tabular extensions of $\mathsf{Grz}_t$ (and thus of $\mathsf{S4}_t$) whose coincidence problems are undecidable, while presenting one tabular extension of $\mathsf{Grz}_t$ and infinitely many ones of $\mathsf{S4}_t$ with a decidable coincidence problem. As a consequence, we obtain that the finite model property and tabularity are undecidable in $\mathop{\mathsf{Ext}} \mathsf{biIPC}$, and that there are infinitely many tabular extensions of $\mathsf{biIPC}$ whose coincidence problems are undecidable. These results clarify some similarities and differences between $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$ and $\mathop{\mathsf{NExt}} \mathsf{Grz}$, $\mathop{\mathsf{NExt}} \mathsf{S4}_t$ and $\mathop{\mathsf{NExt}} \mathsf{S4}$, as well as $\mathop{\mathsf{Ext}} \mathsf{biIPC}$ and $\mathop{\mathsf{Ext}} \mathsf{IPC}$. The proofs adapt Chagrov's method of reducing from an undecidable problem for Minsky machines. We isolate and explicitly formulate the method of good valuations, a recurring technique underlying several proofs in the literature that use large frames, making it available for further applications.

math.LO↗

arXiv2026

Most Properties are Undecidable for Transitive Tense Logics

A logics' property is decidable in a class of logics if there exists an algorithm that decides whether a finitely axiomatizable logic in the class has the property. Many properties are undecidable for bimodal logics but decidable for linear tense logics, which leads to a general question on how the interactions of modalities affect the decidability of properties. In this paper, we study the decidability of properties for transitive tense logics and show that most properties are undecidable in the lattice NExt(K4t) of transitive tense logics, including Kripke completeness, the finite model property, and decidability. Our proof method adapts Chagrov's approach of constructing a reduction from an undecidable problem of Minsky machines to the decision problem for logics' properties, yielding a general scheme of proving the undecidability of these properties.

cs.LO↗

arXiv2026

The Cardinalities of Intervals of Equational Theories and Logics

We study the cardinality of classes of equational theories (varieties) and logics by applying descriptive set theory. We affirmatively solve open problems raised by Jackson and Lee [Trans. Am. Math. Soc. 370 (2018), pp. 4785-4812] regarding the cardinalities of subvariety lattices, and by Bezhanishvili et al. [J. Math. Log. (2025), in press] regarding the degrees of the finite model property (fmp). By coding equations and formulas by natural numbers, and theories and logics by real numbers, we examine their position in the Borel hierarchy. We prove that every interval of equational theories in a countable language corresponds to a $\boldsymbol{\Pi}^0_1$ set, and every fmp span of a normal modal logic to a $\boldsymbol{\Pi}^0_2$ set. It follows that they have cardinality either $\leq \aleph_0$ or $2^{\aleph_0}$, provably in ZFC. In the same manner, we observe that the set of pretabular extensions of a tense logic is a $\boldsymbol{\Pi}^0_2$ set, so its cardinality is either $\leq \aleph_0$ or $2^{\aleph_0}$. We also point out a negative solution to another open problem raised by Jackson and Lee, op. cit., regarding the existence of independent systems, which relies on Je\v{z}ek et al. [Bull. Aust. Math. Soc. 42 (1990), pp. 57-70].

math.LO↗

arXiv2025

Chopping More Finely: Finite Countermodels in Modal Logic via the Subdivision Construction

We present a new method, the Subdivision Construction, for proving the finite model property (the fmp) for broad classes of modal logics and modal rule systems. The construction builds on the framework of stable canonical rules, and produces a finite modal space, dually, a finite modal algebra, that serves as a finite countermodel of such rules, yielding the fmp. We apply the Subdivision Construction to prove the fmp for logics and rule systems axiomatized by stable canonical formulas and rules of finite modal algebras of finite height. As a consequence, we identify a class of union-splittings in $\mathsf{NExt}(\mathsf{K4})$ with degree of Kripke incompleteness 1.

math.LO↗

arXiv2025

Stable Canonical Rules and Formulas for Pre-transitive Logics via Definable Filtration

We generalize the theory of stable canonical rules by adopting definable filtration, a generalization of the method of filtration. We show that for a modal rule system or a modal logic that admits definable filtration, each extension is axiomatizable by stable canonical rules. Moreover, we provide an algebraic presentation of Gabbay's filtration and generalize stable canonical formulas and the axiomatization results via stable canonical formulas for $\mathsf{K4}$ to pre-transitive logics $\mathsf{K4^{m+1}_{1}} = \mathsf{K} + \Diamond^{m+1} p \to \Diamond p$ $(m \geq 1)$. As consequences, we obtain the fmp of $\mathsf{K4^{m+1}_{1}}$-stable logics and a characterization of splitting and union-splitting logics in the lattice $\mathsf{NExt}\mathsf{K4^{m+1}_{1}}$. There are continuum many $\mathsf{K4^{m+1}_{1}}$-stable logics that are neither $\mathsf{K4}$-stable logics nor subframe logics. Finally, we introduce $m$-stable canonical formulas, strengthening the axiomatization results for these logics.

math.LO↗

arXiv2025

Decidability of Being a Union-splitting

Many logical properties are known to be undecidable for normal modal logics, with few exceptions such as consistency and coincidence with $\mathsf{K}$. This paper shows that the property of being a union-splitting in $\mathsf{NExt}\mathsf{K}$, the lattice of normal modal logics, is decidable, thus answering the open problem [WZ07, Problem 2]. This is done by providing a semantic characterization of union-splittings in terms of finite modal algebras. Moreover, by clarifying the connection to union-splittings, we show that in $\mathsf{NExt}\mathsf{K}$, having a decidable axiomatization problem and being a (un)decidable formula are also decidable. The latter answers [CZ97, Problem 17.3] for $\mathsf{NExt}\mathsf{K}$.

math.LO↗