Sage Journals: Discover world-class research

Abstract

The existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. Following Berardi, Valentini and thus Krivine but using the relative interpretation of negation (that is, as “implies $0 = 1$ ”) we show, in constructive set theory with minimal logic, how for countable rings one can do without any kind of choice and without the usual decidability assumption that the ring is strongly discrete (membership in finitely generated ideals is decidable). By a functional recursive definition we obtain a maximal ideal in the sense that the quotient ring is a residue field (every noninvertible element is zero), and with strong discreteness even a geometric field (every element is either invertible or else zero). Krull’s lemma for the related notion of prime ideal follows by passing to rings of fractions. By employing a construction variant of set-theoretic forcing due to Joyal and Tierney, we expand our treatment to arbitrary rings and establish a connection with dynamical algebra: We recover the dynamical approach to maximal ideals as a parametrized version of the celebrated double negation translation. This connection allows us to give formal a priori criteria elucidating the scope of the dynamical method. Along the way we do a case study for proofs in algebra with minimal logic, and generalize the construction to arbitrary inconsistency predicates. A partial Agda formalization is available at an accompanying repository.1 ¹

See https://github.com/iblech/constructive-maximal-ideals/. This text is a revised and extended version of the conference paper (In Revolutions and Revelations in Computability. 18th Conference on Computability in Europe (2022) Springer). The conference paper only briefly sketched the connection with dynamical algebra; did not compare this connection with other flavors of set-theoretic forcing; and sticked to the case of commutative algebra only, passing on the generalization to inconsistency predicates and well-orders.

Keywords

Maximal ideals set-theoretic forcing constructive commutative algebra dynamical algebra

Get full access to this article

View all access options for this article.

References

Aczel, An introduction to inductive definitions, in: Handbook of Mathematical Logic,

Barwise, ed., Stud. Logic Found. Math., Vol. 90, North-Holland, 1977, pp. 739–782. doi:10.1016/S0049-237X(08)71120-0.

Aczel, The Russell–Prawitz modality, Math. Structures Comput. Sci11(4) (2001), 541–554. doi:10.1017/S0960129501003309.

Aczel and

Rathjen, Constructive Set Theory, 2010, book draft.

Aczel and

Rathjen, Notes on constructive set theory, Technical report, Institut Mittag–Leffler, 2000, Report No. 40.

Apfelmus, The operational monad tutorial, The Monad. Reader15 (2010), 37–56.

Avigad, Forcing in proof theory, Bull. Symbolic Logic10(3) (2004), 305–333. doi:10.2178/bsl/1102022660.

Banaschewski, The power of the ultrafilter theorem, J. London Math. Soc.27(2) (1983), 193–202. doi:10.1112/jlms/s2-27.2.193.

Banaschewski, A new proof that ‘Krull implies Zorn’, Math. Log. Quart.40(4) (1994), 478–480. doi:10.1002/malq.19940400405.

Banaschewski and

Erné, On Krull’s separation lemma, Order10 (1993), 253–260. doi:10.1007/BF01110546.

10.

Banaschewski and

Vermeulen, Polynomials and radical ideals, J. Pure Appl. Algebra113(3) (1996), 219–227. doi:10.1016/0022-4049(95)00149-2.

11.

Barr, Toposes without points, J. Pure Appl. Algebra5(3) (1974), 265–280. doi:10.1016/0022-4049(74)90037-1.

12.

Barton, Forcing and the universe of sets: Must we lose insight?, J. Philos. Logic49 (2020), 575–612. doi:10.1007/s10992-019-09530-y.

13.

Bauer, Realizability as the connection between computable and constructive mathematics, 2005, http://math.andrej.com/asset/data/c2c.pdf.

14.

Bauer, Intuitionistic mathematics and realizability in the physical world, in: A Computable Universe,

Zenil, ed., World Scientific Pub Co, 2012.

15.

Bauer, Five stages of accepting constructive mathematics, Bull. AMS54 (2017), 481–498. doi:10.1090/bull/1556.

