The completeness of Heyting first-order logic
W. W. Tait · Journal of Symbolic Logic · 2003
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.