caa a22 4500 388039817 CHVBK 20180307125018.0 cr unu---uuuuu 161130e199809 xx s 000 0 eng 10.2307/2586717 doi S002248120001464X pii (NATIONALLICENCE)cambridge-10.2307/2586717 Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic [Elektronische Daten] 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 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, [3], 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. Copyright © Association for Symbolic Logic 1998 Dekkers Wil Faculty of Mathematics and Computer Science, Catholic University, Nijmegen, The Netherlands E-mail: wil@cs.kun.nl Bunder Martin Faculty of Informatics, Department of Mathematics, University of Wollonoong, Nsw Australia E-mail: martin_bunder@uow.edu.au Barendregt Henk Faculty of Mathematics and Computer Science, Catholic University, Nijmegen, The Netherlands E-mail: henk@cs.kun.nl The Journal of Symbolic Logic Cambridge University Press 63/3(1998-09), 869-890 0022-4812 63:3<869 1998 63 JSL https://doi.org/10.2307/2586717 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.2307/2586717 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Dekkers Wil Faculty of Mathematics and Computer Science, Catholic University, Nijmegen, The Netherlands E-mail: wil@cs.kun.nl NATIONALLICENCE 700 1- Bunder Martin Faculty of Informatics, Department of Mathematics, University of Wollonoong, Nsw Australia E-mail: martin_bunder@uow.edu.au NATIONALLICENCE 700 1- Barendregt Henk Faculty of Mathematics and Computer Science, Catholic University, Nijmegen, The Netherlands E-mail: henk@cs.kun.nl NATIONALLICENCE 773 0- The Journal of Symbolic Logic Cambridge University Press 63/3(1998-09), 869-890 0022-4812 63:3<869 1998 63 JSL CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-cambridge