×

Interrelation between weak fragments of double negation shift and related principles. (English) Zbl 1445.03006

The following weak fragments of the double negation shift (DNS), the law of excluded middle (LEM), the double negation elimination (DNE), and De Morgan’s law (DML) are considered:
\(\Sigma^0_2\text{-DNS}^0\):
\(\forall\alpha(\forall x\neg\neg\exists y\forall z\,\alpha(x,y,z)=0\to\neg\neg\forall x\exists y\forall z\, \alpha(x,y,z)=0)\);
\(\Sigma^0_1\text{-DNS}^0\):
\(\forall\alpha(\forall x\neg\neg\exists y\,\alpha(x,y)=0\to\neg\neg\forall x\exists y\,\alpha(x,y,z)=0)\);
\(\neg\neg\Sigma^0_1\text{-LEM}\):
\(\forall\alpha\neg\neg\forall x\,(\exists y\,\alpha(x,y)=0\lor\neg\exists y\,\alpha(x,y)=0)\);
\(\neg\neg\Pi^0_1\text{-LEM}\):
\(\forall\alpha\neg\neg\forall x\,(\forall y\,\alpha(x,y)=0\lor\neg\forall y\,\alpha(x,y)=0)\);
\(\Sigma^0_1\text{-DML}\):
\(\forall\alpha,\beta\neg\neg\forall x\,(\neg(\exists y\,\alpha(x,y)=0\land\exists z\,\beta(x,z)=0)\to \neg\exists y\,\alpha(x,y)=0\lor\neg\exists z\,\beta(x,z)=0)\);
\(\neg\neg\Pi^0_1\text{-DML}\):
\(\forall\alpha,\beta\neg\neg\forall x\,(\neg(\forall y\,\alpha(x,y)=0\land\forall z\,\beta(x,z)=0)\to\neg\forall y\,\alpha(x,y)=0\lor\neg\forall z\,\beta(x,z)=0)\);
\(\Sigma^0_1\text{-DNE}\):
\(\forall\alpha\neg\neg\forall x\,(\neg\neg\exists y\,\alpha(x,y)=0\to\exists y\,\alpha(x,y)=0)\);
\(\neg\neg\Delta_{\mathrm{a}}\text{-LEM}\):
\(\forall\alpha,\beta\neg\neg\forall x\,(\exists y\,\alpha(x,y)=0\leftrightarrow\neg\exists z\,\beta(x,z)=0)\to \exists y\,\alpha(x,y)=0\lor\neg\exists y\,\alpha(x,y)=0)\);
\(\neg\neg\Delta_{\mathrm{b}}\text{-LEM}\):
\(\forall\alpha,\beta\neg\neg\forall x\,(\neg\exists y\,\alpha(x,y)=0\leftrightarrow\exists z\,\beta(x,z)=0)\to\exists y\,\alpha(x,y)=0\lor\neg\exists y\,\alpha(x,y)=0)\).
Their first-order counterparts are obtained if one replaces function variables by primitive recursive terms. Interrelation between these principles over elementary intuitionistic analysis \(\mathrm{EL}\) is fully studied. The same is done for the first-order counterparts over intuitionistic arithmetic \(\mathrm{HA}\). The investigation is motivated by application of negative translation in consistency proofs of second-order classical theories relative to the intuitionistic ones.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
03F50 Metamathematics of constructive systems
03F10 Functionals in proof theory
03F25 Relative consistency and interpretations
03F35 Second- and higher-order arithmetic and fragments
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Akama, Y.; Berardi, S.; Hayashi, S.; Kohlenbach, U., Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, An arithmetical hierarchy of the law of excluded middle and related principles, 192-201, (2004), IEEE Computer Society: IEEE Computer Society, Washington, DC
[2] Avigad, J.; Feferman, S.; Buss, S. R., Handbook of Proof Theory, 137, Gödel’s functional (“Dialectica”) interpretation, 337-405, (1998), North-Holland: North-Holland, Amsterdam · doi:10.1016/S0049-237X(98)80020-7
[3] Berardi, S.; Steila, S.; Matthes, R.; Schubert, A., 19th International Conference on Types for Proofs and Programs, 26, Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic, 64-83, (2014), Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH: Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Wadern · Zbl 1359.03045
[4] Cichon, E. A., A short proof of two recently discovered independence results using recursion theoretic methods, Proceedings of the American Mathematical Society, 87, 4, 704-706, (1983) · Zbl 0512.03028 · doi:10.1090/S0002-9939-1983-0687646-0
[5] Dorais, F. G., Classical consequences of continuous choice principles from intuitionistic analysis, Notre Dame Journal of Formal Logic, 55, 1, 25-39, (2014) · Zbl 1331.03013 · doi:10.1215/00294527-2377860
[6] Feferman, S.; Barwise, J., Handbook of Mathematical Logic, 90, Theories of finite type related to mathematical practice, 913-971, (1977), Elsevier · doi:10.1016/S0049-237X(08)71126-1
[7] Fujiwara, M., Intuitionistic and uniform provability in reverse mathematics, (2015), Tohoku University
[8] Fujiwara, M.; Beckmann, A.; Mitrana, V.; Soskova, M., Evolving Computability, 9136, 186-195, (2015), Springer: Springer, Cham · Zbl 1461.03009 · doi:10.1007/978-3-319-20028-6_19
[9] Fujiwara, M.; Ishihara, H.; Nemoto, T., Some principles weaker than Markov’s principle, Archive for Mathematical Logic, 54, 7-8, 861-870, (2015) · Zbl 1354.03093 · doi:10.1007/s00153-015-0444-9
[10] Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, 12, 280-287, (1958) · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[11] Ishihara, H., Indagationes Mathematicae (N.S.), 4, 3, 321-325, (1993) · Zbl 0795.03087 · doi:10.1016/0019-3577(93)90005-J
[12] Ishihara, H.; Crosilla, L.; Schuster, P., From Sets and Types to Topology and Analysis, 48, Constructive reverse mathematics: Compactness properties, 245-267, (2005), Oxford University Press: Oxford University Press, Oxford
[13] Kirby, L.; Paris, J., Accessible independence results for Peano arithmetic, Bulletin of the London Mathematical Society, 14, 4, 285-293, (1982) · Zbl 0501.03017 · doi:10.1112/blms/14.4.285
[14] Kohlenbach, U., Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, (2008), Springer Monographs in Mathematics, Springer-Verlag: Springer Monographs in Mathematics, Springer-Verlag, Berlin · Zbl 1158.03002
[15] Kohlenbach, U., On the disjunctive Markov principle, Studia Logica, 103, 6, 1313-1317, (2015) · Zbl 1330.03091 · doi:10.1007/s11225-015-9627-y
[16] Kreisel, G., Proof theoretic results on intuitionistic first order arithmetic, abstract for the meeting of the Association for Symbolic Logic, Leeds 1962, 27, 3, 379-380
[17] Kreisel, G.; Troelstra, A. S., Formal systems for some branches of intuitionistic analysis, Annals of Pure and Applied Logic, 1, 229-387, (1970) · Zbl 0211.01101
[18] Kuyper, R., On weihrauch reducibility and intuitionistic reverse mathematics, 82, 4, 1438-1458, (2017) · Zbl 1421.03003
[19] Moschovakis, J. R., Proceedings of 5th Panhellenic Logic Symposium, (2005), University of Athens: University of Athens, Athens, Greece
[20] Parsons, C., On n-quantifier induction, 37, 466-482, (1972) · Zbl 0264.02027
[21] Scedrov, A.; Vesley, R. E., On a weakening of Markov’s principle, Archive for Mathematical Logic Grundlagenforsch, 23, 3-4, 153-160, (1983) · Zbl 0533.03033 · doi:10.1007/BF02023022
[22] Simpson, S. G., Subsystems of Second Order Arithmetic, (2009), Cambridge University Press: Cambridge University Press, Cambridge · Zbl 1181.03001
[23] Spector, C.; Dekker, J. C. E., Proceedings of Symposia in Pure Mathematics, vol. V, Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, 1-27, (1962), American Mathematical Society: American Mathematical Society, Providence, RI · Zbl 0143.25502
[24] Toftdal, M.; Díaz, J.; Karhumäki, J.; Lepistö, A.; Sannella, D., Automata, Languages and Programming, 3142, A calibration of ineffective theorems of analysis in a hierarchy of semi-classical logical principles (extended abstract), 1188-1200, (2004), Springer: Springer, Berlin · doi:10.1007/978-3-540-27836-8_98
[25] Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, 344, (1973), Springer-Verlag: Springer-Verlag, Berlin, New York · Zbl 0275.02025
[26] Troelstra, A. S.; Van Dalen, D., Constructivism in Mathematics, An Introduction, vol. I, 121, (1988), North-Holland: North-Holland, Amsterdam · Zbl 0661.03047
[27] Troelstra, A. S.; Van Dalen, D., Constructivism in Mathematics, An Introduction, vol. II, 123, (1988), North-Holland: North-Holland, Amsterdam · Zbl 0661.03047
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.