arXiv subjects

Taishi Kurahashi

Publications and source records attributed to Taishi Kurahashi.

At least 19 recordsLinked to original sources

arXiv2026

Fixed points in abstract provability structures

We study fixed points in abstract provability structures (APSs), which were introduced by Beklemishev and Shamkanov as an order-theoretic framework for studying Gödel's second incompleteness theorem (G2). For one-variable APS terms built from the provability and refutability operations $\Box$ and $\boxtimes$, we investigate the existence and uniqueness of fixed points in terms of their degree. The degree of a term is the number of occurrences of $\boxtimes$. We prove that every term of degree two has a fixed point and establish a strict hierarchy among the fixed-point properties of the terms $\boxtimes\Box^k v$. We further show that suitable levels of this hierarchy guarantee the existence and uniqueness of fixed points for arbitrary one-variable APS terms of positive degree. We also obtain several G2-like non-refutability results, some of which depend only on whether the degree is even or odd. Finally, we consider APSs based on meet-semilattices. Under an additional condition, we obtain stronger fixed-point results and show that a parametrized fixed-point property implies an abstract form of Löb's theorem.

math.LO↗

arXiv2026

Very weak subintuitionistic logics

We introduce a new propositional logic, called very weak subintuitionistic logic $\mathbf{VF}$, by adapting the relational semantics of Fitting, Marek, and Truszczyński for the pure logic of necessitation $\mathbf{N}$ to the propositional setting. We prove that $\mathbf{VF}$ and its closed negative extensions are sound and complete with respect to this semantics, and that they have the disjunction property and the finite frame property. We also prove that $\mathbf{VF}$ is strictly weaker than the weak subintuitionistic logic $\mathbf{WF}$ of Maleki and de Jongh. Finally, we study modal companions of $\mathbf{VF}$ and its closed negative extensions via Corsi's modified Gödel translation.

math.LO↗

arXiv2026

Modal logics of conjunctively closed provability predicates

We investigate non-normal modal logics corresponding to provability predicates $\mathrm{Pr}_T(x)$ satisfying the derivability condition $\mathbf{C}$: $T\vdash\mathrm{Pr}_T(\ulcorner φ\urcorner)\land\mathrm{Pr}_T(\ulcorner ψ\urcorner)\to \mathrm{Pr}_T(\ulcorner φ\landψ\urcorner)$. The modal counterpart of this condition is the axiom scheme $\mathsf{C}$: $\Box A\land\Box B\to\Box(A\land B)$. First, we introduce a new semantics based on closure operators for non-normal modal logics including logics adopting $\mathsf{C}$ as an axiom scheme. We prove modal completeness for several non-normal modal logics studied in this paper with respect to this semantics. Second, we prove the arithmetical completeness theorems for the logics $\mathsf{CN}$, $\mathsf{CNP}$, $\mathsf{CNF}$, $\mathsf{CNPF}$, and $\mathsf{CND}$ by using our new semantics.

math.LO↗

arXiv2026

Modal logical aspects of provability predicates and consistency statements

This paper studies the modal logical aspects of provability predicates and consistency statements for theories of arithmetic. First, we provide an overview of previous works on the correspondence between various derivability conditions for provability predicates and different modal logics. The main technical contribution of the present paper is to establish the arithmetical completeness of the logics $\mathsf{NP}$, $\mathsf{ND}$, $\mathsf{NP4}$, and $\mathsf{ND4}$ by extending Solovay's method and refining Arai's construction of Rosser provability predicates.

math.LO↗

arXiv2026

Finite Kripke models and provability interpretations in quantified modal logic

In this paper, we investigate arithmetical completeness with respect to finite Kripke models of quantified modal logic. We adapt the finite-model embedding techniques of Artemov and Japaridze to two settings involving finite Kripke models. First, for conversely well-founded finite Kripke models of quantified modal logic, we construct a $Σ_2$ Fefermanian provability predicate together with an arithmetical interpretation that embeds the model into arithmetic. Second, for finite constant domain Kripke models of quantified modal logic, we construct a $Σ_1$ provability predicate satisfying $\mathbf{D2^G}$ and an arithmetical interpretation yielding such an embedding.

math.LO↗

arXiv2026

Extensional Independence

Joel Hamkins asks whether there is a $Π^0_1$-formula $ρ(x)$ such that $ρ(ϕ)$ is independent over ${\sf PA}+ϕ$, if this theory is consistent, where this construction is extensional in $ϕ$ with respect to ${\sf PA}$-provable equivalence. We show that there can be no such extensional Rosser formula of any complexity. We give a positive answer to Hamkins' question for the case where we replace Extensionality by a weaker demand *Consistent Extensionality*. We also prove that we can demand the negation of $ρ$ to be $Π^0_1$-conservative, if we ask for the still weaker *Conditional Extensionality*. We show that an intensional version of the result for Conditional Extensionality cannot work.

