Journal of Symbolic Logic 58 (3):769-788 (1993)
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 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. The two direct translations turn out to be complete. The paper fulfills the program of Church ,  and Curry  to base logic on a consistent system of λ-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||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
Propositional and Predicate Calculuses Based on Combinatory Logic.M. W. Bunder - 1974 - Notre Dame Journal of Formal Logic 15 (1):25-34.
A Deduction Theorem for Restricted Generality.M. W. Bunder - 1973 - Notre Dame Journal of Formal Logic 14 (3):341-346.
Citations of this work BETA
1995 European Summer Meeting of the Association for Symbolic Logic.Johann A. Makowsky - 1997 - Bulletin of Symbolic Logic 3 (1):73-147.
Similar books and articles
The Church-Rosser Property in Dual Combinatory Logic.Katalin Bimbó - 2003 - Journal of Symbolic Logic 68 (1):132-152.
A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic.M. W. Bunder - 1983 - Journal of Symbolic Logic 48 (3):771-776.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
Introduction to Combinators and [Lambda]-Calculus.J. Roger Hindley - 1986 - Cambridge University Press.
Equivalences Between Pure Type Systems and Systems of Illative Combinatory Logic.M. W. Bunder & W. J. M. Dekkers - 2005 - Notre Dame Journal of Formal Logic 46 (2):181-205.
On the Equivalence of Systems of Rules and Systems of Axioms in Illative Combinatory Logic.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (3):603-608.
Investigation Into Combinatory Systems with Dual Combinators.Katalin Bimbó - 2000 - Studia Logica 66 (2):285-296.
Arithmetic Based on the Church Numerals in Illative Combinatory Logic.M. W. Bunder - 1988 - Studia Logica 47 (2):129 - 143.
Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Journal of Symbolic Logic 63 (3):869-890.
Added to index2009-01-28
Total downloads27 ( #185,357 of 2,153,472 )
Recent downloads (6 months)1 ( #399,080 of 2,153,472 )
How can I increase my downloads?