Abstract.This paper is the first in a series of three which culminates in an ordinal analysis of Π12-comprehension. On the set-theoretic side Π12-comprehension corresponds to Kripke-Platek set theory, KP, plus Σ1-separation. The strength of the latter theory is encapsulated in the fact that it proves the existence of ordinals π such that, for all β>π, π is β-stable, i.e. Lπ is a Σ1-elementary substructure of Lβ. The objective of this paper is to give an ordinal analysis of a scenario of (...) not too complicated stability relations as experience has shown that the understanding of the ordinal analysis of Π12-comprehension is greatly facilitated by explicating certain simpler cases first.This paper introduces an ordinal representation system based on ν-indescribable cardinals which is then employed for determining an upper bound for the proof–theoretic strength of the theory KPi+ ∀ρ ∃ππ is π+ρ-stable, where KPi is KP augmented by the axiom saying that every set is contained in an admissible set. (shrink)

Part of the ambiguity lies in the various points of view from which this question might be considered. The crudest di erence lies between the point of view of the working mathematician and that of the logician concerned with the foundations of mathematics. Now some of my fellow mathematical logicians might protest this distinction, since they consider themselves to be just more of those \working mathematicians". Certainly, modern logic has established itself as a very respectable branch of mathematics, and there (...) are quite a few highly technical journals in logic, such as The Journal of Sym-. (shrink)

In this paper we introduce a notation system for the infinitary derivations occurring in the ordinal analysis of KP + Π₃-Reflection due to Michael Rathjen. This allows a finitary ordinal analysis of KP + Π₃-Reflection. The method used is an extension of techniques developed by Wilfried Buchholz, namely operator controlled notation systems for RS∞-derivations. Similarly to Buchholz we obtain a characterisation of the provably recursive functions of KP + Π₃-Reflection as <-recursive functions where < is the ordering on Rathjen's ordinal (...) notation system J(K). Further we show a conservation result for $\Pi _{2}^{0}$-sentences. (shrink)

The paper relativizes the method of ordinal analysis developed for Kripke–Platek set theory to theories which have the power set axiom. We show that it is possible to use this technique to extract information about Power Kripke–Platek set theory, KP.As an application it is shown that whenever KP+AC proves a ΠP2 statement then it holds true in the segment Vτ of the von Neumann hierarchy, where τ stands for the Bachmann–Howard ordinal.

The technique of using infinitary rules in an ordinal analysis has been one of the most productive developments in ordinal analysis. Unfortunately, one of the most advanced variants, the Buchholz Ωμ rule, does not apply to systems much stronger than -comprehension. In this paper, we propose a new extension of the Ω rule using game-theoretic quantifiers. We apply this to a system of inductive definitions with at least the strength of a recursively inaccessible ordinal.

This paper gives a formalization of general topology in second-order arithmetic using countably based MF spaces. This formalization is used to study the reverse mathematics of general topology. For each poset P we let MF denote the set of maximal filters on P endowed with the topology generated by {Np | p ∈ P}, where Np = {F ∈ MF | p ∈ F}. We define a countably based MF space to be a space of the form MF for some (...) countable poset P. The class of countably based MF spaces includes all complete separable metric spaces as well as many nonmetrizable spaces. The following reverse mathematics results are obtained. The proposition that every nonempty Gδ subset of a countably based MF space is homeomorphic to a countably based MF space is equivalent to [Formula: see text] over ACA0. The proposition that every uncountable closed subset of a countably based MF space contains a perfect set is equivalent over [Formula: see text] to the proposition that [Formula: see text] is countable for all A ⊆ ℕ. The proposition that every regular countably based MF space is homeomorphic to a complete separable metric space is equivalent to [Formula: see text] over [Formula: see text]. (shrink)

We will study patterns which occur when considering how Σ1-elementary substructures arise within hierarchies of structures. The order in which such patterns evolve will be seen to be independent of the hierarchy of structures provided the hierarchy satisfies some mild conditions. These patterns form the lowest level of what we call patterns of resemblance. They were originally used by the author to verify a conjecture of W. Reinhardt concerning epistemic theories 449–460; Ann. Pure Appl. Logic, to appear), but their relationship (...) to axioms of infinity and usefulness for ordinal analysis were manifest from the beginning. This paper is the first part of a series which provides an introduction to an extensive program including the ordinal analysis of set theories. Future papers will conclude the introduction and establish, among other things, that notations we will derive from the patterns considered here represent the proof-theoretic ordinal of the theory KPℓ0 or, equivalently, Π11−CA0. (shrink)

This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality and renormalization issues (...) in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

The \-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \ using a variant of the cut-elimination formalism introduced by Mints.

Sections 1 through 4 define, in the usual inductive style, various classes of object including one which is called the “combinatory terms of polymorphic type”. Section 5 defines a reduction relation on these terms. Section 6 shows that the weak normalizability of the combinatory terms of polymorphic type entails the weak normalizability of the lambda terms of polymorphic type. The entailment is not vacuous, because the combinatory terms of polymorphic type are indeed weakly normalizable, as is proven in Sect. 7 (...) using Tait and Girard’s computability predicates. The remainder of the paper is devoted to arguing that interesting consequences would follow from the existence of an “ordinally informative” proof, i.e. one which uses transfinite induction over recursive ordinal numbers and otherwise finitary methods, of normalizability for as large a class of the terms as possible. (shrink)

We will study patterns which occur when considering how Σ 1 -elementary substructures arise within hierarchies of structures. The order in which such patterns evolve will be seen to be independent of the hierarchy of structures provided the hierarchy satisfies some mild conditions. These patterns form the lowest level of what we call patterns of resemblance . They were originally used by the author to verify a conjecture of W. Reinhardt concerning epistemic theories 449–460; Ann. Pure Appl. Logic, to appear), (...) but their relationship to axioms of infinity and usefulness for ordinal analysis were manifest from the beginning. This paper is the first part of a series which provides an introduction to an extensive program including the ordinal analysis of set theories. Future papers will conclude the introduction and establish, among other things, that notations we will derive from the patterns considered here represent the proof-theoretic ordinal of the theory KPℓ 0 or, equivalently, Π 1 1 −CA 0. (shrink)