Tait’s conservative extension theorem revisited. (English) Zbl 1190.03015

In “The completeness of Heyting first-order logic” [J. Symb. Log. 68, No. 3, 751–763 (2003; Zbl 1055.03036)], W. W. Tait claims the conservativeness of CH over HL. Here, CH is the Tait version of Curry-Howard construction theory and HL is Heyting (i.e. intuitionistic) logic. In this paper, the author points out that Tait’s proof of the main theorem [Theorem 5.1] is defective, and hence the conservativeness above, which is its corollary, is not yet proved. Even worse, by providing a counter-example, he shows that Theorem 5.1 is just plain wrong. However, the author amends Tait’s proof, shows the CH/HL conservativeness, and presents a modified version of Theorem 5.1. He exhibits a few examples which are totally lacking in Tait’s article, but repeats definitions and explains again mechanisms and meanings of various notions.
In item [1] of the references, p. 167, “pp. 221–224” should be “pp. 127–172”.


03B20 Subsystems of classical logic (including intuitionistic logic)
03F25 Relative consistency and interpretations
03F65 Other constructive mathematics


Zbl 1055.03036
Full Text: DOI


[1] The provenance of pure reason: Essays in the philosophy of mathematics and its history (2005) · Zbl 1111.00006
[2] The completeness of Hey ting first-order logic 68 pp 751– (2003)
[3] Twenty-five years of constructive type theory pp 221– (1998)
[4] DOI: 10.1007/BF00413978
[5] Journal of Philosophical Logic 12 pp 173– (1983)
[6] Mathematics and mind pp 45– (1994) · Zbl 0834.00012
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.