Archive for Mathematical Logic 51 (5-6):475-501 (2012)

The article investigates a system of polymorphically typed combinatory logic which is equivalent to Gödel’s T. A notion of (strong) reduction is defined over terms of this system and it is proved that the class of well-formed terms is closed under both bracket abstraction and reduction. The main new result is that the number of contractions needed to reduce a term to normal form is computed by an ε 0-recursive function. The ordinal assignments used to obtain this result are also used to prove that the system under consideration is indeed equivalent to Gödel’s T. It is hoped that the methods used here can be extended so as to obtain similar results for stronger systems of polymorphically typed combinatory terms. An interesting corollary of such results is that they yield ordinally informative proofs of normalizability for sub-systems of second-order intuitionist logic, in natural deduction style.
Keywords Proof theory  Combinatory logic  Primitive recursive functionals  Gödel’s T  Ordinal analysis  Second-order logic
Categories (categorize this paper)
DOI 10.1007/s00153-012-0277-8
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: 54,740
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

Basic Proof Theory.A. S. Troelstra - 2000 - Cambridge University Press.
Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
Subrecursion: Functions and Hierarchies.H. E. Rose - 1984 - Oxford University Press.
Combinatory Logic, Volume I.Haskell B. Curry, Robert Feys & William Craig - 1959 - Philosophical Review 68 (4):548-550.

View all 9 references / Add more references

Citations of this work BETA

A Decidable Theory of Type Assignment.William R. Stirton - 2013 - Archive for Mathematical Logic 52 (5-6):631-658.

Add more citations

Similar books and articles

What Are Numbers?Zvonimir Šikić - 1996 - International Studies in the Philosophy of Science 10 (2):159-171.
Definedness.Solomon Feferman - 1995 - Erkenntnis 43 (3):295 - 320.
The Church-Rosser Property in Dual Combinatory Logic.Katalin Bimbó - 2003 - Journal of Symbolic Logic 68 (1):132-152.
A Model-Theoretic Approach to Ordinal Analysis.Jeremy Avigad & Richard Sommer - 1997 - Bulletin of Symbolic Logic 3 (1):17-52.
The Church-Rosser Property in Symmetric Combinatory Logic.Katalin Bimbó - 2005 - Journal of Symbolic Logic 70 (2):536 - 556.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.


Added to PP index

Total views
19 ( #527,141 of 2,386,875 )

Recent downloads (6 months)
6 ( #128,435 of 2,386,875 )

How can I increase my downloads?


My notes