In this paper we formulate epsilon substitution method for a theory $\Pi _{2}^{0}$-FIX for non-monotonic $\Pi _{2}^{0}$ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].

In this paper we formulate epsilon substitution method for a theory $\Pi _{2}^{0}$-FIX for non-monotonic $\Pi _{2}^{0}$ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].

Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert's Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,… . The problem is to show that the approximating process terminates. After Gentzen's innovation, Ackermann 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints as an Ariadne's (...) thread we formulate the epsilon substitution method for the theory ID1 of non-iterated inductive definitions for disjunctions of simply universal and existential operators, and give a termination proof of the H-process based on Ackermann 162). The termination proof is based on transfinite induction up to the Howard ordinal. (shrink)

This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.

This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.

In this, journal, W. Buchholz gave an elegant proof of a characterization theorem for provably total recursive functions in the theory IDv for the v-times iterated inductive definitions . He characterizes the classes of functions by Hardy functions. In this note we will show that a slow growing analogue to the theorem can be obtained by a slight modification of Buchholz' proof.

We formulate epsilon substitution method for theories (H)α0 of absolute jump hierarchies, and give two termination proofs of the H-process: The first proof is an adaption of Mints M, Mints-Tupailo-Buchholz MTB, i.e., based on a cut-elimination of a specially devised infinitary calculus. The second one is an adaption of Ackermann Ack. Each termination proof is based on transfinite induction up to an ordinal θ(α0+ ω)0, which is best possible.

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

In this note the well-ordering principle for the derivative \ of normal functions \ on ordinals is shown to be equivalent to the existence of arbitrarily large countable coded \-models of the well-ordering principle for the function \.

In this paper we introduce a recursive notation system $O(\mu)$ of ordinals. An element of the notation system is called an ordinal diagram following G. Takeuti [25]. The system is designed for proof theoretic study of theories of recursively Mahlo universes. We show that for each $\alpha<\Omega$ in $O(\mu)$ KPM proves that the initial segment of $O(\mu)$ determined by $\alpha$ is a well ordering. Proof theoretic study for such theories will be reported in [9].

In this paper, we prove the wellfoundedness of recursive notation systems for reflecting ordinals up to Π₃-reflection by relevant inductive definitions.

We show that the existence of a weakly compact cardinal over the Zermelo–Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.

In this paper we introduce a recursive notation system O(Π 3 ) of ordinals. An element of the notation system is called an ordinal diagram. The system is designed for proof theoretic study of theories of Π 3 -reflection. We show that for each $\alpha in O(Π 3 ) a set theory KP Π 3 for Π 3 -reflection proves that the initial segment of O(Π 3 ) determined by α is a well ordering. Proof theoretic study for such theories (...) will be reported in [4]. (shrink)

We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down $\alpha\mapsto\alpha [1]$ in ordinals. Also a generalization to theories $ID_q$ of finitely iterated inductive definitions is proved.

In this paper we introduce a system AID 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 in Buss 3–29). We show that AID proves the soundness of F , and conversely any Σ 0 b -theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ 1 b -faithful interpretations between AID+Σ 0 b -CA and (...) a quantified theory QALV of an equational system ALV in Clote 57–106). Hence ALV also proves the soundness of F. (shrink)

In this note we give a simplified ordinal analysis of first-order reflection. An ordinal notation system$OT$is introduced based on$\psi $-functions. Provable$\Sigma _{1}$-sentences on$L_{\omega _{1}^{CK}}$are bounded through cut-elimination on operator controlled derivations.

For α < ε0, Nα denotes the number of occurrences of ω in the Cantor normal form of α with the base ω. For a binary number-theoretic function f let B denote the length n of the longest descending chain of ordinals <ε0 such that for all i < n, Nαi ≤ f . Simpson [2] called ε0 as slowly well ordered when B is totally defined for f = K · . Let |n| denote the binary length of the (...) natural number n, and |n|k the k-times iterate of the logarithmic function |n|. For a unary function h let L denote the function B ) with h0 = K + |i| · |i|h. In this note we show, inspired from Weiermann [4], that, under a reasonable condition on h, the functionL is primitive recursive in the inverse h–1 and vice versa. (shrink)

Weiermann [18] introduces a new method to generate fast growing functions in order to get an elegant and perspicuous proof of a bounding theorem for provably total recursive functions in a formal theory, e.g., in PA. His fast growing function θαn is described as follows. For each ordinal α and natural number n let T α n denote a finitely branching, primitive recursive tree of ordinals, i.e., an ordinal as a label is attached to each node in the tree so (...) that the labelling is compatible with the tree ordering. Then the tree T α n is well founded and hence finite by Konig's lemma. Define θαn=the depth of the tree T α n =the length of the longest branch in T α n . We introduce new fast and slow growing functions in this mode of definitions and show that each of these majorizes provably total recursive functions in PA. (shrink)

In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of 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.

In this paper we show that the intuitionistic fixed point theory FiXi over set theories T is a conservative extension of T if T can manipulate finite sequences and has the full foundation schema.

Inspired from a joint work by A. Beckmann, S. Buss and S. Friedman, we propose a class of set-theoretic functions, predicatively computable set functions. Each function in this class is polynomial time computable when we restrict to finite binary strings.

In Arai (An ordinal analysis of a single stable ordinal, submitted) it is shown that an ordinal \(\sup _{N is an upper bound for the proof-theoretic ordinal of a set theory \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma _{1}}V)\). In this paper we show that a second order arithmetic \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) proves the wellfoundedness up to \(\psi _{\varOmega _{1}}(\varepsilon _{\varOmega _{{\mathbb {S}}+N+1}})\) for each _N_. It is easy to interpret \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) in \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma (...) _{1}}V)\). (shrink)

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.

Following our [6], though with somewhat different methods here, further variants of Goodstein sequences are introduced in terms of parameterized Ackermann–Péter functions. Each of the sequences is shown to terminate, and the proof-theoretic strengths of these facts are calibrated by means of ordinal assignments, yielding independence results for a range of theories: PRA, PA,$\Sigma ^1_1$-DC$_0$, ATR$_0$, up to ID$_1$. The key is the so-called “Hardy hierarchy” of proof-theoretic bounding finctions, providing a uniform method for associating Goodstein-type sequences with parameterized normal (...) form representations of positive integers. (shrink)

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., \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Sigma^{b}_{1}}$$\end{document}-definable functions in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${T^{2}_{2}}$$\end{document} are characterized in terms of the nested PLS.

In this paper we show some non-elementary speed-ups in logic calculi: Both a predicative second-order logic and a logic for fixed points of positive formulas are shown to have non-elementary speed-ups over first-order logic. Also it is shown that eliminating second-order cut formulas in second-order logic has to increase sizes of proofs super-exponentially, and the same in eliminating second-order epsilon axioms. These are proved by relying on results due to P. Pudlák.

In this note the proof-theoretic ordinal of the well-ordering principle for the normal functions \ on ordinals is shown to be equal to the least fixed point of \. Moreover corrections to the previous paper are made.