16.

Becher, Splitting fields of central simple algebras of exponent two, J. Pure Appl. Algebra220 (2016), 3450–3453. doi:10.1016/j.jpaa.2016.04.009.

17.

Bélanger and

J.-P.

Marquis, Menger and Nöbeling on pointless topology, Logic Log. Philos.22(2) (2013), 145–165.

18.

Bell, Set Theory. Boolean-Valued Models and Independence Proofs, Oxford Logic Guides, Oxford University Press, 2005.

19.

Berardi and

Valentini, Krivine’s intuitionistic proof of classical completeness (for countable languages), Ann. Pure Appl. Log.129(1–3) (2004), 93–106. doi:10.1016/j.apal.2004.01.002.

20.

Blass, Well-ordering and induction in intuitionistic logic and topoi, in: Mathematical Logic and Theoretical Computer Science,

Kueker,

Lopez-Escobar and

Smith, eds, Lect. Notes Pure Appl. Math., Vol. 106, 1986, pp. 29–48.

21.

Blass and

Ščedrov, Classifying topoi and finite forcing, J. Pure Appl. Algebra28(2) (1983), 111–140. doi:10.1016/0022-4049(83)90085-3.

22.

Blechschmidt, Using the internal language of toposes in algebraic geometry, PhD thesis, University of Augsburg, 2017.

23.

Blechschmidt, An elementary and constructive proof of Grothendieck’s generic freeness lemma, 2018, https://arxiv.org/abs/1807.01231.

24.

Blechschmidt, A general Nullstellensatz for generalized spaces, 2020, https://rawgit.com/iblech/internal-methods/master/paper-qcoh.pdf.

25.

Blechschmidt, Generalized spaces for constructive algebra, in: Proof and Computation II,

Mainzer,

Schuster and

Schwichtenberg, eds, World Scientific, 2021, pp. 99–187. doi:10.1142/9789811236488_0004.

26.

Blechschmidt, Exploring mathematical objects from custom-tailored mathematical universes, in: Objects, Structures, and Logics: FilMat Studies in the Philosophy of Mathematics,

Oliveri,

Ternullo and

Boscolo, eds, Springer, 2022.

27.

Blechschmidt and

Oldenziel, The topos-theoretic multiverse: A modal approach for computation, 2023.

28.

Blechschmidt and

Schuster, Maximal ideals in countable rings, constructively, in: Revolutions and Revelations in Computability. 18th Conference on Computability in Europe,

Berger and

Franklin, eds, Lect. Notes Comput. Sci., Springer, 2022, Proceedings, CiE 2022, Swansea, Wales, July 11–15, 2022.

29.

Błocki, An elementary proof of the McCoy theorem, Univ. Iagel. Acta Math.30 (1993), 215–218.

30.

Bonacina and

Wessel, Ribenboim’s order extension theorem from a constructive point of view, Algebra Universalis81(5) (2020).

31.

Borceux, Handbook of Categorical Algebra: Volume 3, Sheaf Theory, Encyclopedia Math. Appl., Cambridge University Press, 1994.

32.

Bridges and

Palmgren, Constructive mathematics, in: The Stanford Encyclopedia of Philosophy,

Zalta, ed., Metaphysics Research Lab, 2018.

33.

Cave,

Ferreira,

Panangaden and

Pientka, Fair reactive programming, in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, 2014, pp. 361–372.

34.

Cederquist and

Coquand, Entailment relations and distributive lattices, in: Logic Colloquium ’98. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9–15, 1998,

Buss,

Hájek and

Pudlák, eds, Lect. Notes Logic, Vol. 13, A. K. Peters, 2000, pp. 127–139.

35.

Conrad, Constructing Algebraic Closures, 2021, https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosureshorter.pdf .

36.

Coquand, Notions invariant by change of basis, 2001, https://www.cse.chalmers.se/~coquand/base.ps.

37.

