Mathematical Logic Quarterly 52 (3):237-252 (2006)

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
Keywords applicative theories  primitive recursion  Proof theory  type two functionals
Categories (categorize this paper)
DOI 10.1002/malq.200510029
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 51,480
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Definedness.Solomon Feferman - 1995 - Erkenntnis 43 (3):295 - 320.
Totality in Applicative Theories.Gerhard Jäger & Thomas Strahm - 1995 - Annals of Pure and Applied Logic 74 (2):105-120.
Polytime, Combinatory Logic and Positive Safe Induction.Cantini Andrea - 2002 - Archive for Mathematical Logic 41 (2):169-189.

View all 7 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

A Decidable Theory of Type Assignment.William R. Stirton - 2013 - Archive for Mathematical Logic 52 (5-6):631-658.
A Theory of Rules for Enumerated Classes of Functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Monotone Majorizable Functionals.Helmut Schwichtenberg - 1999 - Studia Logica 62 (2):283-289.
Equivalence of Bar Recursors in the Theory of Functionals of Finite Type.Marc Bezem - 1988 - Archive for Mathematical Logic 27 (2):149-160.
On Nested Simple Recursion.Ján Komara - 2011 - Archive for Mathematical Logic 50 (5-6):617-624.
Unary Primitive Recursive Functions.Daniel E. Severin - 2008 - Journal of Symbolic Logic 73 (4):1122-1138.


Added to PP index

Total views
14 ( #647,687 of 2,330,807 )

Recent downloads (6 months)
3 ( #256,394 of 2,330,807 )

How can I increase my downloads?


My notes