Article contents
The system CΔ of combinatory logic1
Published online by Cambridge University Press: 12 March 2014
Extract
The system of combinatory logic to be presented in this paper will be called CΔ. It may be compared to various systems of combinatory logic constructed by Schonfinkel [11], Curry [1], Rosser [10], and Curry and Feys [2], and to the author's systems K′ [3] and S [5], and to extensional modifications of K′ [6], [7], [8], [9]. The present system falls within this latter category of extensional or semi-extensional systems, but it is more perspicuous than the others, and the proof of its consistency is more direct. It contains the theory of combinators in full strength. It also contains operators for disjunction, conjunction, negation, existence (that is, non-emptiness), and universality. A considerable part of classical mathematical analysis can be shown to be derivable in CΔ, just as in K′ [4], but with the added advantage of the availability of a limited extensionality principle.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1964
Footnotes
This paper reports one aspect of a more general research program supported by the Office of Naval Research, Group Psychology Branch, Contract No. SAR/Nonr-609(16). Permission is granted for reproduction, translation, publication, and disposal in whole or in part by or for the U.S. Government. The Association for Symbolic Logic retains copyright authority for all other uses. The writer wishes to express his indebtedness to Professor Haskell B. Curry for some helpful criticisms and suggestions.
References
- 14
- Cited by