Coquand, About Goodman’s theorem, Ann. Pure Appl. Logic164(4) (2013), 437–442. doi:10.1016/j.apal.2012.10.007.

38.

Coquand, Point-free topology and sheaf models. Slides for the workshop on critical views on infinity, organized by Laura Crosilla, 2021, https://www.cse.chalmers.se/~coquand/potential.pdf.

39.

Coquand and

Lombardi, Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings, in: Commutative Ring Theory and Applications,

Fontana,

S.-E.

Kabbaj and

Wiegand, eds, Lect Notes Pure Appl. Math., Vol. 231, Addison-Wesley, 2002, pp. 477–499.

40.

Coquand and

Lombardi, A logical approach to abstract algebra, Math. Structures Comput. Sci16(5) (2006), 885–900. doi:10.1017/S0960129506005627.

41.

Coquand and

Lombardi, Krull’s principal ideal theorem, Technical report, 30, Institut Mittag-Leffler, 2000/2001.

42.

Coquand and

Persson, Gröbner bases in type theory, in: TYPES 1998: Types for Proofs and Programs,

Altenkirch,

Reus and

Naraschewski, eds, Lecture Notes in Comput. Sci., Vol. 1657, Springer, 1999, pp. 33–46.

43.

Coste,

Lombardi and

M.-F.

Roy, Dynamical method in algebra: Effective Nullstellensätze, Ann. Pure Appl. Logic111(3) (2001), 203–256. doi:10.1016/S0168-0072(01)00026-4.

44.

Crosilla, Exploring predicativity, in: Proof and Computation,

Mainzer,

Schuster and

Schwichtenberg, eds, World Scientific, 2018, pp. 83–108. doi:10.1142/9789813270947_0003.

45.

Dora,

Dicrescenzo and

Duval, About a new method for computing in algebraic number fields, in: Europ. Conference on Computer Algebra (2), 1985, pp. 289–290.

46.

Erné, A primrose path from Krull to Zorn, Comment. Math. Univ. Carolin.36(1) (1995), 123–126.

47.

Escardó and

Oliva, The Peirce translation and the double negation shift, in: Programs, Proofs, Processes,

Ferreira,

Löwe,

Mayordomo and

Mendes Gomes, eds, Lecture Notes in Comput. Sci., Vol. 6158, Springer, 2010, pp. 151–161. doi:10.1007/978-3-642-13962-8_17.

48.

Ferreira and

Oliva, On various negative translations, in: Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21–22 August 2010,

van Bakel,

Berardi and

Berger, eds, EPTCS, Vol. 47, 2010, pp. 21–33.

49.

Ferreira and

Oliva, On the relation between various negative translations, in: Logic, Construction, Computation,

Berger,

Diener,

Schuster and

Seisenberger, eds, Ontos Math. Log., Vol. 3, De Gruyter, 2012, pp. 227–258.

50.

Forster,

Kirst and

Wehr, Completeness theorems for first-order logic analysed in constructive type theory: Extended version, J. Logic Comput.31 (2021), 112–151. doi:10.1093/logcom/exaa073.

51.

Friedman, The consistency of classical set theory relative to a set theory with intuitionistic logic, J. Symbolic Logic38 (1973), 315–319. doi:10.2307/2272068.

52.

Friedman, Classical and intuitionistically provably recursive functions, in: Higher Set Theory,

Müller and

Scott, eds, LNM, Vol. 669, Springer, 1978, pp. 21–27. doi:10.1007/BFb0103100.

53.

Geschke, Models of Set Theory, 2011, https://www.math.uni-hamburg.de/home/geschke/teaching/ModelsSetTheory.pdf .

54.

Geschke and

Quickert, On Sacks forcing and the Sacks property, in: Classical and New Paradigms of Computation and Their Complexity Hierarchies. Papers of the Conference “Foundations of the Formal Sciences III”,

Löwe,

Piwinger and

Räsch, eds, Trends Log. Stud. Log. Libr., Vol. 23, Springer, 2004, pp. 95–139.

55.

