Searcharxiv⌕ Search

arXiv subjects

Toshiyasu Arai

Publications and source records attributed to Toshiyasu Arai.

44 records · Page 3Linked to original sources
arXiv2010

Iterating the recursively Mahlo operations

In this paper we address a problem: How far can we iterate lower recursively Mahlo operations in higher reflecting universes? Or formally: How much can lower recursively Mahlo operations be iterated in set theories for higher reflecting universes? It turns out that in $Π_N$-reflecting universes the lowest recursively Mahlo operation can be iterated along towers of $Σ_1$-exponential orderings of height $N-3$, and that all we can do is such iterations. Namely the set theory for $Π_N$-reflecting universes is proof-theoretically reducible to iterations of the operation along such a tower.

math.LO↗
arXiv2010

Provably $Δ^0_2$ and weakly descending chains

In this note we show that a set is provably $Δ^0_2$ in the fragment $IΣ_n$ of arithmetic iff it is $IΣ_n$-provably in the class $D_α$ of $α$-r.e. sets in the Ershov hierarchy for an $α<_{ε_0} ω_{1+n}$, where $<_{ε_0}$ denotes a standard $ε_0$-ordering. In the Appendix it is shown that a limit existence rule $(LimR)$ due to Beklemishev and Visser becomes stronger when the number of nested applications of the inference rule grows.

math.LO↗
arXiv2010

Intuitionistic fixed point theories over Heyting arithmetic

In this paper we show that an intuitionistic theory for fixed points is conservative over the Heyting arithmetic with respect to a certain class of formulas. This extends partly the result of mine. The proof is inspired by the quick cut-elimination due to G. Mints.

math.LO↗
arXiv2010

Exact bounds on epsilon processes

In this paper we show that the lengths of the approximating processes in epsilon substitution method are calculable by ordinal recursions in an optimal way.

math.LO↗
arXiv2010

nested PLS

In this note we will introduce a class of search problems, called nested Polynomial Local Search (nPLS) problems, and show that definable NP search problems, i.e., $Σ^b_1$-definable functions in $T^2_2$ are characterized in terms of the nested PLS.

math.LO↗
arXiv2008

A new function algebra of EXPTIME functions by safe nested recursion

Bellantoni and Cook have given a function-algebra characterization of the polynomial-time computable functions via an unbounded recursion scheme which is called safe recursion. Inspired by their work, we characterize the exponential-time computable functions with the use of a safe variant of nested recursion.

cs.CC↗
arXiv1998

Bounded arithmetic AID for Frege system

In this paper we introduce a system AID (Alogtime Inductive Definitions) of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss' propositional consistency proof of Frege systems F. We show that AID proves the soundness of F, and conversely any Σ^b_0-theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ^b_1-faithful interpretations between AID + Σb^_0 - CA and a quantified theory QALV of an equational system ALV in P. Clote. Hence ALV also proves the soundness of F.

math.LO↗