×

A short proof of Glivenko theorems for intermediate predicate logics. (English) Zbl 1316.03015

This short paper deals with Glivenko-type theorems for intermediate logics, which are, among other things, shown to follow from the deduction theorem. In the terminology adopted by the author, the original Glivenko theorem shows that the Glivenko theorem holds for (propositional) classical logic over intuitionistic logic (IL). So the paper contains a short proof that for any set \(S\) of sentences, valid in classical logic, the Glivenko theorem holds for (a) IL + law of the excluded middle for sentences (REM) + \(S\) over (b) IL + \(S\). From this proposition, the well known original version of Glivenko theorem and its version for first-order logic (with additional double negation shift scheme) as well as infinitely many other variants of Glivenko-type theorems can be obtained as corollaries. Moreover, (a) is the biggest logic with this property for (b). Further, if \(S\) only contains \(\neg\neg\)-stable (in intuitionistic logic) sentences, then (b) is the least logic for the given (a) with this property.
The paper also contains a proposition characterizing the double negation shift (DNS) axiom scheme in the domain of intermediate logics. DNS is shown to be the weakest scheme deriving classical logic in IL + REM, and the strongest one among the \(\neg\neg\)-stable sentences valid in classical logic. It is shown to be independent from REM, and the latter is shown to be unable to derive any new \(\neg\neg\)-stable sentences in intuitionistic logic.

MSC:

03B55 Intermediate logics
03F03 Proof theory in general (including proof-theoretic semantics)

References:

[1] Church A.: Introduction to Mathematical Logic. Princeton University Press, Princeton (1956) · Zbl 0073.24301
[2] Farahani H., Ono H.: Glivenko theorems and negative translations in substructural predicate logics. Arch. Math. Logic 51, 695-707 (2012) · Zbl 1277.03015 · doi:10.1007/s00153-012-0293-8
[3] Gabbay D.M.: Applications of trees to intermediate logics. J. Symb. Logic 37, 135-138 (1972) · Zbl 0243.02019 · doi:10.2307/2272556
[4] Glivenko V.: Sur quelques points de la logique de M. Brouwer. Académie Royale de Belgique—Bulletin de la classe des sciences, ser. 5 15, 183-188 (1929) · JFM 55.0030.05
[5] Kleene S.C.: Introduction to metamathematics. D. Van Nostrand Co., Inc., New York (1952) · Zbl 0047.00703
[6] Kuroda S.: Intuitionistische Untersuchungen der Formalistischen Logik. Nagoya Math. J. 2, 35-47 (1951) · Zbl 0042.00606
[7] Ono H.: Glivenko theorems revisited. Ann. Pure Appl. Logic 161, 246-250 (2009) · Zbl 1181.03021 · doi:10.1016/j.apal.2009.05.006
[8] Troelstra A.S., Schwichtenberg H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996) · Zbl 0868.03024
[9] Umezawa T.: On some properties of intermediate logics. Proc. Jpn. Acad. 35, 575-577 (1959) · Zbl 0113.24301 · doi:10.3792/pja/1195524178
[10] Umezawa T.: On logics intermediate between intuitionistic and classical predicate logic. J. Symb. Logic 24, 141-153 (1959) · Zbl 0143.01004 · doi:10.2307/2964756
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.