Feferman, S. and G. Jäger, Systems of explicit mathematics with non-constructive μ-operator. Part I, Annals of Pure and Applied Logic 65 243-263. This paper is mainly concerned with the proof-theoretic analysis of systems of explicit mathematics with a non-constructive minimum operator. We start off from a basic theory BON of operators and numbers and add some principles of set and formula induction on the natural numbers as well as axioms for μ. The principal results then state: BON plus set induction (...) is proof-theoretically equivalent to Peano arithmetic PA; BON plus formula induction is proof-theoretically equivalent to the system <0 of second-order arithmetic. (shrink)

The present volume is intended as an all-round introduction to constructivism. Here constructivism is to be understood in the wide sense, and covers in particular Brouwer's intuitionism, Bishop's constructivism and A.A. Markov's constructive recursive mathematics. The ending "-ism" has ideological overtones: "constructive mathematics is the (only) right mathematics"; we hasten, however, to declare that we do not subscribe to this ideology, and that we do not intend to present our material on such a basis.

This paper is concerned with the determination of the proof-strength of the power set axiom relative to axiom systems for Feferman's explicit mathematics. As conjectured by Feferman, we obtain that the presence of the power set axiom does not increase proof-strength. Results are achieved by reducing the systems including the power set axiom to subsystems of classical analysis. In those cases where only the induction axiom is available, we make use of the technique of asymmetrical interpretations.

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.

The aim of this paper is to introduce a formal system STW of self-referential truth, which extends the classical first-order theory of pure combinators with a truth predicate and certain approximation axioms. STW naturally embodies the mechanisms of general predicate application/abstraction on a par with function application/abstraction; in addition, it allows non-trivial constructions, inspired by generalized recursion theory. As a consequence, STW provides a smooth inner model for Myhill's systems with levels of implication.

We show that the untyped λ -calculus can be extended with Frege's interpretation of propositional notions, provided we restrict β -conversion to positive expressions. The system of illative λ -calculus so obtained admits a natural Scott-style semantics.

In this note it is shown that in explicit mathematics the strong power type axiom is inconsistent with (uniform) elementary comprehension and discuss some general aspects of power types in explicit mathematics.

We study elementary second order extensions of the theoryID 1 of non-iterated inductive definitions and the theoryPA Ω of Peano arithmetic with ordinals. We determine the exact proof-theoretic strength of those extensions and their natural subsystems, and we relate them to subsystems of analysis with arithmetic comprehension plusΠ 1 1 comprehension and bar induction without set parameters.

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).

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)