Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic
Journal of Symbolic Logic 63 (3):869-890 (1998)
|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. In a preceding paper, , we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. 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 the cited paper we proved completeness of the two direct translations. In the present paper we prove that also the two indirect translations are complete. These proofs are direct whereas in another version, , we proved completeness by showing that the two corresponding illative systems are conservative over the two systems for the direct translations. Moreover we shall prove that one of the systems is also complete for predicate calculus with higher type functions|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Henk Barendregt, Martin Bunder & Wil Dekkers (1993). Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus. Journal of Symbolic Logic 58 (3):769-788.
M. W. Bunder (1979). $\Lambda$-Elimination in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):628-630.
Linda Postniece, Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.
Katalin Bombó (2005). The Church-Rosser Property in Symmetric Combinatory Logic. Journal of Symbolic Logic 70 (2):536 - 556.
M. W. Bunder (1982). Illative Combinatory Logic Without Equality as a Primitive Predicate. Notre Dame Journal of Formal Logic 23 (1):62-70.
M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.
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.
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 (1988). Arithmetic Based on the Church Numerals in Illative Combinatory Logic. Studia Logica 47 (2):129 - 143.
Martin Bunder & Wil Dekkers (2001). Pure Type Systems with More Liberal Rules. Journal of Symbolic Logic 66 (4):1561-1580.
Added to index2009-01-28
Total downloads7 ( #142,359 of 722,932 )
Recent downloads (6 months)1 ( #61,087 of 722,932 )
How can I increase my downloads?