Journal of Symbolic Logic 58 (3):769-788 (1993)
AbstractIllative 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)
Similar books and articles
The Church-Rosser Property in Dual Combinatory Logic.Katalin Bimbó - 2003 - Journal of Symbolic Logic 68 (1):132-152.
Arithmetic Based on the Church Numerals in Illative Combinatory Logic.M. W. Bunder - 1988 - Studia Logica 47 (2):129 - 143.
Investigation Into Combinatory Systems with Dual Combinators.Katalin Bimbó - 2000 - Studia Logica 66 (2):285-296.
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.
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.
Introduction to Combinators and (Lambda) Calculus.J. Roger Hindley - 1986 - Cambridge University Press.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic.M. W. Bunder - 1983 - Journal of Symbolic Logic 48 (3):771-776.
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 PP
Historical graph of downloads
Citations of this work
The Impact of the Lambda Calculus in Logic and Computer Science.Henk Barendregt - 1997 - Bulletin of Symbolic Logic 3 (2):181-215.
Typed Lambda Calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 1091--1132.
Completeness of Two Systems of Illative Combinatory Logic for First-Order Propositional and Predicate Calculus.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Archive for Mathematical Logic 37 (5-6):327-341.
Circular Languages.Hannes Leitgeb & Alexander Hieke - 2004 - Journal of Logic, Language and Information 13 (3):341-371.
1995 European Summer Meeting of the Association for Symbolic Logic.Johann A. Makowsky - 1997 - Bulletin of Symbolic Logic 3 (1):73-147.
References found in this work
The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
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.
Introduction to Combinators and Λ-Calculus.J. Roger Hindley & Jonathan P. Seldin - 1988 - Journal of Symbolic Logic 53 (3):985-986.