A constructive proof of a theorem by Ferreira-Zantema
This note was written in Jan. 23, 2015 to answer a problem raised by G. Moser, who asked a constructive proof of a theorem by Ferreira-Zantema.
Source author record
Toshiyasu Arai
Toshiyasu Arai appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.
ResearcherUnclaimed source record
Catalog footprint
What is connected
23works
2topics
0close collaborators
Research graph
See the researcher in context
Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
23 published item(s)
preprint2020arXiv
Refinement of proof-theoretic analysis of the lpo due to Buchholz
We give a refinement of proof-theoretic analysis of the lpo (lexicographic path order) due to W. Buchholz. This note was written in Feb. 5, 2015 when G. Moser visited Japan.
0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv
Two remarks on proof theory of first-order arithmetic
In this note let us give two remarks on proof-theory of PA. First a derivability relation is introduced to bound witnesses for provable $Σ_{1}$-formulas in PA. Second Paris-Harrington's proof for their independence result is reformulated to show a `consistency' proof of PA based on a combinatorial principle.
0 citations0 reviewsNo code linkedOpen access
preprint2017arXiv
Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema
Following G. Mints(Kluwer 2000 and draft 2013), we present terminating and bicomplete proof searches in multi-succedent sequent calculi for intuitionistic propositional logic, fragments of intuitionistic predicate logic and full intuitionistic predicate logic in the spirit of Schuette's schema.
0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv
Cut-elimination for SBL
In this paper we give a terminating cut-elimination procedure for a logic calculus SBL. SBL corresponds to the second order arithmetic Pi^{1}_{2}-Separation and Bar Induction.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
$omega_{1}$ under $Pi_{1}$-Collection
We describe a proof-theoretic bound on $Sigma_{2}$-definable countable ordinals in Kripke-Platek set theory with $Pi_{1}$-Collection and the existence of $omega_{1}$.
0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv
Lifting proof theory to the countable ordinals II: second-order indescribable cardinals
We show that the existence of a Pi^{1}_{N}-indescribable cardinal over the Zermelo-Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and lower Mahlo operations. Furthermore we describe a proof-theoretic bound on definable countable ordinals whose existence is provable from the existence of second order indescribable cardinals over ZF.
0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv
Predicatively computable functions on sets
Inspired from a joint work by A. Beckmann, S. Buss and S. Friedman, we propose a class of set-theoretic functions, predicatively computable functions. Each function in this class is polynomial time computable when we restrict to finite binary strings.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
A polynomial time complete disjunction property in intuitionistic propositional logic
We extend the polynomial time algorithms due to Buss and Mints(APAL 1999) and Ferrari, Fiorentini and Fiorino(LPAR 2002) to yield a polynomial time complete disjunction property in intuitionistic propositional logic.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
Conservations of first-order reflections
The set theory KP$Π_{N+1}$ for $Π_{N+1}$-reflecting universes is shown to be $Π_{N+1}$-conservative over iterations of $Π_{N}$-recursively Mahlo operations for each $N\geq 2$.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
Lifting up the proof theory to the countables : Zermelo-Fraenkel set theory
We describe the countable ordinals in terms of iterations of Mostowski collapsings. This gives a proof-theoretic bound of definable countable ordinals in the Zermelo-Fraenkel's set theory ZF.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
Proof theory of weak compactness
We show that the existence of a weakly compact cardinal over the Zermelo-Fraenkel's set theory is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.
0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv
A sneak preview of proof theory of ordinals
This talk is a sneak preview of the project, 'proof theory for theories of ordinals'. Background, aims, survey and furture works on the project are given. Subsystems of second order arithmetic are embedded in recursively large ordinals and then the latter are analysed. We scarcely touch upon proof theoretical matters.
0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv
Introducing the hardline in proof theory
In this paper we expound some basic ideas of proof theory for theories of ordinals such that there are many stable ordinals below the ordinals.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
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.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
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.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
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.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
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.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
Proof theory for theories of ordinals III: $Π_{N}$-reflection
This paper deals with a proof theory for a theory of $Π_{N}$-reflecting ordinals using a system of ordinal diagrams. This is a sequel to the previous one(APAL 129)in which a theory for $Π_{3}$-reflection is analysed proof-theoretically.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
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.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
Quick cut-elimination for strictly positive cuts
In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of the Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
Wellfoundedness proofs by means of non-monotonic inductive definitions II: first order operators
In this paper, we give two proofs of the wellfoundedness of recursive notation systems for $Π_N$-reflecting ordinals. One is based on $Π_{N-1}^0$-inductive definitions, and the other is based on distinguished classes.
0 citations0 reviewsNo code linkedOpen access
preprint1998arXiv
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.
0 citations0 reviewsNo code linkedOpen access