Archive for Mathematical Logic 37 (5-6):327-341 (1998)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of $\lambda$ -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent)
Keywords Legacy
Categories (categorize this paper)
DOI 10.1007/s001530050102
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: 71,464
Through your library

References found in this work BETA

Add more references

Citations of this work BETA

Higher-Order Illative Combinatory Logic.Łukasz Czajka - 2013 - Journal of Symbolic Logic 78 (3):837-872.
Pure Type Systems with More Liberal Rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.

Add more citations

Similar books and articles

Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
Pure Type Systems with More Liberal Rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
The Church-Rosser Property in Symmetric Combinatory Logic.Katalin Bimbó - 2005 - Journal of Symbolic Logic 70 (2):536 - 556.
An Approach to Infinitary Temporal Proof Theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.


Added to PP index

Total views
32 ( #359,102 of 2,520,787 )

Recent downloads (6 months)
1 ( #405,623 of 2,520,787 )

How can I increase my downloads?


My notes