The Jacobson radical of a propositional theory. (English) Zbl 07550752
Summary: Alongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum’s Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko’s Theorem. The Jacobson radical in fact turns out to coincide with the classical deductive closure. As a by-product we obtain a possible interpretation in logic of the axioms-as-rules conservation criterion for a multi-conclusion Scott-style entailment relation over a single-conclusion one.
MSC:
| 03F03 | Proof theory in general (including proof-theoretic semantics) |
| 03F65 | Other constructive mathematics |
| 13C10 | Projective and free modules and ideals in commutative rings |
Keywords:
Jacobson radical; propositional theory; Lindenbaum’s Lemma; Glivenko’s Theorem; axioms as rules; conservation criterion; entailment relationSoftware:
PescaReferences:
| [1] | Aczel, P., The type theoretic interpretation of constructive set theory, Logic Colloquium ’77, Studies in Logic and the Foundations of Mathematics, vol. 96, North-Holland, Amsterdam, 1978, pp. 55-66. · Zbl 0481.03035 |
| [2] | Aczel, P., The type theoretic interpretation of constructive set theory: Choice principles, The L. E. J. Brouwer Centenary Symposium, Studies in Logic and the Foundations of Mathematics, vol. 110, North-Holland, Amsterdam, 1982, pp. 1-40. · Zbl 0529.03035 |
| [3] | Aczel, P., The type theoretic interpretation of constructive set theory: Inductive definitions, Logic, Methodology and Philosophy of Science, VII, Studies in Logic and the Foundations of Mathematics, vol. 114, North-Holland, Amsterdam, 1986, pp. 17-49. · Zbl 0624.03044 |
| [4] | Aczel, P. and Rathjen, M., Notes on constructive set theory, Technical report no. 40, Institut Mittag-Leffler, 2000. |
| [5] | Aczel, P. and Rathjen, M., Constructive set theory, Book draft, 2010. Available at https://www1.maths.leeds.ac.uk/ rathjen/book.pdf (accessed 24 August, 2021). |
| [6] | Avron, A., Simple consequence relations. Information and Computation, vol. 92 (1991), pp. 105-139. · Zbl 0733.03007 |
| [7] | Béziau, J.-Y., Les axiomes de Tarski, La philosophie en Pologne 1919-1939 (R. Pouivet and M. Resbuschi, editors), Librairie Philosophique J. VRIN, Paris, 2006. |
| [8] | Bishop, E., Foundations of Constructive Analysis, McGraw-Hill, New York, 1967. · Zbl 0183.01503 |
| [9] | Bishop, E. and Bridges, D., Constructive Analysis, Springer, Berlin-Heidelberg, 1985. · Zbl 0656.03042 |
| [10] | Blass, A., Prime ideals yield almost maximal ideals. Fundamenta Mathematicae, vol. 127 (1987), no. 1, pp. 57-66. · Zbl 0609.06006 |
| [11] | Brouwer, L. E. J., De onbetrouwbaarheid der logische principes, Tijdschrift voor Wijsbegeerte, vol. 2 (1908), pp. 152-158. |
| [12] | Brouwer, L. E. J., Intuitionistische Zerlegung mathematischer Grundbegriffe, Jahresbericht der Deutschen Mathematiker-Vereinigung, vol. 33 (1925), pp. 251-256. · JFM 51.0047.06 |
| [13] | Carnap, R., Formalization of Logic, Harvard University Press, Cambridge, 1943. · Zbl 0061.00709 |
| [14] | Cederquist, J. and Coquand, T., Entailment relations and distributive lattices, Logic Colloquium ’98 (S. R. Buss, P. Hájek, and P. Pudlák, editors), Lecture Notes in Logic, vol. 13, A. K. Peters, Natick, 2000, pp. 127-139. · Zbl 0948.03056 |
| [15] | Cederquist, J., Coquand, T., and Negri, S., The Hahn-Banach theorem in type theory, Twenty-Five Years of Constructive Type Theory (G. Sambin and J. M. Smith, editors), Oxford Logic Guides, vol. 36, Oxford University Press, New York, 1998, pp. 57-72. · Zbl 0940.03069 |
| [16] | Cintula, P. and Carles, N., The proof by cases property and its variants in structural consequence relations. Studia Logica, vol. 101 (2013), no. 4, pp. 713-747. · Zbl 1316.03040 |
| [17] | Ciraulo, F., Maietti, M. E., and Sambin, G., Convergence in formal topology: A unifying notion. Journal of Logic and Analysis, vol. 5 (2013), no. 2, pp. 1-45. · Zbl 1280.54003 |
| [18] | Ciraulo, F., Rinaldi, D., and Schuster, P., Lindenbaum’s lemma via open induction, Advances in Proof Theory (R. Kahle, T. Strahm, and T. Studer, editors), Progress in Computer Science and Applied Logic, vol. 28, Springer, Cham, 2016, pp. 65-77. · Zbl 1439.03032 |
| [19] | Ciraulo, F. and Sambin, G., Finitary formal topologies and Stone’s representation theorem. Theoretical Computer Science, vol. 405 (2008), nos. 1-2, pp. 11-23. · Zbl 1187.54010 |
| [20] | Coquand, T., A direct proof of the localic Hahn-Banach theorem, 2000. Available at http://www.cse.chalmers.se/ coquand/formal.html (accessed 24 August, 2021). |
| [21] | Coquand, T., Lewis Carroll, Gentzen and entailment relations, 2000. Available at http://www.cse.chalmers.se/ coquand/formal.html. |
| [22] | Coquand, T., About Stone’s notion of spectrum. Journal of Pure and Applied Algebra, vol. 197 (2005), nos. 1-3, pp. 141-158. · Zbl 1061.06031 |
| [23] | Coquand, T., Geometric Hahn-Banach theorem. Mathematical Proceedings of the Cambridge Philosophical Society, vol. 140 (2006), pp. 313-315. · Zbl 1095.46046 |
| [24] | Coquand, T., Space of valuations. Annals of Pure and Applied Logic, vol. 157 (2009), 97-109. · Zbl 1222.03072 |
| [25] | Coquand, T. and Lombardi, H., Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings, Commutative Ring Theory and Applications (M. Fontana, S.-E. Kabbaj, and S. Wiegand, editors), Lecture Notes in Pure and Applied Mathematics, vol. 231, Addison-Wesley, Reading, 2002, pp. 477-499. · Zbl 1096.13507 |
| [26] | Coquand, T. and Lombardi, H., A logical approach to abstract algebra. Mathematical Structures in Computer Science, vol. 16 (2006), pp. 885-900. · Zbl 1118.03059 |
| [27] | Coquand, T., Lombardi, H., and Neuwirth, S., Lattice-ordered groups generated by an ordered group and regular systems of ideals. The Rocky Mountain Journal of Mathematics, vol. 49 (2019), no. 5, pp. 1449-1489. · Zbl 1496.06018 |
| [28] | Coquand, T., Lombardi, H., and Quitté, C., Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon: Algèbre et Théorie des Nombres, 2006, pp. 57-100. · Zbl 1158.13308 |
| [29] | Coquand, T. and Persson, H., Valuations and Dedekind’s Prague theorem. Journal of Pure and Applied Algebra, vol. 155 (2001), nos. 2-3, pp. 121-129. · Zbl 0983.11061 |
| [30] | Coquand, T., Sadocco, S., Sambin, G., and Smith, J. M., Formal topologies on the set of first-order formulae. The Journal of Symbolic Logic, vol. 65 (2000), no. 3, pp. 1183-1192. · Zbl 0965.03072 |
| [31] | Coquand, T., Sambin, G., Smith, J., and Valentini, S., Inductively generated formal topologies. Annals of Pure and Applied Logic, vol. 124 (2003), pp. 71-106. · Zbl 1070.03041 |
| [32] | Coquand, T. and Zhang, G.-Q., Sequents, frames, and completeness, Computer Science Logic (P. G. Clote and H. Schwichtenberg, editors), Lecture Notes in Computer Science, vol. 1862, Springer, Berlin, 2000, pp. 277-291. · Zbl 0973.03080 |
| [33] | Coste, M., Lombardi, H., and Roy, M.-F., Dynamical method in algebra: Effective Nullstellensätze. Annals of Pure and Applied Logic, vol. 111 (2001), no. 3, pp. 203-256. · Zbl 0992.03076 |
| [34] | David, R., Nour, K., and Raffalli, C., Introduction à la Logique. Théorie de la démonstration, second ed., Dunod, Paris, 2003. |
| [35] | Došen, K., On passing from singular to plural consequences, Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa (E. Orlowska, editor), Studies in Fuzziness and Soft Computing, vol. 24, Physica, Heidelberg, 1999, pp. 533-547. · Zbl 0923.03020 |
| [36] | Espíndola, C., A short proof of Glivenko theorems for intermediate predicate logics. Archive for Mathematical Logic, vol. 52 (2013), nos. 7-8, pp. 823-826. · Zbl 1316.03015 |
| [37] | , Intermediate logic, 2016. Available at http://www.encyclopediaofmath.org/index.php?title=Intermediate_logic&oldid=39747 (accessed 13 November, 2016). |
| [38] | Fellin, G., The Jacobson Radical: From Algebra to Logic, Master’s thesis, Università di Verona, Dipartimento di Informatica, Verona, 2018. |
| [39] | Fellin, G. and Schuster, P., A general Glivenko-Gödel theorem for nuclei, Proceedings of the 37th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2021 (A. Sokolova, editor), Electronic Notes in Theoretical Computer Science, Elsevier, 2021. |
| [40] | Fellin, G., Schuster, P., and Wessel, D., The Jacobson radical of a propositional theory, Proof-Theoretic Semantics: Assessment and Future Perspectives (T. Piecha and P. Schroeder-Heister, editors), University of Tübingen, 2019, pp. 287-299, http://doi.org/10.15496/publikation-35319. |
| [41] | Gabbay, D. M., Semantical Investigations in Heyting’s Intuitionistic Logic, Synthese Library, vol. 148, D. Reidel Publishing Co., Dordrecht-Boston, 1981. · Zbl 0453.03001 |
| [42] | Galatos, N. and Ono, H., Glivenko theorems for substructural logics over FL. The Journal of Symbolic Logic, vol. 71 (2006), no. 4, pp. 1353-1384. · Zbl 1109.03016 |
| [43] | Gentzen, G., Untersuchungen über das logische Schließen I. Mathematische Zeitschrift, vol. 39 (1934), pp. 176-210. · JFM 60.0020.02 |
| [44] | Gentzen, G., Untersuchungen über das logische Schließen II. Mathematische Zeitschrift, vol. 39 (1934), pp. 405-431. · Zbl 0010.14601 |
| [45] | Glivenko, V., Sur la logique de M. Brouwer. Academie Royale des Sciences des Lettres et des Beaux-Arts de Belgique. Bulletin de la Classe des Sciences Cinquième Série, vol. 14 (1928), pp. 225-228. · JFM 54.0054.01 |
| [46] | Glivenko, V., Sur quelques points de la Logique de M. Brouwer. Academie Royale des Sciences des Lettres et des Beaux-Arts de Belgique. Bulletin de la Classe des Sciences Cinquième Série, vol. 15 (1929), 183-188. · JFM 55.0030.05 |
| [47] | Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, vol. 12 (1958), pp. 280-287. · Zbl 0090.01003 |
| [48] | Guerrieri, G. and Naibo, A., Postponement of \(\mathsf{raa}\) and Glivenko’s theorem, revisited. Studia Logica, vol. 107 (2019), no. 1, pp. 109-144. · Zbl 1531.03090 |
| [49] | Hertz, P., Über Axiomensysteme für beliebige Satzsysteme. I. Teil. Sätze ersten Grades. Mathematische Annalen, vol. 87 (1922), no. 3, pp. 246-269. · JFM 48.1117.05 |
| [50] | Hertz, P., Über Axiomensysteme für beliebige Satzsysteme. II. Teil. Sätze höheren Grades. Mathematische Annalen, vol. 89 (1923), no. 1, pp. 76-102. · JFM 49.0683.01 |
| [51] | Hertz, P., Über Axiomensysteme für beliebige Satzsysteme. Mathematische Annalen, vol. 101 (1929), no. 1, pp. 457-514. · JFM 55.0627.01 |
| [52] | Humberstone, L., On a conservative extension argument of Dana Scott. Logic Journal of the IGPL, vol. 19 (2011), pp. 241-288. · Zbl 1216.03036 |
| [53] | Humberstone, L., Dana Scott’s work with generalized consequence relations, Universal Logic: An Anthology. From Paul Hertz to Dov Gabbay (J.-Y. Béziau, editor), Studies in Universal Logic, Birkhäuser, Basel, 2012, pp. 263-279. · Zbl 1295.03008 |
| [54] | Iemhoff, R., Consequence relations and admissible rules. Journal of Philosophical Logic, vol. 45 (2016), no. 3, pp. 327-348. · Zbl 1392.03021 |
| [55] | Ishihara, H., Classical propositional logic and decidability of variables in intuitionistic propositional logic. Logical Methods in Computer Science, vol. 10 (2014), no. 3, pp. 3:1-3:7. · Zbl 1337.03017 |
| [56] | Ishihara, H. and Schwichtenberg, H., Embedding classical in minimal implicational logic. Mathematical Logic Quarterly, vol. 62 (2016), nos. 1-2, pp. 94-101. · Zbl 1367.03020 |
| [57] | Jacobson, N., The radical and semi-simplicity for arbitrary rings. American Journal of Mathematics, vol. 67 (1945), no. 2, pp. 300-320. · Zbl 0060.07305 |
| [58] | Johnstone, P., Almost maximal ideals. Fundamenta Mathematicae, vol. 123 (1984), no. 3, pp. 197-209. · Zbl 0552.06004 |
| [59] | Legris, J., Paul Hertz and the origins of structural reasoning, Universal Logic: An Anthology. From Paul Hertz to Dov Gabbay (J.-Y. Béziau, editor), Studies in Universal Logic, Birkhäuser, Basel, 2012, pp. 3-10. · Zbl 1291.03005 |
| [60] | Litak, T., Polzer, M., and Rabenstein, U., Negative translations and normal modality, 2nd International Conference on Formal Structures for Computation and Deduction, LIPIcs-Leibniz International Proceedings in Informatics, vol. 84, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Wadern, 2017, Article no. 27, pp. 27:1-27:18. · Zbl 1434.03074 |
| [61] | Lombardi, H., Le contenu constructif d’un principe local-global avec une application à la structure d’un module projectif de type fini, Publications Mathématiques de Besançon: Algèbre et Théorie des Nombres, 1997, Fascicule 94-95 & 95-96.1997 · Zbl 1221.13016 |
| [62] | Lombardi, H., Relecture constructive de la théorie d’Artin-Schreier. Annals of Pure and Applied Logic, vol. 91 (1998), pp. 59-92. · Zbl 0945.03094 |
| [63] | Lombardi, H., Algèbre dynamique, espaces topologiques sans points et programme de Hilbert. Annals of Pure and Applied Logic, vol. 137 (2006), pp. 256-290. · Zbl 1077.03039 |
| [64] | Lombardi, H. and Quitté, C., Commutative Algebra: Constructive Methods. Finite Projective Modules, Algebra and Applications, vol. 20, Springer Netherlands, Dordrecht, 2015. · Zbl 1327.13001 |
| [65] | Lorenzen, P., Über halbgeordnete Gruppen. Mathematische Zeitschrift, vol. 52 (1950), no. 1, pp. 483-526. · Zbl 0035.29303 |
| [66] | Lorenzen, P., Algebraische und logistische Untersuchungen über freie Verbände. The Journal of Symbolic Logic, vol. 16 (1951), no. 2, pp. 81-106. · Zbl 0045.29502 |
| [67] | Lorenzen, P., Teilbarkeitstheorie in Bereichen. Mathematische Zeitschrift, vol. 55 (1952), no. 3, pp. 269-275. · Zbl 0048.01202 |
| [68] | Lorenzen, P., Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen. Mathematische Zeitschrift, vol. 58 (1953), no. 1, pp. 15-24. · Zbl 0051.25302 |
| [69] | Mines, R., Richman, F., and Ruitenburg, W., A Course in Constructive Algebra, Universitext, Springer, New York, 1988. · Zbl 0725.03044 |
| [70] | Mulvey, C. J. and Wick-Pelletier, J., The dual locale of a seminormed space. Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 23 (1982), no. 1, pp. 73-92. · Zbl 0475.18006 |
| [71] | Mulvey, C. J. and Wick-Pelletier, J., A globalization of the Hahn-Banach theorem. Advances in Mathematics, vol. 89 (1991), pp. 1-59. · Zbl 0745.03047 |
| [72] | Negri, S., Stone bases alias the constructive content of Stone representation, Logic and Algebra (A. Ursini and P. Aglianò, editors), Lecture Notes in Pure and Applied Mathematics, vol. 180, Marcel Dekker, New York, 1996, pp. 617-636. · Zbl 0862.03035 |
| [73] | Negri, S., Continuous domains as formal spaces. Mathematical Structures in Computer Science, vol. 12 (2002), no. 1, pp. 19-52. · Zbl 0994.06005 |
| [74] | Negri, S., Proof analysis beyond geometric theories: From rule systems to systems of rules. Journal of Logic and Computation, vol. 26 (2014), no. 2, pp. 513-537. · Zbl 1403.03116 |
| [75] | Negri, S., Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, vol. 55 (2016), nos. 3-4, pp. 461-473. · Zbl 1356.03048 |
| [76] | Negri, S. and Von Plato, J., Cut elimination in the presence of axioms, this Journal, vol. 4 (1998), no. 4, pp. 418-435. · Zbl 0934.03072 |
| [77] | Negri, S. and Von Plato, J., Structural Proof Theory, Cambridge University Press, Cambridge, 2001. · Zbl 1113.03051 |
| [78] | Negri, S. and Von Plato, J., Proof Analysis: A Contribution to Hilbert’s Last Problem, Cambridge University Press, Cambridge, 2011. · Zbl 1247.03001 |
| [79] | Negri, S. and Von Plato, J., Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen’s altitude line construction, Concepts of Proof in Mathematics, Philosophy, and Computer Science (D. Probst and P. Schuster, editors), Ontos Mathematical Logic, vol. 6, Walter de Gruyter, Berlin, 2016, pp. 269-290. · Zbl 1433.03135 |
| [80] | Negri, S., Von Plato, J., and Coquand, T., Proof-theoretical analysis of order relations. Archive for Mathematical Logic, vol. 43 (2004), pp. 297-309. · Zbl 1062.03055 |
| [81] | Neuwirth, S., Lorenzen’s theory of divisibility in monoid-preordered sets, preprint, 2018. Available at https://lmb.univ-fcomte.fr/IMG/pdf/lorenzen_s_theory_of_divisibility_in_monoid_preordered_sets.pdf. |
| [82] | Ono, H., Glivenko theorems revisited. Annals of Pure and Applied Logic, vol. 161 (2009), no. 2, pp. 246-250. · Zbl 1181.03021 |
| [83] | Payette, G. and Schotch, P. K., Remarks on the Scott-Lindenbaum theorem. Studia Logica, vol. 102 (2014), no. 5, pp. 1003-1020. · Zbl 1329.03088 |
| [84] | Pereira, L. C. and Haeusler, E. H., On constructive fragments of classical logic, Dag Prawitz on proofs and meaning, Outstanding Contributions to Logic, vol. 7, Springer, Cham, 2015, pp. 281-292. · Zbl 1429.03059 |
| [85] | Popper, K. R., On the theory of deduction, Part I. Derivation and its generalizations. Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, vol. 51 (1948), no. 2, pp. 173-183. |
| [86] | Popper, K. R., On the theory of deduction, Part II. The definitions of classical and intuitionist negation. Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, vol. 51 (1948), no. 3, pp. 322-331. · Zbl 0030.10106 |
| [87] | Rathjen, M., Generalized inductive definitions in constructive set theory, From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics (L. Crosilla and P. Schuster, editors), Oxford Logic Guides, vol. 48, Clarendon Press, Oxford, 2005, Chap. 16. · Zbl 1095.03076 |
| [88] | Restall, G., An Introduction to Substructural Logics, Routledge, London, 2000. · Zbl 1028.03018 |
| [89] | Rinaldi, D., Formal Methods in the Theories of Rings and Domains. Doctoral dissertation, Universität München, 2014. |
| [90] | Rinaldi, D. and Schuster, P., A universal Krull-Lindenbaum theorem. Journal of Pure and Applied Algebra, vol. 220 (2016), pp. 3207-3232. · Zbl 1420.03128 |
| [91] | Rinaldi, D., Schuster, P., and Wessel, D., Eliminating disjunctions by disjunction elimination. this Journal, vol. 23 (2017), no. 2, pp. 181-200. · Zbl 1455.03074 |
| [92] | Rinaldi, D., Schuster, P., and Wessel, D., Eliminating disjunctions by disjunction elimination. Indagationes Mathematicae. New Series, vol. 29 (2018), no. 1, pp. 226-259. · Zbl 1437.03163 |
| [93] | Rinaldi, D. and Wessel, D., Extension by conservation. Sikorski’s theorem. Logical Methods in Computer Science, vol. 14 (2018), nos. 4:8, pp. 1-17. · Zbl 1454.03085 |
| [94] | Rinaldi, D. and Wessel, D., Cut elimination for entailment relations. Archive for Mathematical Logic, vol. 58 (2019), nos. 5-6, pp. 605-625. · Zbl 1477.03243 |
| [95] | Sambin, G., Intuitionistic formal spaces—A first communication, Mathematical Logic and Its Applications (D. Skordev, editor), Plenum, New York, 1987, pp. 187-204. · Zbl 0703.03040 |
| [96] | Sambin, G., Pretopologies and completeness proofs. The Journal of Symbolic Logic, vol. 60 (1995), no. 3, pp. 861-878. · Zbl 0839.03022 |
| [97] | Sambin, G., Some points in formal topology. Theoretical Computer Science, vol. 305 (2003), nos. 1-3, pp. 347-408. · Zbl 1044.54001 |
| [98] | Sambin, G., The Basic Picture: Structures for Constructive Topology, Oxford Logic Guides, Clarendon Press, Oxford, 2018. |
| [99] | Sandqvist, T., Preservation of structural properties in intuitionistic extensions of an inference relation, this Journal, vol. 24 (2018), no. 3, pp. 291-305. · Zbl 1522.03317 |
| [100] | Schlagbauer, K., Schuster, P., and Wessel, D., Der Satz von Hahn-Banach per Disjunktionselimination. Confluentes Mathematici, vol. 11 (2019), no. 1, pp. 79-93. · Zbl 1480.03061 |
| [101] | Scott, D., On engendering an illusion of understanding. The Journal of Philosophy, vol. 68 (1971), pp. 787-807. |
| [102] | Scott, D., Completeness and axiomatizability in many-valued logic, Proceedings of the Tarski Symposium (L. Henkin, J. Addison, C. C. Chang, W. Craig, D. Scott, and R. Vaught, editors), Proceedings of Symposia in Pure Mathematics, Vol. XXV, American Mathematical Society, Providence, 1974, pp. 411-435. · Zbl 0318.02021 |
| [103] | Scott, D. S., Background to formalization, Truth, Syntax and Modality (H. Leblanc, editor), Studies in Logic and the Foundations of Mathematics, Vol. 68, North-Holland, Amsterdam, 1973, pp. 244-273. · Zbl 0277.02003 |
| [104] | Shoesmith, D. J. and Smiley, T. J., Multiple-Conclusion Logic, Cambridge University Press, Cambridge, 1978. · Zbl 0381.03001 |
| [105] | Takeuti, G., Proof Theory, second ed., Studies in Logic and the Foundations of Mathematics, vol. 81, North-Holland Publishing Co., Amsterdam, 1987. · Zbl 0609.03019 |
| [106] | Tarski, A., Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I. Monatshefte für Mathematik Physik, vol. 37 (1930), pp. 361-404. · JFM 56.0046.02 |
| [107] | Troelstra, A. S. and Schwichtenberg, H., Basic Proof Theory, second edition, Cambridge University Press, Cambridge, 2000. · Zbl 0957.03053 |
| [108] | Troelstra, A. S. and Van Dalen, D., Constructivism in Mathematics: An Introduction, Studies in Logic and the Foundations of Mathematics, vol. I, North-Holland, Amsterdam, 1988. · Zbl 0661.03047 |
| [109] | Troelstra, A. S., On the early history of intuitionistic logic, Mathematical Logic (P. P. Petkov, editor), Plenum Press, New York, 1990, pp. 3-17. · Zbl 0770.03002 |
| [110] | Van Atten, M. and Sundholm, G., L.E.J. Brouwer’s ‘Unreliability of the Logical Principles’: A new translation, with an introduction. History and Philosophy of Logic, vol. 38 (2017), no. 1, pp. 24-47. · Zbl 1372.01108 |
| [111] | Van Dalen, D., Logic and Structure, fifth ed., Universitext, Springer, London, 2013. · Zbl 1262.03002 |
| [112] | Wang, S.-M. and Cintula, P., Logics with disjunction and proof by cases. Archive for Mathematical Logic, vol. 47 (2008), no. 5, pp. 435-446. · Zbl 1147.03005 |
| [113] | Wessel, D., Choice, extension, conservation. From transfinite to finite proof methods in abstract algebra, Ph.D. thesis, Università degli Studi di Trento, 2018. |
| [114] | Wessel, D., Ordering groups constructively. Communications in Algebra, vol. 47 (2019), no. 12, pp. 4853-4873. · Zbl 1468.03079 |
| [115] | Wessel, D., Point-free spectra of linear spreads, Mathesis Universalis, Computability and Proof (S. Centrone, S. Negri, D. Sarikaya, and P. Schuster, editors), Synthese Library, Springer, Cham, 2019, pp. 353-374. · Zbl 1476.03078 |
| [116] | Wessel, D., A note on connected reduced rings. Journal of Commutative Algebra, vol. 13 (2021), no. 4, pp. 583-588. · Zbl 1481.13016 |
| [117] | Wójcicki, R., Theory of Logical Calculi: Basic Theory of Consequence Operations, Synthese Library, vol. 199, Kluwer Academic Publishers Group, Dordrecht, 1988. · Zbl 0682.03001 |
| [118] | Yengui, I., Making the use of maximal ideals constructive. Theoretical Computer Science, vol. 392 (2008), pp. 174-178. · Zbl 1141.13303 |
| [119] | Yengui, I., Constructive Commutative Algebra: Projective Modules over Polynomial Rings and Dynamical Gröbner Bases, Lecture Notes in Mathematics, vol. 2138, Springer, Cham, 2015. · Zbl 1360.13002 |
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.
