Classical provability of uniform versions and intuitionistic provability. (English) Zbl 1367.03108
J. L. Hirst and C. Mummert [Notre Dame J. Formal Logic 52, No. 2, 149–162 (2011; Zbl 1225.03083)] and F. G. Dorais [Notre Dame J. Formal Logic 55, No. 1, 25–39 (2014; Zbl 1331.03013)] analyze the relationship between classical uniform provability and intuitionistic provability. They proved some kinds of uniformization theorems.
In the paper under review, the uniformization theorems on uniform versions for RCA and for RCA+WKL are proved. The main theorem states that for every \(\Pi_2\)-statement \(S\) of some syntactical form, if its uniform version derives the uniform variant of ACA over a classical system of arithmetic in all finite types with weak extensionality, \(S\) is not provable in the strong semi-intuitionistic system including bar induction in all finite types but also some nonconstructive principles. The results are used for mathematical principles whose sequential versions imply ACA.
In the paper under review, the uniformization theorems on uniform versions for RCA and for RCA+WKL are proved. The main theorem states that for every \(\Pi_2\)-statement \(S\) of some syntactical form, if its uniform version derives the uniform variant of ACA over a classical system of arithmetic in all finite types with weak extensionality, \(S\) is not provable in the strong semi-intuitionistic system including bar induction in all finite types but also some nonconstructive principles. The results are used for mathematical principles whose sequential versions imply ACA.
Reviewer: Mladen Vuković (Zagreb)
MSC:
| 03F45 | Provability logics and related algebras (e.g., diagonalizable algebras) |
| 03F55 | Intuitionistic mathematics |
| 03B30 | Foundations of classical theories (including reverse mathematics) |
References:
| [1] | Y.Akama, S.Berardi, S.Hayashi and U.Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles, in: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14‐17 July 2004, Turku, Finland, Proceedings (IEEE Press, 2004) pp. 192-201. |
| [2] | J.Avigad and S.Feferman, Gödel’s functional (‘Dialectica’) interpretation, in: Handbook of Proof Theory, edited by S. R.Buss (ed.), Studies in Logic and the Foundations of Mathematics Vol. 137 (Elsevier, 1998) pp. 337-410. · Zbl 0913.03053 |
| [3] | M. A.Bezem, Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, J. Symb. Log.50, 652-660 (1985). · Zbl 0578.03030 |
| [4] | F. G.Dorais, Classical consequences of continuous choice principles from intuitionistic analysis, Notre Dame J. Formal Log.55, 25-39 (2014). · Zbl 1331.03013 |
| [5] | F. G.Dorais, J. L.Hirst, and P.Shafer, Reverse mathematics, trichotomy, and dichotomy, J. Log. Analysis4(13), 1-14 (2012). · Zbl 1296.03008 |
| [6] | S.Feferman, Theories of finite type related to mathematical practice, in: Handbook of Mathematical Logic, edited by J.Barwise (ed.), Studies in Logic and the Foundations of Mathematics Vol. 90 (North‐Holland, 1977) pp. 913-971. |
| [7] | F.Ferreira, Proof interpretations and majorizability, in: Logic Colloquium 2007. Selected papers from the European Summer Meeting of the Association for Symbolic Logic held in Wrocław, July 14-19, 2007, edited by F.Delon (ed.), U.Kohlenbach (ed.), P.Maddy (ed.), and F.Stephan (ed.), Lecture Notes in Logic Vol. 35 (Cambridge University Press, 2010) pp. 32-81. · Zbl 1231.03051 |
| [8] | M.Fujiwara and K.Yokoyama, A note on the sequential version of \(\Pi_2^1\) statements, in: The Nature of Computation. Logic, Algorithms, Applications, 9th Conference on Computability in Europe, CiE 2013, Milan, Italy, July 1-5, 2013. Proceedings, edited by P.Bonizzoni (ed.), V.Brattka (ed.), and B.Löwe (ed.), Lecture Notes in Computer Science Vol. 7921 (Springer‐Verlag, 2013) pp. 171-180. · Zbl 1388.03057 |
| [9] | J. L.Hirst and C.Mummert, Reverse mathematics and uniformity in proofs without excluded middle, Notre Dame J. Formal Log.52(2), 149-162 (2011). · Zbl 1225.03083 |
| [10] | W. A.Howard, Functional interpretation of bar induction by bar recursion, Compositio Math.20, 107-124 (1968). · Zbl 0162.31503 |
| [11] | W. A.Howard and G.Kreisel, Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, J. Symb Log.31(3), 325-358 (1966). · Zbl 0156.00804 |
| [12] | U.Kohlenbach, Pointwise hereditary majorization and some applications, Arch. Math. Log.31, 227-241 (1992). · Zbl 0729.03031 |
| [13] | U.Kohlenbach, Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization, J. Symb. Log.57, 1239-1273 (1992). · Zbl 0781.03051 |
| [14] | U.Kohlenbach, Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Arch. Math. Log.36, 31-71 (1996). · Zbl 0882.03050 |
| [15] | U.Kohlenbach, A note on Spector’s quantifier‐free rule of extensionality, Arch. Math. Log.40, 89-92 (2001). · Zbl 0980.03058 |
| [16] | U.Kohlenbach, On uniform weak König’s lemma, Ann. Pure Appl. Log.114, 103-116 (2002). · Zbl 1001.03052 |
| [17] | U.Kohlenbach, Foundational and mathematical uses of higher types, in: Reflections on the foundations of mathematics. Essays in honor of Solomon Feferman. Papers from the symposium held at Stanford University, Stanford, CA, December 11-13, 1998, edited by W.Sieg (ed.), R.Sommer (ed.), and C.Talcott (ed.), Lecture Notes in Logic Vol. 15 (A. K. Peters, 2002) pp. 92-116. · Zbl 1022.03044 |
| [18] | U.Kohlenbach, Higher order reverse mathematics, in: Reverse mathematics 2001, edited by S. G.Simpson (ed.), Lecture Notes in Logic Vol. 21 (A. K. Peters, 2005) pp. 281-295. · Zbl 1097.03053 |
| [19] | U.Kohlenbach, Applied proof theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics (Springer‐Verlag, 2008). · Zbl 1158.03002 |
| [20] | H.Luckhardt, Extensional Gödel Functional Interpretation. A consistency proof of classical analysis, Springer Lecture Notes in Mathematics Vol. 306 (Springer‐Verlag, 1973). · Zbl 0262.02031 |
| [21] | N.Sakamoto and T.Yamazaki, Uniform versions of some axioms of second order arithmetic, Math. Log. Q.50(6), 587-593 (2004). · Zbl 1063.03045 |
| [22] | S. G.Simpson, Subsystems of Second Order Arithmetic, Second Edition, Perspectives in Mathematical Logic (Cambridge University Press, 2009). · Zbl 1181.03001 |
| [23] | C.Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics, in: Recursive function theory. Proceedings of the Fifth Symposium in Pure Mathematics of the American Mathematical Society held in New York, April 6-7, 1961, edited by J. C. E.Dekker (ed.), Proceedings of Symposia in Pure Mathematics Vol. V (American Mathematical Society, 1962) pp. 1-27. · Zbl 0143.25502 |
| [24] | A. S.Troelstra (ed.) (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics Vol. 344 (Springer‐Verlag, 1973). · Zbl 0275.02025 |
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.