Gilmer, A note on the algebraic closure of a field, Amer. Math. Monthly75(10) (1968), 1101–1102. doi:10.2307/2315743.

56.

Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Natl. Acad. Sci. USA24(12) (1938), 556–557. doi:10.1073/pnas.24.12.556.

57.

Goldblatt, Grothendieck topology as geometric modality, MLQ Math. Log. Q.27(31–35) (1981), 495–529. doi:10.1002/malq.19810273104.

58.

Goldblatt, Topoi: The Categorical Analysis of Logic, Stud. Logic Found. Math., Vol. 98, Elsevier, 1984.

59.

Grayson, Forcing in intuitionistic systems without power-set, J. Symbolic Logic48(3) (1983), 670–682. doi:10.2307/2273459.

60.

Hamkins, The set-theoretic multiverse, Rev. Symb. Log.5 (2012), 416–449. doi:10.1017/S1755020311000359.

61.

Hatzikiriakou, Minimal prime ideals and arithmetic comprehension, J. Symbolic Logic56(1) (1991), 67–70. doi:10.2307/2274904.

62.

Henkin, Metamathematical theorems equivalent to the prime ideal theorem for Boolean algebras, Bull. Amer. Math. Soc.60 (1954), 387–388.

63.

Herbelin and

Ilik, An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem (draft), 2016.

64.

Hodges, Krull implies Zorn, J. Lond. Math. Soc.19(2) (1979), 285–287. doi:10.1112/jlms/s2-19.2.285.

65.

Howard and

Rubin, Consequences of the Axiom of Choice, Math. Surveys Monogr., AMS, 1998.

66.

Hyland, The effective topos, in: The L. E. J. Brouwer Centenary Symposium,

A.S.

Troelstra and

van Dalen, eds, North-Holland, 1982, pp. 165–216.

67.

Ishihara,

Khoussainov and

Nerode, Decidable Kripke models of intuitionistic theories, Ann. Pure Appl. Logic93 (1998), 115–123. doi:10.1016/S0168-0072(97)00057-2.

68.

Jacobsson and

Löfwall, Standard bases for general coefficient rings and a new constructive proof of Hilbert’s basis theorem, J. Symbolic Comput.12(3) (1991), 337–372. doi:10.1016/S0747-7171(08)80154-X.

69.

Jech, Multiple Forcing, Cambridge Tracts in Math., Vol. 88, Oxford University Press, 1987.

70.

Johansson, Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compos. Math.4 (1937), 119–136.

71.

P.T.

Johnstone, Topos Theory, L.M.S. Monographs, Vol. 10, Academic Press, 1977.

72.

P.T.

Johnstone, The point of pointless topology, Bull. AMS8(1) (1983), 41–53. doi:10.1090/S0273-0979-1983-15080-2.

73.

P.T.

Johnstone, The art of pointless thinking: A student’s guide to the category of locales, in: Category Theory at Work (Bremen, 1990), Res. Exp. Math., Heldermann, 1991, pp. 85–107.

74.

P.T.

Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Oxford University Press, 2002.

75.

Joyal and

Tierney, An extension of the Galois theory of Grothendieck, in: Mem. AMS, Vol. 309, AMS, 1984.

76.

Kiselyov and

Ishii, Freer monads, more extensible effects, in: Haskell ’15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, 2015, pp. 94–105. doi:10.1145/2804302.2804319.

77.

J.-L.

Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique, Bull. Symb. Logic2 (1996), 405–421. doi:10.2307/421172.

78.

Krull, Idealtheorie in Ringen ohne Endlichkeitsbedingung, Math. Ann.101 (1929), 729–744. doi:10.1007/BF01454872.

79.

T.Y.

Lam, Exercises in Modules and Rings, Problem Books in Math., Springer, 2007.

80.

Lombardi and

Quitté, Commutative Algebra: Constructive Methods, Springer, 2015.

81.

Lorenzen, Algebraische und logistische Untersuchungen über freie Verbände, Vol. 16, 1951, pp. 81–106, English translation available [89].

