Journal of Symbolic Logic 68 (3):751-763 (2003)

William W. Tait
University of Chicago
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 firstorderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting’s system.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1058448436
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 60,795
Through your library

References found in this work BETA

The Law of Excluded Middle and the Axiom of Choice.W. W. Tait - 1994 - In Alexander George (ed.), Mathematics and Mind. Oxford University Press. pp. 45--70.
Intensional Interpretations of Functionals of Finite Type I.W. W. Tait - 1975 - Journal of Symbolic Logic 40 (4):624-625.

Add more references

Citations of this work BETA

Godel's Interpretation of Intuitionism.William Tait - 2006 - Philosophia Mathematica 14 (2):208-228.

Add more citations

Similar books and articles


Added to PP index

Total views
142 ( #72,159 of 2,438,766 )

Recent downloads (6 months)
2 ( #283,612 of 2,438,766 )

How can I increase my downloads?


My notes