Systems of illative combinatory logic complete for first-order propositional and predicate calculus
Journal of Symbolic Logic 58 (3):769-788 (1993)
| Abstract | 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 [1932], [1933] and Curry [1930] 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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,664 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesKatalin 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.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads6 ( #145,498 of 549,013 )Recent downloads (6 months)1 ( #63,261 of 549,013 )How can I increase my downloads? |
My notes
Discussion