82.

Maietti, Joyal’s arithmetic universes as list-arithmetic pretoposes, Theory Appl. Categ.23(3) (2010), 39–83.

83.

Mannaa and

Coquand, A sheaf model of the algebraic closure, in: Proc. of the Fifth International Workshop on Classical Logic and Computation, 2014.

84.

Mines,

Richman and

Ruitenburg, A Course in Constructive Algebra, Universitext, Springer, 1988.

85.

Misselbeck-Wessel and

Schuster, Radical theory of Scott-open filters, Theoret. Comput. Sci.945 (2023), 113677.

86.

Moerdijk and

Vermeulen, Proper maps of toposes, in: Mem. Amer. Math. Soc., Vol. 705, AMS, 2000.

87.

Moore, The Method of Forcing, 2019, https://arxiv.org/abs/1902.03235 .

88.

Murthy, Classical proofs as programs: How, what and why, in: Constructivity in Comp. Science,

Myers and

O’Donnell, eds, Springer, 1992, pp. 71–88. doi:10.1007/BFb0021084.

89.

Neuwirth, Algebraic and logistic investigations on free lattices, 2017, English translation of [81], https://arxiv.org/abs/1710.08138.

90.

Neuwirth, Lorenzen’s reshaping of Krull’s Fundamentalsatz for integral domains (1938–1953), in: Paul Lorenzen: Mathematician and Logician,

Heinzmann and

Wolters , eds, Log. Epistemol. Unity Sci., Vol. 51, Springer, 2021, pp. 143–183.

91.

Palmgren, Constructive sheaf semantics, Math. Log. Quart.43 (1997), 321–327. doi:10.1002/malq.19970430304.

92.

Paykin,

Krishnaswami and

Zdancewic, The essence of event-driven programming, 2016, https://jpaykin.github.io/papers/pkz_CONCUR_2016.pdf.

93.

Penelope and

Meadows, A reconstruction of Steel’s multiverse project, Bull. Symb. Logic26(2) (2020), 118–169. doi:10.1017/bsl.2020.5.

94.

Perdry, Strongly Noetherian rings and constructive ideal theory, J. Symbolic Comput.37(4) (2004), 511–535. doi:10.1016/j.jsc.2003.02.001.

95.

Perdry, Lazy bases: A minimalist constructive theory of Noetherian rings, MLQ Math. Log. Q.54(1) (2008), 70–82. doi:10.1002/malq.200710042.

96.

Perdry and

Schuster, Noetherian orders, Math. Structures in Comput. Sci.21(1) (2011), 111–124. doi:10.1017/S0960129510000460.

97.

Persson, An application of the constructive spectrum of a ring, in: Type Theory and the Integrated Logic of Programs, Chalmers Univ., Univ. of Gothenburg, 1999.

98.

Pfenning and

Davies, A judgmental reconstruction of modal logic, Math. Structures Comput. Sci.11(4) (2001), 511–540. doi:10.1017/S0960129501003322.

99.

Phoa, An introduction to fibrations, topos theory, the effective topos and modest sets, Technical report, University of Edinburgh, 1992.

100.

Picado and

Pultr, Frames and Locales. Topology Without Points, Front. Math., Birkhäuser, 2012.

101.

Pohst and

Zassenhaus, Algorithmic Algebraic Number Theory, Encyclopedia Math. Appl., Cambridge University Press, 1989.

102.

Poincaré, La logique de l’infini, Rev. méta. et mor.17 (1909), 461–482.

103.

Powell, On the computational content of Zorn’s lemma, in: LICS ’20, ACM, 2020, pp. 768–781. doi:10.1145/3373718.3394745.

104.

Powell,

Schuster and

Wiesnet, A universal algorithm for Krull’s theorem, Information and Computation (2021).

105.

Rathjen, Generalized inductive definitions in constructive set theory, in: From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics,

Crosilla and

Schuster, eds, Oxford Logic Guides, Vol. 48, Clarendon Press, 2005, chapter 16.