math.LO↗

arXiv2025

Refinements of provability and consistency principles for the second incompleteness theorem

This paper continues the author's previous study \cite{Kura20}, showing that several weak principles inspired by non-normal modal logic suffice to derive various refined forms of the second incompleteness theorem. Among the main results of the present paper, we show that the set $\{\mathbf{E},\mathbf{C}, \mathbf{D3}\}$ suffices to establish the unprovability of the consistency statement $\neg\, \mathrm{Pr}_T(\ulcorner 0=1 \urcorner)$. We also prove that the set $\{\mathbf{E}^{\mathrm{U}}, \mathbf{CB_{\exists}}\}$ yields formalized $Σ_1$-completeness.

math.LO↗

arXiv2025

Hierarchical formula classes with respect to semi-classical prenex normalization

In [10], the authors formalized the standard transformation procedure for prenex normalization of first-order formulas and showed that the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ introduced in Akama et al. [1] are exactly the classes induced by $Σ_k$ and $Π_k$ respectively via the transformation procedure. In that sense, the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ correspond to $Σ_k$ and $Π_k$ based on classical logic respectively. On the other hand, some transformations of the prenex normalization are not possible in constructive theories. In this paper, we introduce new classes $\mathcal{E}_k^n$ and $\mathcal{U}_k^n$ of first-order formulas with two parameters $k$ and $n$, and show that they are exactly the classes induced by $Σ_k$ and $Π_k$ respectively according to the $n$-th level semi-classical prenex normalization, which is obtained by the prenex normalization in [10] with some restriction to the introduced classes of degree $n$. In particular, the latter corresponds to possible transformations in intuitionistic arithmetic augmented with the law-of-excluded-middle schema restricted to formulas of $Σ_n$-form. In fact, if $ n\geq k$, our classes $\mathcal{E}_k^n$ and $\mathcal{U}_k^n$ are identical with the cumulative variants $\mathrm{E}^+_k$ and $\mathrm{U}^+_k$ of $\mathrm{E}_k$ and $\mathrm{U}_k$ respectively. In this sense, our classes are refinements of $\mathrm{E}^+_k$ and $\mathrm{U}^+_k$ with respect to the prenex normalization from the semi-classical perspective.

math.LO↗

arXiv2025

Lyndon interpolation property for extensions of $\mathbf{S4}$ and intermediate propositional logics

We study the Lyndon interpolation property (LIP) and the uniform Lyndon interpolation property (ULIP) for extensions of $\mathbf{S4}$ and intermediate propositional logics. We prove that among the 18 consistent normal modal logics of finite height extending $\mathbf{S4}$ known to have CIP, 11 logics have LIP and 7 logics do not. We also prove that for intermediate propositional logics, the Craig interpolation property, LIP, and ULIP are equivalent.

math.LO↗

arXiv2025

Doubly partially conservative sentences

The purpose of the present paper is to analyze several variants of Solovay's theorem on the existence of doubly partially conservative sentences. First, we investigate $Θ$ sentences that are doubly $(Γ, Λ)$-conservative over $T$ for several triples $(Θ, Γ, Λ)$. Among other things, we prove that the existence of a $Δ_{n+1}(\mathsf{PA})$ sentence that is doubly $(Σ_n, Σ_n)$-conservative over $T$ is equivalent to the $Σ_{n+1}$-inconsistency of $T$ over $\mathsf{PA}$. Secondly, we study $Θ$ sentences that are hereditarily doubly $(Γ, Λ)$-conservative over $T$ for several triples $(Θ, Γ, Λ)$.

math.LO↗

arXiv2025

A variety of partially conservative sentences

We study the existence of a $Θ$ sentence which is simultaneously $Γ$-conservative over consistent RE extensions $T$ and $U$ of Peano Arithmetic for various reasonable pairs $(Γ, Θ)$. As a result of this study, we prove the existence of a sentence which is essentially $Θ$ and exactly hereditarily $Γ$-conservative over any single theory $T$ for various reasonable pairs $(Γ, Θ)$. This is an affirmative answer to Guaspari's question.

math.LO↗

arXiv2025

Smullyan's truth and provability

We revisit Smullyan's paper ``Truth and Provability'' (2013) for three purposes. First, we introduce the notion of Smullyan models to give a precise definition for Smullyan's framework discussed in that paper. Second, we clarify the relationship between three theorems proved by Smullyan and other newly introduced properties for Smullyan models in terms of both implications and non-implications. Third, we construct two Smullyan models based on arithmetical ideas and show the correspondence between the properties of these Smullyan models and those concerning truth and provability in arithmetic.

math.LO↗

arXiv2025

Cut-free sequent calculi for the provability logic D

