Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-27T11:28:31.463Z Has data issue: false hasContentIssue false
  • English
  • Français

The completeness of Heyting first-order logic

Published online by Cambridge University Press:  12 March 2014

W. W. Tait
W. W. Tait*
Affiliation:
5522 S. Everett Ave., Chicago, IL 60637, USA, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Restricted to first-order formulas, the rules of inference in the Curry-Howard type theory are equivalent to those of first-order predicate logic as formalized by Heyting, with one exception: ∃-elimination in the Curry-Howard theory, where ∃x: A,F(x) is understood as disjoint union, are the projections, and these do not preserve first-orderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting's system.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 68 , Issue 3 , September 2003 , pp. 751 - 763
Copyright
Copyright © Association for Symbolic Logic 2003

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

[1] Hindley, J. and Sheldon, J. (editors), To H.B. Curry: Essays on Combinatorial Logic, Lambda Calculus and Formalism, Academic Press, London, 1980.Google Scholar
[2] Howard, W., The formula as-types notion of construction, In Hindley, and Sheldon, [1], pp. 479–490.Google Scholar
[3] Martin-Löf, P., An intuitionistic theory of types, In Sambin, and Smith, [4], pp. 221–244.Google Scholar
[4] Sambin, G. and Smith, J. (editors), Twenty five years of constructive type theory, Oxford University Press, Oxford, 1998.Google Scholar
[5] Tait, W., A second order theory of functional of higher type, with two appendices. Appendix A: Intensional functional. Appendix B: An interpretation of functional by convertible terms, Stanford Seminar Report 1963, pp. 171–206. A published version is [6].Google Scholar
[6] Tait, W., Intensional interpretations of functional offinite type I, this Journal, vol. 32 (1967), pp. 198–212.Google Scholar
[7] Tait, W., The law of excluded middle and the axiom of choice, Mathematics and Mind (George, A., editor), Oxford University Press, Oxford, 1994, pp. 45–70.CrossRefGoogle Scholar