106.

Renardel de Lavalette, Extended bar induction in applicative theories, Ann. Pure Appl. Logic50(2) (1990), 139–189. doi:10.1016/0168-0072(90)90047-6.

107.

Richman, Constructive aspects of Noetherian rings, Proc. AMS44(2) (1974), 436–441. doi:10.1090/S0002-9939-1974-0416874-9.

108.

Richman, Nontrivial uses of trivial rings, Proc. AMS103 (1988), 1012–1014. doi:10.1090/S0002-9939-1988-0954974-5.

109.

Richman, The ascending tree condition: Constructive algebra without choice, Comm. Algebra31(4) (2003), 1993–2002. doi:10.1081/AGB-120018518.

110.

Richman, A theorem of Gilmer and the canonical universal splitting ring, Comm. Alg.6(1) (2014), 101–108.

111.

Rinaldi and

Schuster, A universal Krull–Lindenbaum theorem, J. Pure Appl. Algebra220 (2016), 3207–3232. doi:10.1016/j.jpaa.2016.02.011.

112.

Rinaldi,

Schuster and

Wessel, Eliminating disjunctions by disjunction elimination, Bull. Symb. Logic23(2) (2017), 181–200. doi:10.1017/bsl.2017.13.

113.

Rinaldi,

Schuster and

Wessel, Eliminating disjunctions by disjunction elimination, Indag. Math. (N. S.)29(1) (2018), 226–259. doi:10.1016/j.indag.2017.09.011.

114.

Rinaldi and

Wessel, Cut elimination for entailment relations, Arch. Math. Logic58 (2019), 605–625. doi:10.1007/s00153-018-0653-0.

115.

Roberts, Class forcing and topos theory, Technical report, The University of Adelaide, 2018.

116.

Roitman, The uses of set theory, Math. Intelligencer14(1) (1992), 63–69. doi:10.1007/BF03024144.

117.

Sato, Forcing for hat inductive definitions in arithmetic, Math. Log. Quart.60(4–5) (2004), 314–318.

118.

Ščedrov, Forcing and classifying topoi, in: Mem. Amer. Math. Soc., Vol. 48, AMS, 1985.

119.

Schilhan, Forcing and applications on bounding, splitting and almost disjointness, Bachelor’s thesis, at the Universität Wien, 2016.

120.

Schoenfield, The problem of predicativity, in: Essays on the Foundations of Mathematics,

Bar-Hillel,

Poznanski,

Rabin and

Robinson, eds, Magnes, 1961, pp. 132–139.

121.

Schuster, Induction in algebra: A first case study, in: LICS ’12, ACM, 2012, pp. 581–585.

122.

Schuster, Induction in algebra: A first case study, Log. Methods Comput. Sci.9(3:20) (2013), 1–19.

123.

Schuster and

Wessel, A general extension theorem for directed-complete partial orders, Rep. Math. Logic53 (2018), 79–96.

124.

Schuster and

Wessel, Resolving finite indeterminacy: A definitive constructive universal prime ideal theorem, in: LICS ’20, ACM, 2020, pp. 820–830. doi:10.1145/3373718.3394777.

125.

Schuster and

Wessel, The computational significance of Hausdorff’s maximal chain principle, in: CiE ’20, Lecture Notes in Comput. Sci., 2020.

126.

Schuster and

Wessel, Syntax for semantics: Krull’s maximal ideal theorem, in: Paul Lorenzen: Mathematician and Logician,

Heinzmann and

Wolters , eds, Log. Epistemol. Unity Sci., Vol. 51, Springer, 2021, pp. 77–102.

127.

Schuster and

Wessel, The Jacobson radical for an inconsistency predicate, Computability11(2) (2022), 147–162. doi:10.3233/COM-210365.

128.

Schuster,

Wessel and

Yengui, Dynamic evaluation of integrity and the computational content of Krull’s lemma, J. Pure Appl. Algebra226(1) (2022).

129.

Schuster and

