arXiv subjects

Taishi Kurahashi

Publications and source records attributed to Taishi Kurahashi.

At least 37 records · Page 2Linked to original sources

arXiv2023

On the conservation results for local reflection principles

For a class $Γ$ of formulas, $Γ$ local reflection principle $\mathrm{Rfn}_Γ(T)$ for a theory $T$ of arithmetic is a scheme formalizing the $Γ$-soundness of $T$. Beklemishev proved that for every $Γ\in \{Σ_n, Π_{n+1} \mid n \geq 1\}$, the full local reflection principle $\mathrm{Rfn}(T)$ is $Γ$-conservative over $T + \mathrm{Rfn}_Γ(T)$. We firstly generalize the conservation theorem to nonstandard provability predicates: we prove that the second condition $\mathbf{D2}$ of the derivability conditions is a sufficient condition for the conservation theorem to hold. We secondly investigate the conservation theorem in terms of Rosser provability predicates. We construct Rosser predicates for which the conservation theorem holds and Rosser predicates for which the theorem does not hold.

math.LO↗

arXiv2023

Interpolation properties for the bimodal provability logic $\mathbf{GR}$

We study interpolation properties for Shavrukov's bimodal logic $\mathbf{GR}$ of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic $\mathbf{GR}^\circ$ of $\mathbf{GR}$ and its relational semantics. Based on our new semantics, we prove that $\mathbf{GR}^\circ$ and $\mathbf{GR}$ enjoy Lyndon interpolation property and uniform interpolation property.

math.LO↗

arXiv2023

Prenex normalization and the hierarchical classification of formulas

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ introduced in [1] are exactly the classes induced by $Σ_k$ and $Π_k$ respectively via the transformation procedure in any first-order theory.

math.LO↗

arXiv2023

The Modal Logic of Provability and Forcing

Solovay's arithmetical completeness theorem states that the modal logic of provability coincides with the modal logic $\mathbf{GL}$. Hamkins and Löwe studied the modal logical aspects of set theoretic multiverse and proved that the modal logic of forcing is exactly the modal logic $\mathbf{S4.2}$. We explore the interaction between the notions of provability and forcing in terms of modal logic. We introduce the bimodal logic $\mathbf{PF}$ and prove that the modal logic of provability and forcing is exactly $\mathbf{PF}$. We also introduce the bimodal logic $\mathbf{PF}^ω$ and prove that $\mathbf{PF}^ω$ is exactly the modal logic of provability and forcing true in $ω$-models of set theory.

math.LO↗

arXiv2023

The persistence principle over weak interpretability logic

We focus on the persistence principle over weak interpretability logic. Our object of study is the logic obtained by adding the persistence principle to weak interpretability logic from several perspectives. Firstly, we prove that this logic enjoys a weak version of the fixed point property. Secondly, we introduce a system of sequent calculus and prove the cut-elimination theorem for it. As a consequence, we prove that the logic enjoys the Craig interpolation property. Thirdly, we show that the logic is the natural basis of a generalization of simplified Veltman semantics, and prove that it has the finite frame property with respect to that semantics. Finally, we prove that it is sound and complete with respect to some appropriate arithmetical semantics.

math.LO↗

arXiv2023

The provability logic of all provability predicates

We prove that the provability logic of all provability predicates is exactly Fitting, Marek, and Truszczyński's pure logic of necessitation $\mathsf{N}$. Moreover, we introduce three extensions $\mathsf{N4}$, $\mathsf{NR}$, and $\mathsf{NR4}$ of $\mathsf{N}$ and investigate the arithmetical semantics of these logics. In fact, we prove that $\mathsf{N4}$, $\mathsf{NR}$, and $\mathsf{NR4}$ are the provability logics of all provability predicates satisfying the third condition $\mathbf{D3}$ of the derivabiity conditions, all Rosser's provability predicates, and all Rosser's provability predicates satisfying $\mathbf{D3}$, respectively.

math.LO↗

arXiv2023

Incompleteness and undecidability of theories consistent with $\mathsf{R}$

We prove the following version of the first incompleteness theorem that simultaneously strengthens Mostowski's theorem and Vaught's theorem: For any c.e. family $\{ T_i \}_{i \in ω}$ of consistent extensions of Tarski, Mostowski and Robinson's arithmetic $\mathsf{R}$, there exists a sentence $φ$ of arithmetic such that $φ\vdash \mathsf{R}$ and for all $i \in ω$, $T_i \nvdash φ$ and $T_i \nvdash \neg φ$.

math.LO↗

arXiv2023

Some observations on the FGH theorem

We investigate the Friedman--Goldfarb--Harrington theorem from two perspectives. Firstly, in the frameworks of classical and modal propositional logics, we study the forms of sentences whose existence is guaranteed by the FGH theorem. Secondly, we prove some variations of the FGH theorem with respect to Rosser provability predicates.

math.LO↗

arXiv2023

Arithmetical completeness theorems for monotonic modal logics

