Systems of explicit mathematics provide an axiomatic framework for representing programs and proving properties of them. We introduce such a system with a new form of power types using a monotone power type generator. These power types allow us to model impredicative overloading. This is a very general form of type dependent computation which occurs in the study of object-oriented programming languages. We also present a set-theoretic interpretation for monotone power types. Thus establishing the consistency our system of explicit mathematics.

This paper deals with the proof theory of first-order applicative theories with non-constructive μ operator and a form of the bar rule, yielding systems of ordinal strength Γ0 and 20, respectively. Relevant use is made of fixed-point theories with ordinals plus bar rule.

In this paper we study (self)-applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on W = {0, 1} * are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.

This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the two subsystems of (...) second order arithmetic, Π10-CA and Π11-CA, respectively. (shrink)

In this chapter, I consider some problems with naturalizing mathematics. More specifically, I consider how the two leading kinds of approach to naturalizing mathematics, to wit, Quinean indispensability‐based approaches and Maddy's Second Philosophical approach, seem to run afoul of constraints that any satisfactory naturalistic mathematics must meet. I then suggest that the failure of these kinds of approach to meet the relevant constraints indicates a general problem with naturalistic mathematics meeting these constraints, and thus with the project of naturalizing mathematics (...) itself. (shrink)

In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories.

In this paper we summarize some results about sets in Frege structures. The resulting set theory is discussed with respect to its historical and philosophical significance. This includes the treatment of diagonalization in the presence of a universal set.

We give a survey on truth theories for applicative theories. It comprises Frege structures, universes for Frege structures, and a theory of supervaluation. We present the proof-theoretic results for these theories and show their syntactical expressive power. In particular, we present as a novelty a syntactical interpretation of ID1 in a applicative truth theory based on supervaluation.

This paper deals with: (i) the theory ID # 1 which results from $\widehat{\mathrm{ID}}_1$ 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.

In this paper we study applicative theories of operations and numbers with the non-constructive minimum operator in the context of a total application operation. We determine the proof-theoretic strength of such theories by relating them to well-known systems like Peano Arithmetic PA and the system <0 of second order arithmetic. Essential use will be made of so-called fixed-point theories with ordinals, certain infinitary term models and Church-Rosser properties.

The Suslin operator is a type-2 functional testing for the well-foundedness of binary relations on the natural numbers. In the context of applicative theories, its proof-theoretic strength has been analyzed in Jäger and Strahm [18]. This article provides a more direct approach to the computation of the upper bounds in question. Several theories featuring the Suslin operator are embedded into ordinal theories tailored for dealing with non-monotone inductive definitions that enable a smooth definition of the application relation.

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.

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.

The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for 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 is proof-theoretically equivalent to Peano arithmetic PA <0).

The unfolding of schematic formal systems is a novel concept which was initiated in Feferman , Gödel ’96, Lecture Notes in Logic, Springer, Berlin, 1996, pp. 3–22). This paper is mainly concerned with the proof-theoretic analysis of various unfolding systems for non-finitist arithmetic . In particular, we examine two restricted unfoldings and , as well as a full unfolding, . The principal results then state: is equivalent to ; is equivalent to ; is equivalent to . Thus is proof-theoretically equivalent (...) to predicative analysis. (shrink)