David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
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)|
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
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Katalin Bimbó (2003). The Church-Rosser Property in Dual Combinatory Logic. Journal of Symbolic Logic 68 (1):132-152.
M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.
Sabine Broda & Luís Damas (1997). Compact Bracket Abstraction in Combinatory Logic. Journal of Symbolic Logic 62 (3):729-740.
J. Roger Hindley (1986). Introduction to Combinators and [Lambda]-Calculus. Cambridge University Press.
M. W. Bunder & W. J. M. Dekkers (2005). Equivalences Between Pure Type Systems and Systems of Illative Combinatory Logic. Notre Dame Journal of Formal Logic 46 (2):181-205.
M. W. Bunder (1979). On the Equivalence of Systems of Rules and Systems of Axioms in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):603-608.
Katalin Bombó (2005). The Church-Rosser Property in Symmetric Combinatory Logic. Journal of Symbolic Logic 70 (2):536 - 556.
Katalin Bimbó (2000). Investigation Into Combinatory Systems with Dual Combinators. Studia Logica 66 (2):285-296.
M. W. Bunder (1988). Arithmetic Based on the Church Numerals in Illative Combinatory Logic. Studia Logica 47 (2):129 - 143.
Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. Journal of Symbolic Logic 63 (3):869-890.
Added to index2009-01-28
Total downloads25 ( #149,989 of 1,792,082 )
Recent downloads (6 months)7 ( #119,870 of 1,792,082 )
How can I increase my downloads?