The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of these new cut (...) elimination techniques to attain an ordinal analysis of П12 comprehension by approaching П12 comprehension through transfinite levels of reflection. (shrink)

In the first part we show why ordinals and ordinal notations are naturally connected with proof theoretical research. We introduce the program of ordinal analysis. The second part gives examples of applications of ordinal analysis.

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical (...) point of view. (shrink)

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and I (...) apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions. (shrink)

We study and some of its most important extensions primarily from a proof-theoretic perspective, determine their consistency strengths by exhibiting equivalent systems in the realm of traditional set theory and introduce a new and interesting extension of which is conservative over.

It is shown how the strong ordinal notation systems that figure in proof theory and have been previously defined by employing large cardinals, can be developed directly on the basis of their recursively large counterparts. Thereby we provide a completely new approach to well-ordering proofs as will be exemplified by determining the proof-theoretic ordinal of the systemKPM of [R91].