Maximal ideals in countable rings, constructively. (English) Zbl 1524.13008

Blechschmidt, Ingo; Schuster, Peter

Berger, Ulrich (ed.) et al., Revolutions and revelations in computability. 18th conference on computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13359, 24-38 (2022).

The standard way of proving the existence of a maximal ideal in a nontrivial commutative ring is to apply Zorn’s lemma, that is, to use the axiom of choice. The paper under review shows how for countable rings one can obtain similar result without any kind of choice and without the usual decidability assumption that the ring is strongly discrete (membership in finitely generated ideals is decidable). The authors work in a constructive metatheory; in the spirit of [H. Lombardi and C. Quitté, Commutative algebra: constructive methods. Finite projective modules. Translated from the French by Tania K. Roblot. Dordrecht: Springer (2015; Zbl 1327.13001)], they employ minimal logic (see [I. Johansson, Compos. Math. 4, 119–136 (1936; JFM 62.1045.08)]), where by “not \(\phi\)” one means “\(\phi\Rightarrow 1=_{A} 0\)”, and do not assume any form of the axiom of choice. By a functional recursive definition the authors obtain a maximal ideal in the sense that the quotient ring is a residue field (every non-invertible element is zero), and with strong discreteness even a geometric field (every element is either invertible or else zero). It is also shown that the obtained results can be extended to rings indexed by any well-founded set, and can be carried over to Heyting arithmetic with minimal logic. Furthermore, the authors explain how metatheorem of Joyal and Tierney can be used to expand our treatment to arbitrary rings.
For the entire collection see [Zbl 1499.68011].

Reviewer: Alexander B. Levin (Washington, D.C.)

MSC:

13A15	Ideals and multiplicative ideal theory in commutative rings
03F65	Other constructive mathematics

Citations:

Zbl 1327.13001; JFM 62.1045.08

References:

