University of Wollongong
Browse

Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic

Download (411.3 kB)
journal contribution
posted on 2024-11-14, 01:53 authored by Wil Dekkers, Martin BunderMartin Bunder, Henk Barendregt
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 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.

History

Citation

Dekkers, W., Bunder, M. & Barendregt, H. (1998). Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic. The Journal of Symbolic Logic, 63 (3), 869-890.

Journal title

Journal of Symbolic Logic

Volume

63

Issue

3

Pagination

869-890

Language

English

RIS ID

87047

Usage metrics

    Categories

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC