×

Glivenko and Kuroda for simple type theory. (English) Zbl 1337.03015

Summary: Glivenko’s theorem states that an arbitrary propositional formula is classically provable if and only if its double negation is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order predicate logic without the universal quantifier. A recent paper by K. Zdanowski [J. Symb. Log. 74, No. 1, 157–167 (2009; Zbl 1163.03010)] shows that Glivenko’s theorem also holds for second-order propositional logic without the universal quantifier. We prove that Glivenko’s theorem extends to some versions of simple type theory without the universal quantifier. Moreover, we prove that Kuroda’s negative translation, which is known to embed classical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included.

MSC:

03B15 Higher-order logic; type theory (MSC2010)
03B20 Subsystems of classical logic (including intuitionistic logic)

Citations:

Zbl 1163.03010

Software:

ETPS
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] A formulation of the simple theory of types 5 pp 56– (1940)
[2] Higher-order semantics and extensionality 69 pp 1027– (2004)
[3] On second order intuitionistic propositional logic without a universal quantifier 74 pp 157– (2009) · Zbl 1163.03010
[4] An introduction to mathematical logic and type theory: To truth through proof (2002) · Zbl 1002.03002
[5] DOI: 10.1016/j.apal.2010.04.009 · Zbl 1225.03034 · doi:10.1016/j.apal.2010.04.009
[6] Resolution in type theory 36 pp 414– (1971) · Zbl 0231.02038
[7] On various negative translations, Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21–22 August 2010 47 pp 21– (2010)
[8] Nagoya Mathematical Journal 2 pp 35– (1951) · Zbl 0042.00606 · doi:10.1017/S0027763000010023
[9] O principe tertium non datur. Matematiceskij Sbornik 32 pp 646– (1925)
[10] Zur intuitionistischen arithmetik und zahlentheorie. Ergebnisse eines mathematischen Kolloquiums 4 pp 34– (1933)
[11] Sur quelques points de la logique de M. Brouwer. Bulletins de la classe des sciences 15 pp 183– (1929)
[12] Über das verhältnis zwischen intuitionistischer und klassischer arithmetik. Archiv für mathematische Logik und Grundlagenforschung 16 pp 119– (1974)
[13] Intuitionistic logic, model theory and forcing (1969)
[14] Introduction to higher order categorical logic (1986) · Zbl 0596.03002
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.