We investigate modal logical aspects of provability predicates $\mathrm{Pr}_T(x)$ satisfying the following condition: $\mathbf{M}$: If $T \vdash φ\to ψ$, then $T \vdash \mathrm{Pr}_T(\ulcorner φ\urcorner) \to \mathrm{Pr}_T(\ulcorner ψ\urcorner)$. We prove the arithmetical completeness theorems for monotonic modal logics $\mathsf{MN}$, $\mathsf{MN4}$, $\mathsf{MNP}$, $\mathsf{MNP4}$, and $\mathsf{MND}$ with respect to provability predicates satisfying the condition $\mathbf{M}$. That is, we prove that for each logic $L$ of them, there exists a $Σ_1$ provability predicate $\mathrm{Pr}_T(x)$ satisfying $\mathbf{M}$ such that the provability logic of $\mathrm{Pr}_T(x)$ is exactly $L$. In particular, the modal formulas $\mathrm{P}$: $\neg \Box \bot$ and $\mathrm{D}$: $\neg (\Box A \land \Box \neg A)$ are not equivalent over non-normal modal logic and correspond to two different formalizations $\neg \mathrm{Pr}_T(\ulcorner 0=1 \urcorner)$ and $\neg \big(\mathrm{Pr}_T(\ulcorner φ\urcorner) \land \mathrm{Pr}_T(\ulcorner \neg φ\urcorner) \bigr)$ of consistency statements, respectively. Our results separate these formalizations in terms of modal logic.

math.LO↗

arXiv2022

Disjunction and existence properties in modal arithmetic

We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm{B}$, $Δ(\mathrm{B})$, and $Σ(\mathrm{B})$ of formulas of modal arithmetic, and study basic properties of them. Then, we prove several implications between the properties. In particular, among other things, we prove that for any consistent recursively enumerable extension $T$ of $\mathbf{PA}(\mathbf{K})$ with $T \nvdash \Box \bot$, the $Σ(\mathrm{B})$-disjunction property, the $Σ(\mathrm{B})$-existence property, and the $\mathrm{B}$-existence property are pairwise equivalent. Moreover, we introduce the notion of the $Σ(\mathrm{B})$-soundness of theories, and prove that for any consistent recursively enumerable extension of $\mathbf{PA}(\mathbf{K4})$, the modal disjunction property is equivalent to the $Σ(\mathrm{B})$-soundness.

math.LO↗

arXiv2022

Refining the arithmetical hierarchy of classical principles

We refine the arithmetical hierarchy of various classical principles by finely investigating the derivability relations between these principles over Heyting arithmetic. We mainly investigate some restricted versions of the law of excluded middle, de Morgan's law, the double negation elimination, the collection principle and the constant domain axiom.

math.LO↗

arXiv2022

On Guaspari's problem about partially conservative sentences

We investigate sentences which are simultaneously partially conservative over several theories. First, we generalize Bennet's results on this topic to the case of more than two theories. In particular, for any finite family $\{T_i\}_{i \leq k}$ of consistent r.e. extensions of Peano Arithmetic, we give a necessary and sufficient condition for the existence of a $Π_n$ sentence which is unprovable in $T_i$ and $Σ_n$-conservative over $T_i$ for all $i \leq k$. Secondly, we prove that for any finite family of such theories, there exists a $Σ_n$ sentence which is simultaneously unprovable and $Π_n$-conservative over each of these theories. This constitutes a positive solution to a particular case of Guaspari's problem. Finally, we demonstrate several non-implications among related properties of families of theories.

math.LO↗

arXiv2022

Conservation theorems on semi-classical arithmetic

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf{PA}$ and intuitionistic arithmetic $\mathsf{HA}$. Using a generalized negative translation, we first provide a new structured proof of the fact that $\mathsf{PA}$ is $Π_{k+2}$-conservative over $\mathsf{HA} + Σ_k\text{-}\mathrm{LEM}$ where $Σ_k\text{-}\mathrm{LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $Σ_k$. In addition, we show that this conservation theorem is optimal in the sense that for any semi-classical arithmetic $T$, if $\mathsf{PA}$ is $Π_{k+2}$-conservative over $T$, then $T$ proves $Σ_k\text{-}\mathrm{LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles.

math.LO↗

arXiv2021

Effectively constructible fixed points in Sacchetti's modal logics of provability

We give a purely syntactical proof of the fixed point theorem for Sacchetti's modal logics ${\bf K} + \Box(\Box^n p \to p) \to \Box p$ ($n \geq 2$) of provability. From our proof, an effective procedure for constructing fixed points in these logics is obtained. We also show the existence of simple fixed points for particular modal formulas.

math.LO↗

arXiv2021

Topological semantics of conservativity and interpretability logics

We introduce and develop a topological semantics of conservativity logics and interpretability logics. We prove the topological compactness theorem of consistent normal extensions of the conservativity logic $\mathbf{CL}$ by extending Shehtman's ultrabouquet construction method to our framework. As a consequence, we prove that several extensions of $\mathbf{CL}$ such as $\mathbf{IL}$, $\mathbf{ILM}$, $\mathbf{ILP}$ and $\mathbf{ILW}$ are strongly complete with respect to our topological semantics.

math.LO↗

arXiv2021

On inclusions between quantified provability logics

We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation between quantified provability logics with respect to $Σ_1$ arithmetical interpretations.

math.LO↗

arXiv2020

Modal completeness of sublogics of the interpretability logic $\mathbf{IL}$

We study modal completeness and incompleteness of several sublogics of the interpretability logic $\mathbf{IL}$. We introduce the sublogic $\mathbf{IL}^-$, and prove that $\mathbf{IL}^-$ is sound and complete with respect to Veltman prestructures which are introduced by Visser. Moreover, we prove the modal completeness of twelve logics between $\mathbf{IL}^-$ and $\mathbf{IL}$ with respect to Veltman prestructures. On the other hand, we prove that eight natural sublogics of $\mathbf{IL}$ are modally incomplete. Finally, we prove that these incomplete logics are complete with respect to generalized Veltman prestructures. As a consequence of these investigations, we obtain that the twenty logics studied in this paper are all decidable.

math.LO↗

arXiv2020

Prenex normal form theorems in semi-classical arithmetic

Akama et al. systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem, then modify it in an appropriate way. In addition, we characterize several prenex normal form theorems with respect to semi-classical arithmetic.

math.LO↗