We say that a Kripke model is a GL-model if the accessibility relation $\prec$ is transitive and converse well-founded. We say that a Kripke model is a D-model if it is obtained by attaching infinitely many worlds $t_1, t_2, \ldots$, and $t_ω$ to a world $t_0$ of a GL-model so that $t_0 \succ t_1 \succ t_2 \succ \cdots \succ t_ω$. A non-normal modal logic D, which was studied by Beklemishev (1999), is characterized as follows. A formula $φ$ is a theorem of D if and only if $φ$ is true at $t_ω$ in any D-model. D is an intermediate logic between the provability logics GL and S. A Hilbert-style proof system for D is known, but there has been no sequent calculus. In this paper, we establish two sequent calculi for D, and show the cut-elimination theorem. We also introduce new Hilbert-style systems for D by interpreting the sequent calculi. Moreover, we show that D-models can be defined using an arbitrary limit ordinal as well as $ω$. Finally, we show a general result as follows. Let $X$ and $X^+$ be arbitrary modal logics. If the relationship between semantics of $X$ and semantics of $X^+$ is equal to that of GL and D, then $X^+$ can be axiomatized based on $X$ in the same way as the new axiomatization of D based on GL.

math.LO↗

arXiv2024

On collection schemes and Gaifman's splitting theorem

We study model theoretic characterizations of various collection schemes over $\mathbf{PA}^-$ from the viewpoint of Gaifman's splitting theorem. Among other things, we prove that for any $n \geq 0$ and $M \models \mathbf{PA}^-$, the following are equivalent: 1. $M$ satisfies the collection scheme for $Σ_{n+1}$ formulas. 2. For any $K, N \models \mathbf{PA}^-$, if $M \subseteq_{\mathrm{cof}} K$, $M \prec_{Δ_0} K$ and $M \prec N$, then $M \prec_{Σ_{n+2}} K$ and $\sup_N(M) \prec_{Σ_n} N$. 3. For any $N \models \mathbf{PA}^-$, if $M \prec N$, then $M \prec_{Σ_{n+2}} \sup_N(M) \prec_{Σ_{n}} N$. Here, $\sup_N(M)$ is the unique $K$ satisfying $M \subseteq_{\mathrm{cof}} K \subseteq_{\mathrm{end}} N$. We also investigate strong collection schemes and parameter-free collection schemes from the similar perspective.

math.LO↗

arXiv2024

The finite frame property of some extensions of the pure logic of necessitation

We study the finite frame property of some extensions of Fitting, Marek, and Truszczyński's pure logic of necessitation $\mathbf{N}$. For any natural numbers $m, n$, we introduce the logic $\mathbf{N}^+\mathbf{A}_{m, n}$ by adding the single axiom scheme $\Box^n φ\to \Box^m φ$ and the rule $\dfrac{\neg \Box φ}{\neg \Box \Box φ}$ (Ros$^\Box$) into $\mathbf{N}$. We prove the finite frame property of $\mathbf{N}^+\mathbf{A}_{m, n}$ with respect to Fitting, Marek, and Truszczyński's relational semantics. We also prove that for $n \ge 2$, the logic obtained by removing the rule Ros$^\Box$ from $\mathbf{N}^+\mathbf{A}_{0, n}$ is incomplete with respect to that semantics.

math.LO↗

arXiv2024

Certified $Σ_1$-sentences

In this paper, we study the employment of $Σ_1$-sentences with certificates, i.e., $Σ_1$-sentences where a number of principles is added to ensure that the witness is sufficiently number-like. We develop certificates in some detail and illustrate their use by reproving some classical results and proving some new ones. An example of such a classical result is Vaught's theorem of the strong effective inseparability of $\mathsf{R}_0$. We also develop the new idea of a theory being ${\sf R}_{0{\sf p}}$-sourced. Using this notion, we can transfer a number of salient results from $\mathsf{R}_0$ to a variety of other theories.

math.LO↗

arXiv2024

Pour-El's Landscape

We study the effective versions of several notions related to incompleteness, undecidability and inseparability along the lines of Pour-El's insights. Firstly, we strengthen Pour-El's theorem on the equivalence between effective essential incompleteness and effective inseparability. Secondly, we compare the notions obtained by restricting that of effective essential incompleteness to intensional finite extensions and extensional finite extensions. Finally, we study the combination of effectiveness and hereditariness, and prove an adapted version of Pour-El's result for this combination.

math.LO↗

arXiv2024

Visser frames for sublogics of $\mathbf{IL}$

We study the modal completeness and the finite frame property of several sublogics of the logic $\mathbf{IL}$ of interpretability with respect to Visser frames, which are also called simplified Veltman frames. Among other things, we prove that the logic $\mathbf{CL}$ of conservativity has the finite frame property with respect to that frames. This is an affirmative solution to Ignatiev's problem.

math.LO↗