This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

Constructive ZF + full separation is shown to be equiconsistent with Second Order Arithmetic.

The purpose of this article is to present a new theory for fixed points over arithmetic which allows the building up of fixed points in a very nested and entangled way. But in spite of its great expressive power we can show that the proof-theoretic strength of our theory—which is intensional in a meaning to be described below—is characterized by the Feferman–Schütte ordinal Γ0. Our approach is similar to the building up of fixed points over state spaces in the propositional (...) modal μ-calculus. (shrink)

This English translation of the author's original work has been thoroughly revised, expanded and updated. The book covers logical systems known as type-free or self-referential . These traditionally arise from any discussion on logical and semantical paradoxes. This particular volume, however, is not concerned with paradoxes but with the investigation of type-free sytems to show that: (i) there are rich theories of self-application, involving both operations and truth which can serve as foundations for property theory and formal semantics; (ii) these (...) theories provide a new outlook on classical topics, such as inductive definitions and predicative mathematics; (iii) they are particularly promising with regard to applications. Research arising from paradoxes has moved progressively closer to the mainstream of mathematical logic and has become much more prominent in the last twenty years. A number of significant developments, techniques and results have been discovered. Academics, students and researchers will find that the book contains a thorough overview of all relevant research in this field. (shrink)

The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκ where κ is a strongly inaccessible cardinal and Vκ denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the context in (...) which they are embedded. The context here will be the theory CZF− of constructive Zermelo–Fraenkel set theory but without -Induction . Let INAC be the statement that for every set there is an inaccessible set containing it. CZF−+INAC is a mathematically rich theory in which one can easily formalize Bishop style constructive mathematics and a great deal of category theory. CZF−+INAC also has a realizability interpretation in type theory which gives its theorems a direct computational meaning. The main result presented here is that the proof theoretic ordinal of CZF−+INAC is a small ordinal known as the Feferman–Schütte ordinal Γ0. (shrink)

Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories.

We prove here that the intuitionistic theory $T_{0}\upharpoonright + UMID_{N}$ , or even $EEJ\upharpoonright + UMID_{N}$ , of Explicit Mathematics has the strength of $\prod_{2}^{1} - CA_{0}$ . In Section I we give a double-negation translation for the classical second-order $\mu-calculus$ , which was shown in [ $M\ddot{o}02$ ] to have the strength of $\prod_{2}^{1}-CA_{0}$ . In Section 2 we interpret the intuitionistic $\mu-calculus$ in the theory $EETJ\upharpoonright + UMID_{N}$ . The question about the strength of monotone inductive definitions in (...) $T_{0}$ was asked by S. Feferman in 1982, and - assuming classical logic - was addressed by M. Rathjen. (shrink)

We study the extension of Feferman’s operational set theory provided by adding operational versions of unbounded existential quantification and power set and determine its proof-theoretic strength in terms of a suitable theory of sets and classes.

We investigate a theory of Frege structures extended by the Myhill-Flagg hierarchy of implications. We study its relation to a property theory with an approximation operator and we give a proof theoretical analysis of the basic system involved. MSC: 03F35, 03D60.

We introduce an operational set theory in the style of [5] and [16]. The theory we develop here is a theory of constructive sets and operations. One motivation behind constructive operational set theory is to merge a constructive notion of set ([1], [2]) with some aspects which are typical of explicit mathematics [14]. In particular, one has non-extensional operations (or rules) alongside extensional constructive sets. Operations are in general partial and a limited form of self{application is permitted. The system we (...) introduce here is a fully explicit, nitely axiomatised system of constructive sets and operations, which is shown to be as strong as HA. (shrink)