William W. Tait

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.