In this paper we study admissible extensions of several theories T of reverse mathematics. The idea is that in such an extension the structure M = ( N , S , ∈ ) of the natural numbers and collection of sets of natural numbers S has to obey the axioms of T while simultaneously one also has a set-theoretic world with transfinite levels erected on top of M governed by the axioms of Kripke-Platek set theory, KP . In some respects, the admissible extension of T can be viewed as a proof-theoretic analog of Barwise's admissible cover of an arbitrary model of set theory; see [2] . However, by contrast, the admissible extension of T is usually not a conservative extension of T . Owing to the interplay of T and KP , either theory's axioms may force new sets of naturals to exist which in turn may engender yet new sets of naturals on account of the axioms of the other. The paper discerns a general pattern though. It turns out that for many familiar theories T , the second order part of the admissible cover of T equates to T augmented by transfinite induction over all initial segments of the Bachmann-Howard ordinal. Technically, the paper uses a novel type of ordinal analysis, expanding that for KP to the higher set-theoretic universe while at the same time treating the world of subsets of N as an unanalyzed class-sized urelement structure. Among the systems of reverse mathematics, for which we determine the admissible extension, are Π 1 1 - CA 0 and ATR 0 as well as the theory of bar induction, BI .

Abstract Strict-$\varPi ^{1}_{1}$ reflection is an important principle that is discussed in detail, e.g. in Barwise [ 2]. Whereas Barwise puts his focus on the importance of strict-$\varPi ^{1}_{1}$ formulas for generalized recursion theory and definability theory, we choose a proof-theoretic approach.

Abstract BON+ is an applicative theory and closely related to the first order parts of the standard systems of explicit mathematics. As such it is also a natural framework for abstract computations. In this article we analyze this aspect of BON+ more closely. First a point is made for introducing a new operation τN, called truncation, to obtain a natural formalization of partial recursive functions in our applicative framework. Then we introduce the operational versions of a series of notions that are all equivalent to semi-decidability in ordinary recursion theory on the natural numbers, and study their mutual relationships over BON+ with τN.

Abstract Starting points of this article are fixed point axioms for set-bounded monotone Σ1 definable operators in the context of Kripke–Platek set theory $KP$ . We analyze their relationship to other principles such as maximal iterations, bounded proper injections, and Σ1 subset-bounded separation. One of our main results states that in $KP + (V\, = \,L)$ all these principles are equivalent to Σ1 separation.

Abstract In this paper first order theories for nonmonotone inductive definitions are introduced, and a proof-theoretic analysis for such theories based on combined operator forms à la Richter with recursively inaccessible and Mahlo closure ordinals is given.

Abstract In this article we introduce systems for metapredicative Mahlo in explicit mathematics and admissible set theory. The exact upper proof-theoretic bounds of these systems are established.

Abstract This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories and ; the exact proof-theoretic ordinals of these systems are presented.

Abstract In this note it is shown that in explicit mathematics the strong power type axiom is inconsistent with (uniform) elementary comprehension and discuss some general aspects of power types in explicit mathematics.

This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET(μ) plus set induction (type induction, formula induction) is proof-theoretically equivalent to Peano arithmetic PA (the second-order system (Π0∞-CA<ε0, the second-order system (Π0∞-CA)<εε0).

Abstract This paper deals with: (i) the theory which results from by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω0.

Abstract This paper deals with some structural properties of the sequent calculus and describes strong symmetries between cut-free derivations and derivations, which do not make use of identity axioms. Both of them are discussed from a semantic and syntactic point of view. Identity axioms and cuts are closely related to the treatment of negation in the sequent calculus, so the results of this article explain some nice symmetries of negation.

Abstract This paper presents several proof-theoretic results concerning weak fixed point theories over second order number theory with arithmetic comprehension and full or restricted induction on the natural numbers. It is also shown that there are natural second order theories which are proof-theoretically equivalent but have different proof-theoretic ordinals.

In this paper we prove a boundedness theorem in the theory ID1(W). This answers a question asked by Feferman, for example in [3]. The background is the following. Let A[X, x] be an X-positive formula arithmetic in X. The theory ID1(PA) is an extension of Peano arithmetic PA by the following axioms: for arbitrary formulas F; PA is a constant for the least fixed point of A[X, x]. Set-theoretically, PA can be defined by recursion on the ordinals as follows: where is the first nonrecursive ordinal. Now let a ≺ b be the arithmetic relation which expresses that the recursive tree coded by a is a proper subtree of the tree coded by b, and define The least fixed point of Tree[X, x] is the set PTree of all well-founded recursive trees. We write W or Wα for PTree or , respectively. Since W is complete we have for all α < . If we define for each element a ∈ W its inductive norm ∣a∣ by ∣a∣≔ min{ξ: a ∈ Wξ}, then we have = {∣a∣: a ∈ W} and the elements of W can be used as codes for the ordinals less than . Assume that B[X, x] is an X-positive formula arithmetic in X with the only free variables X and x, and assume that QB is a relation that satisfies If we define then we obviously have PB = IB.

The following is part of a series of papers on theories for (iterated) admissible sets (cf. [10], [11], [12], [14], [15]). Although these theories are weak subsystems of Zermelo-Fraenkel set theory, they allow one to formalize and prove a fair amount of definability theory and generalized recursion theory. Using this machinery it is in general not very hard to establish the connections between theories for admissible sets and (for example) systems of second order arithmetic. A proof-theoretic analysis of theories for admissible sets therefore provides quite a uniform and powerful framework for the proof-theoretic treatment of many systems of set theory, second order arithmetic and constructive mathematics (see [12] and [15]). The strongest result in this direction so far is the pair of proof-theoretic equivalences where T0 is Feferman's system for explicit mathematics of [5] and [6], ( -CA) + (BI) is the usual system of second order arithmetic with the axiom of -comprehension and bar induction and KPi is Kripke-Platek set theory with ∈-induction for arbitrary formulas and the additional axiom . The least standard model of KPi is L(i0) where i0 is the first recursively inaccessible ordinal. In this paper we are mainly interested in the theory KPi0 which results from KPi by severely restricting the principles of induction. Basically, complete induction on the natural numbers is allowed only for ∆0-formulas, and (IND∈) is omitted completely.

In [10] Friedman showed that ( -AC) is a conservative extension of ( -CA)<ε0for -sentences wherei= min(n+ 2, 4), i.e.,i= 2, 3, 4 forn= 0, 1, 2 +m. Feferman [5], [7] and Tait [11], [12] reobtained this result forn= 0, 1 and even with ( -DC) instead of ( -AC). Feferman and Sieg established in [9] the conservativeness of ( -DC) over ( -CA)<ε0for -sentences (ias above) for alln. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through languages with Skolem functionals. In this paper we study the same choice principles in the presence of theBar Rule(BR), which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result (Theorem 1 below) characterizes ( -DC) + (BR) as a conservative extension of a system of the autonomously iterated -comprehension axiom for -sentences (idepending onnas above). Forn= 0 this has been proved by Feferman in the form that ( -DC) + (BR) is a conservative extension of ( -CA)<Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger systemZω+μ+ (QF-AC) + (BR) and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below.