Social and Behavioral Sciences Commons^™

Completeness Of The Propositions-As-Types Interpretation Of Intuitionistic Logic Into Illative Combinatory Logic, Wil Dekkers, Martin Bunder, Henk Barendregt

Faculty of Engineering and Information Sciences - Papers: Part A

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, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic prepositional 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 …