The completeness of Heyting first-order logic
Tait, W. W.
J. Symbolic Logic, Tome 68 (2003) no. 1, p. 751- 763 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
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.
Publié le : 2003-09-14
Classification:  
@article{1058448436,
     author = {Tait, W. W.},
     title = {The completeness of Heyting first-order logic},
     journal = {J. Symbolic Logic},
     volume = {68},
     number = {1},
     year = {2003},
     pages = { 751- 763},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1058448436}
}

Tait, W. W. The completeness of Heyting first-order logic. J. Symbolic Logic, Tome 68 (2003) no. 1, pp.  751- 763. http://gdmltest.u-ga.fr/item/1058448436/