Zappe, Do Noetherian rings have Noetherian basis functions? in: Logical Approaches to Computational Barriers. Second Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006,

Beckmann,

Berger,

Löwe and

Tucker, eds, Lect. Notes Comput. Sci., Vol. 3988, Springer, 2006, pp. 481–489.

130.

Scott, Prime ideal theorems for rings, lattices, and Boolean algebras, Bull. Amer. Math. Soc.60(4) (1954), 390.

131.

Scott, Completeness and axiomatizability in many-valued logic, in: Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971),

Henkin,

Addison,

Chang,

Craig,

Scott and

Vaught, eds, AMS, 1974, pp. 411–435. doi:10.1090/pspum/025/0363802.

132.

Seidenberg, What is Noetherian?, Rend. Sem. Mat. Fis. Milano44 (1974), 55–61. doi:10.1007/BF02925651.

133.

Simpson, Subsystems of Second Order Arithmetic, Springer, 1999.

134.

Streicher, Introduction to Category Theory and Categorical Logic, 2004, https://www.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf .

135.

Streicher, Forcing for IZF in sheaf toposes, Georgian Math. J.16(1) (2009), 203–209. doi:10.1515/GMJ.2009.203.

136.

Suslin, On the structure of the special linear group over polynomial rings, Izv. Akad. Nauk SSSR Ser. Mat.41 (1977), 235–252.

137.

Swierstra, Data types à la carte, J. Funct. Programming18 (2008), 423–436. doi:10.1017/S0956796808006758.

138.

Tarski, Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I, Monatsh. Math. Phys.37 (1930), 361–404. doi:10.1007/BF01696782.

139.

Tennenbaum, A constructive version of Hilbert’s basis theorem, PhD thesis, University of California, 1973.

140.

Tierney, Forcing topologies and classifying topoi, in: Algebra, Topology, and Category Theory,

Heller and

Tierney, eds, Academic Press, 1976, pp. 211–219. doi:10.1016/B978-0-12-339050-9.50021-3.

141.

van Dalen, Logic and Structure, Universitext, Springer, 2004.

142.

van Oosten, Realizability: An Introduction to Its Categorical Side, Stud. Logic Found. Math., Vol. 152, Elsevier, 2008.

143.

Veldman and

Bezem, Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics, J. Lond. Math. Soc. (2)47 (1993), 193–211. doi:10.1112/jlms/s2-47.2.193.

144.

Vickers, Locales and toposes as spaces, in: Handbook of Spatial Logics,

Aiello,

Pratt-Hartmann and

van Benthem, eds, Springer, 2007, pp. 429–496. doi:10.1007/978-1-4020-5587-4_8.

145.

Vickers, Continuity and geometric logic, J. Appl. Log.12(1) (2014), 14–27. doi:10.1016/j.jal.2013.07.004.

146.

Vickers, Sketches for arithmetic universes, J. Log. Anal.11(FT4) (2016), 1–56.

147.

Weaver, Forcing for Mathematicians, World Scientific, 2014.

148.

Wessel, Points, ideals, and geometric sequents, Technical report, University of Verona, 2018.

149.

Wessel, Ordering groups constructively, Comm. Alg.47(12) (2019), 4853–4873. doi:10.1080/00927872.2018.1477947.

150.

Wessel, A note on connected reduced rings, J. Comm. Alg.13(4) (2021), 583–588.

151.

Yamamoto, Toposes from forcing for intuitionistic ZF with atoms, 2017, https://arxiv.org/abs/1702.03399.

152.

Yengui, Making the use of maximal ideals constructive, Theoret. Comput. Sci.392 (2008), 174–178. doi:10.1016/j.tcs.2007.10.011.

153.

Yengui, Constructive Commutative Algebra. Projective Modules over Polynomial Rings and Dynamical Gröbner Bases, LNM, Vol. 2138, Springer, 2015.

Reifying dynamical algebra: Maximal ideals in countable rings,constructively

Abstract

Keywords

Get full access to this article

References