Hostname: page-component-77c89778f8-sh8wx Total loading time: 0 Render date: 2024-07-21T12:41:38.477Z Has data issue: false hasContentIssue false
  • English
  • Français

Systems of illative combinatory logic complete for first-order propositional and predicate calculus

Published online by Cambridge University Press:  12 March 2014

Henk Barendregt ,
Martin Bunder  and
Wil Dekkers
Henk Barendregt
Affiliation:
Faculty of Mathematics and Computer Science, Catholic University, Nijmegen, The Netherlands, E-mail: [email protected]
Martin Bunder
Affiliation:
Faculty of Informatics, Department of Mathematics, University of Wollongong, NSW Australia, E-mail: [email protected]
Wil Dekkers
Affiliation:
Faculty of Mathematics and Computer Science, Catholic University, Nijmegen, The Netherlands, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. 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. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 3 , September 1993 , pp. 769 - 788
Copyright
Copyright © Association for Symbolic Logic 1993

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Aczel, P. [1980], Frege structures and the notions of proposition, truth and set, The Kleene symposium (Barwise, J., Keisler, H. J., and Kunen, K., editors), North-Holland, Amsterdam, pp. 31–59.CrossRefGoogle Scholar
Barendregt, H. P. [1984], The lambda calculus, its syntax and semantics, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam.Google Scholar
Barendregt, H. P. [1992], Lambda calculi with types, Handbook of logic in computer science, Vol. II (Abramski, S., Gabbay, D. M., and Maibaum, T. S. E., editors), Oxford University Press, London and New York.Google Scholar
Barendsen, E. [1989], Representation of logic, data types and recursive functions in typed lambda calculi, Masters Thesis, Department of Computer Science, Catholic University, Nijmegen.Google Scholar
Bunder, M. W. [1969], Set theory based on combinatory logic, Ph.D. thesis, Department of Mathematics, University of Amsterdam.Google Scholar
Bunder, M. W. [1973], A deduction theorem for restricted generality, Notre Dame Journal of Formal Logic, vol. 14, pp. 341–346.CrossRefGoogle Scholar
Bunder, M. W. [1974], Propositional and predicate calculus based on combinatory logic, Notre Dame Journal of Formal Logic, vol. 15, pp. 25–32.CrossRefGoogle Scholar
Bunder, M. W. [1976], The inconsistency of , this Journal, vol. 41, pp. 467–468.Google Scholar
Bunder, M. W. [1983], Predicate calculus of arbitrarily high finite order, Archiv für Math Logik und Grundlagenforschung, vol. 23, pp. 1–10.CrossRefGoogle Scholar
Bunder, M. W. [1983a], A one axiom set theory based on higher order predicate calculus, Archiv für Math Logik und Grundlagenforschung, vol. 23, pp. 99–107.CrossRefGoogle Scholar
Bunder, M. W. [1983b], A weak absolute consistency proof for some systems of illative combinatory logic, this Journal, vol. 48, pp. 771–776.Google Scholar
Church, A. [1932, 1933], A set of postulates for the foundation of logic, Annals of Mathematics (2), vol. 33, pp. 346–366 and vol. 34, pp. 839–864.CrossRefGoogle Scholar
Church, A. [1941], The calculi of lambda conversion, Princeton University Press, Princeton.Google Scholar
Curry, H. B. [1930], Grundlagen der kombinatorischen Logik, American Journal of Mathematics, vol. 52, pp. 509–536; pp. 789–834. (Inaugural dissertation)CrossRefGoogle Scholar
Curry, H. B. [1931], The universal quantifier in combinatory logic, Annals of Mathematics, vol. 32, pp. 154–180.CrossRefGoogle Scholar
Curry, H. B. [1932], Some additions to the theory of combinators, American Journal of Mathematics, vol. 54, pp. 551–558.CrossRefGoogle Scholar
Curry, H. B. [1933], Apparent variables from the standpoint of combinatory logic, Annals of Mathematics, vol. 34, pp. 381–404.CrossRefGoogle Scholar
Curry, H. B. [1934a], Functionality in combinatory logic, Proceedings of the National Academy of Sciences of the United States of America, vol. 20, pp. 584–590.CrossRefGoogle ScholarPubMed
Curry, H. B. [1934b], Some properties of equality and implication in combinatory logic, Annals of Mathematics, vol. 35, pp. 849–850.CrossRefGoogle Scholar
Curry, H. B. [1935], Foundations of the theory of abstract sets from the standpoint of combinatory logic, Bulletin of the American Mathematical Society, vol. 40, p. 654. (Abstract).Google Scholar
Curry, H. B. [1936], First properties of functionality in combinatory logic, Tôhoku Mathematical Journal, vol. 41, pp. 371–401.Google Scholar
Curry, H. B. [1942a], Some advances in the combinatory theory of quantification, Proceedings of the National Academy of Sciences of the United States of America, vol. 28, pp. 564–569.CrossRefGoogle ScholarPubMed
Curry, H. B. [1942b], The combinatory foundations of mathematical logic, this Journal, vol. 7, pp. 49–64.Google Scholar
Curry, H. B. [1942c], The inconsistency of certain formal logics, this Journal, vol. 7, pp. 115–117.Google Scholar
Curry, H. B. and Feys, R. [1958], Combinatory logic, Vol. 1, North-Holland, Amsterdam.Google Scholar
Curry, H. B., Hindley, J. R. and Seldin, J. P. [1972], Combinatory logic, Vol. 2, North-Holland, Amsterdam.Google Scholar
Hindley, J. R. and Seldin, J. P. [1986], Introduction to combinators and λ-calculus, Cambridge University Press, London and New York.Google Scholar
Kleene, S. and Rosser, J. B. [1935], The inconsistency of certain formal logics, Annals of Mathematics (2), vol. 36, pp. 630–636.CrossRefGoogle Scholar
Löb, M. [1955], A solution of a problem of Henkin, this Journal, vol. 20, pp. 115–118.Google Scholar
Mostowski, A. [1951], On the rules of proof in the pure functional calculus of first order, this Journal, vol. 16, pp. 107–111.Google Scholar
Peremans, W. [1949], Een opmerking over intuitionistische logica, Report ZW-16, CWI, Kruislaan 413, 1098 SJ Amsterdam.Google Scholar