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.

We characterize the polynomial time operations as those which are provably total in a first order system, which comprises (untyped) combinatory logic with extensionality, together with positive “safe induction” on the set of binary strings. The formalization of safe induction is inspired by Leivants idea of ramification. We also show how to replace ramification by means of modal logic.

Let ≺ be a primitive recursive well-ordering on the natural numbers and assume that its order-type is greater than or equal to the proof-theoretic ordinal of the theory T. We show that the proof-theoretic strength of T is not increased if we add the negation of the statement which formalizes transfinite induction along ≺.

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)

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.