[1]	Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical report, Institut Mittag-Leffler (2000). Report No. 40
[2]	Aczel, P., Rathjen, M.: Constructive set theory (2010). Book draft
[3]	Banaschewski, B., A new proof that ‘Krull implies Zorn’, Math. Log. Quart., 40, 4, 478-480 (1994) · Zbl 0813.03032 · doi:10.1002/malq.19940400405
[4]	Banaschewski, B.; Vermeulen, J., Polynomials and radical ideals, J. Pure Appl. Algebra, 113, 3, 219-227 (1996) · Zbl 0873.13007 · doi:10.1016/0022-4049(95)00149-2
[5]	Barr, M., Toposes without points, J. Pure Appl. Algebra, 5, 3, 265-280 (1974) · Zbl 0294.18009 · doi:10.1016/0022-4049(74)90037-1
[6]	Bauer, A.: Realizability as the connection between computable and constructive mathematics (2005). http://math.andrej.com/asset/data/c2c.pdf
[7]	Bauer, A.: Intuitionistic mathematics and realizability in the physical world. In: Zenil, H. (ed.) A Computable Universe. World Scientific Publishing Co. (2012) · Zbl 1257.03014
[8]	Bauer, A., Five stages of accepting constructive mathematics, Bull. AMS, 54, 481-498 (2017) · Zbl 1469.03171 · doi:10.1090/bull/1556
[9]	Berardi, S.; Valentini, S., Krivine’s intuitionistic proof of classical completeness (for countable languages), Ann. Pure Appl. Log., 129, 1-3, 93-106 (2004) · Zbl 1062.03058 · doi:10.1016/j.apal.2004.01.002
[10]	Blechschmidt, I.: Generalized spaces for constructive algebra. In: Mainzer, K., Schuster, P., Schwichtenberg, H. (eds.) Proof and Computation II, pp. 99-187. World Scientific (2021) · Zbl 1521.03245
[11]	Bonacina, R.; Wessel, D., Ribenboim’s order extension theorem from a constructive point of view, Algebra Universalis, 81, 5, 1-6 (2020) · Zbl 1528.06026
[12]	Bridges, D., Palmgren, E.: Constructive mathematics. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab (2018)
[13]	Caramello, O.: Topos-theoretic background (2014) · Zbl 1335.03073
[14]	Coquand, T.; Lombardi, H., A logical approach to abstract algebra, Math. Struct. Comput. Sci, 16, 5, 885-900 (2006) · Zbl 1118.03059 · doi:10.1017/S0960129506005627
[15]	Coste, M.; Lombardi, H.; Roy, MF, Dynamical method in algebra: effective Nullstellensätze, Ann. Pure Appl. Logic, 111, 3, 203-256 (2001) · Zbl 0992.03076 · doi:10.1016/S0168-0072(01)00026-4
[16]	Crosilla, L.: Exploring predicativity. In: Mainzer, K., Schuster, P., Schwichtenberg, H. (eds.) Proof and Computation, pp. 83-108. World Scientific (2018) · Zbl 07909426
[17]	van Dalen, D., Logic and Structure (2004), Cham: Springer, Cham · Zbl 1048.03001 · doi:10.1007/978-1-4471-4558-5
[18]	Della Dora, J.; Dicrescenzo, C.; Duval, D.; Caviness, BF, About a new method for computing in algebraic number fields, EUROCAL ’85, 289-290 (1985), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-15984-3_279
[19]	Erné, M., A primrose path from Krull to Zorn, Comment. Math. Univ. Carolin., 36, 1, 123-126 (1995) · Zbl 0827.03028
[20]	Friedman, H., The consistency of classical set theory relative to a set theory with intuitionistic logic, J. Symbolic Logic, 38, 315-319 (1973) · Zbl 0278.02045 · doi:10.2307/2272068
[21]	Friedman, H.; Müller, GH; Scott, DS, Classically and intuitionistically provably recursive functions, Higher Set Theory, 21-27 (1978), Heidelberg: Springer, Heidelberg · Zbl 0396.03045 · doi:10.1007/BFb0103100
[22]	Gödel, K., The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Natl. Acad. Sci. USA, 24, 12, 556-557 (1938) · Zbl 0020.29701 · doi:10.1073/pnas.24.12.556
[23]	Hamkins, J., The set-theoretic multiverse, Rev. Symb. Log., 5, 416-449 (2012) · Zbl 1260.03103 · doi:10.1017/S1755020311000359
[24]	Herbelin, H., Ilik, D.: An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem (draft) (2016)
[25]	Hodges, W., Krull implies Zorn, J. Lond. Math. Soc., 19, 2, 285-287 (1979) · Zbl 0394.03045 · doi:10.1112/jlms/s2-19.2.285
[26]	Howard, P., Rubin, J.: Consequences of the Axiom of Choice. Math. Surveys Monogr., AMS (1998) · Zbl 0947.03001
[27]	Hyland, M.: The effective topos. In: Troelstra, A.S., van Dalen, D. (eds.) The L. E. J. Brouwer Centenary Symposium, pp. 165-216. North-Holland (1982)
[28]	Ishihara, H.; Khoussainov, B.; Nerode, A., Decidable Kripke models of intuitionistic theories, Ann. Pure Appl. Logic, 93, 115-123 (1998) · Zbl 0924.03060 · doi:10.1016/S0168-0072(97)00057-2
[29]	Johansson, I., Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compos. Math., 4, 119-136 (1937) · JFM 62.1045.08
[30]	Johnstone, PT, The point of pointless topology, Bull. AMS, 8, 1, 41-53 (1983) · Zbl 0499.54002 · doi:10.1090/S0273-0979-1983-15080-2
[31]	Joyal, A., Tierney, M.: An extension of the Galois theory of Grothendieck, Mem. AMS, vol. 309. AMS (1984) · Zbl 0541.18002
[32]	Krivine, JL, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique, Bull. Symb. Logic, 2, 405-421 (1996) · Zbl 0872.03004 · doi:10.2307/421172
[33]	Krull, W., Idealtheorie in Ringen ohne Endlichkeitsbedingung, Math. Ann., 101, 729-744 (1929) · JFM 55.0681.01 · doi:10.1007/BF01454872
[34]	Lombardi, H.; Quitté, C., Commutative Algebra: Constructive Methods (2015), Dordrecht: Springer, Dordrecht · Zbl 1327.13001 · doi:10.1007/978-94-017-9944-7
[35]	Maietti, M., Modular correspondence between dependent type theories and categories, Math. Struct. Comput. Sci., 15, 6, 1089-1149 (2005) · Zbl 1093.03042 · doi:10.1017/S0960129505004962
[36]	Maietti, M., Joyal’s arithmetic universes as list-arithmetic pretoposes, Theory Appl. Categ., 23, 3, 39-83 (2010) · Zbl 1245.03111
[37]	Mines, R.; Richman, F.; Ruitenburg, W., A Course in Constructive Algebra (1988), Cham: Springer, Cham · Zbl 0725.03044 · doi:10.1007/978-1-4419-8640-5
[38]	Murthy, CR; Myers, JP; O’Donnell, MJ, Classical proofs as programs: how, what and why, Constructivity in Computer Science, 71-88 (1992), Heidelberg: Springer, Heidelberg · Zbl 1379.68099 · doi:10.1007/BFb0021084
[39]	van Oosten, J.: Realizability: An Introduction to its Categorical Side. Studies in Logic and the Foundations of Mathematics, vol. 152. Elsevier (2008) · Zbl 1225.03002
[40]	Persson, H.: An application of the constructive spectrum of a ring. In: Type Theory and the Integrated Logic of Programs. Chalmers University, University of Gothenburg (1999)
[41]	Phoa, W.: An introduction to fibrations, topos theory, the effective topos and modest sets. Technical report, University of Edinburgh (1992)
[42]	Powell, T., Schuster, P., Wiesnet, F.: A universal algorithm for Krull’s theorem. Inf. Comput. (2021) · Zbl 1505.03136
[43]	Powell, T.: On the computational content of Zorn’s lemma. In: LICS 2020, pp. 768-781. ACM (2020) · Zbl 1498.03153
[44]	Rathjen, M.: Generalized inductive definitions in constructive set theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, vol. 48, chap. 16. Clarendon Press (2005) · Zbl 1095.03076
[45]	Richman, F., Nontrivial uses of trivial rings, Proc. AMS, 103, 1012-1014 (1988) · Zbl 0683.13004 · doi:10.1090/S0002-9939-1988-0954974-5
[46]	Rinaldi, D.; Schuster, P., A universal Krull-Lindenbaum theorem, J. Pure Appl. Algebra, 220, 3207-3232 (2016) · Zbl 1420.03128 · doi:10.1016/j.jpaa.2016.02.011
[47]	Rinaldi, D.; Schuster, P.; Wessel, D., Eliminating disjunctions by disjunction elimination, Bull. Symb. Logic, 23, 2, 181-200 (2017) · Zbl 1455.03074 · doi:10.1017/bsl.2017.13
[48]	Rinaldi, D., Schuster, P., Wessel, D.: Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.) 29(1), 226-259 (2018) · Zbl 1437.03163
[49]	Schoenfield, J.: The problem of predicativity. In: Bar-Hillel, Y., Poznanski, E., Rabin, M., Robinson, A. (eds.) Essays on the Foundations of Mathematics, pp. 132-139. Magnes (1961) · Zbl 0173.00903
[50]	Schuster, P.: Induction in algebra: a first case study. In: LICS 2012, pp. 581-585. ACM (2012) · Zbl 1364.03086
[51]	Schuster, P.: Induction in algebra: a first case study. Log. Methods Comput. Sci. 9(3:20), 1-19 (2013) · Zbl 1277.03065
[52]	Schuster, P., Wessel, D.: Resolving finite indeterminacy: a definitive constructive universal prime ideal theorem. In: LICS 2020, pp. 820-830. ACM (2020) · Zbl 1498.03160
[53]	Schuster, P.; Wessel, D.; Anselmo, M.; Della Vedova, G.; Manea, F.; Pauly, A., The computational significance of Hausdorff’s maximal chain principle, Beyond the Horizon of Computability, 239-250 (2020), Cham: Springer, Cham · Zbl 07633512 · doi:10.1007/978-3-030-51466-2_21
[54]	Schuster, P.; Wessel, D., Syntax for semantics: Krull’s maximal ideal theorem, Paul Lorenzen - Mathematician and Logician, 77-102 (2021), Cham: Springer, Cham · Zbl 1490.13001 · doi:10.1007/978-3-030-65824-3_6
[55]	Schuster, P., Wessel, D.: The Jacobson radical for an inconsistency predicate. Computability (2022, forthcoming) · Zbl 1514.03051
[56]	Schuster, P., Wessel, D., Yengui, I.: Dynamic evaluation of integrity and the computational content of Krull’s lemma. J. Pure Appl. Algebra 226(1) (2022) · Zbl 1491.13011
[57]	Schuster, P.; Wessel, D., A general extension theorem for directed-complete partial orders, Rep. Math. Logic, 53, 79-96 (2018) · Zbl 1522.03205
[58]	Scott, D., Prime ideal theorems for rings, lattices and Boolean algebras, Bull. AMS, 60, 390 (1954)
[59]	Shulman, M.: Categorical logic from a categorical point of view (draft for AARMS Summer School 2016) (2016). https://mikeshulman.github.io/catlog/catlog.pdf
[60]	Simpson, S., Subsystems of Second Order Arithmetic (1999), Heidelberg: Springer, Heidelberg · Zbl 0909.03048 · doi:10.1007/978-3-642-59971-2
[61]	Suslin, A., On the structure of the special linear group over polynomial rings, Izv. Akad. Nauk SSSR Ser. Mat., 41, 235-252 (1977) · Zbl 0354.13009
[62]	Tarski, A., Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften, I. Monatsh. Math. Phys., 37, 361-404 (1930) · JFM 56.0046.02 · doi:10.1007/BF01696782
[63]	Vickers, S.; Aiello, M.; Pratt-Hartmann, I.; van Benthem, J., Locales and toposes as spaces, Handbook of Spatial Logics, 429-496 (2007), Heidelberg: Springer, Heidelberg · doi:10.1007/978-1-4020-5587-4_8
[64]	Vickers, S., Continuity and geometric logic, J. Appl. Log., 12, 1, 14-27 (2014) · Zbl 1335.03074 · doi:10.1016/j.jal.2013.07.004
[65]	Vickers, S., Sketches for arithmetic universes, J. Log. Anal., 11, FT4, 1-56 (2016) · Zbl 1420.18011
[66]	Wessel, D., Ordering groups constructively, Comm. Alg., 47, 12, 4853-4873 (2019) · Zbl 1468.03079 · doi:10.1080/00927872.2018.1477947
[67]	Wessel, D., A note on connected reduced rings, J. Comm. Alg., 13, 4, 583-588 (2021) · Zbl 1481.13016
[68]	Yengui, I., Making the use of maximal ideals constructive, Theor. Comput. Sci., 392, 174-178 (2008) · Zbl 1141.13303 · doi:10.1016/j.tcs.2007.10.011
[69]	Yengui, I., Constructive Commutative Algebra. Projective Modules Over Polynomial Rings and Dynamical Gröbner Bases (2015), Cham: Springer, Cham · Zbl 1360.13002 · doi:10.1007/978-3-319-19494-3