TY - JOUR
T1 - A universal algorithm for Krull's theorem
AU - Powell, Thomas
AU - Schuster, Peter
AU - Wiesnet, Franziskus
N1 - Funding Information:
The authors express their gratitude to the anonymous referees, whose detailed and insightful comments improved the paper considerably. In the case of the second author, the present study was carried out within the projects “A New Dawn of Intuitionism: Mathematical and Philosophical Advances” (ID 60842 ) funded by the John Templeton Foundation , and “Reducing complexity in algebra, logic, combinatorics - REDCOM” belonging to the programme “Ricerca Scientifica di Eccellenza 2018” of the Fondazione Cariverona. The second author is member of the Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni (GNSAGA) within the Italian Istituto Nazionale di Alta Matematica (INdAM), and the third author is Marie Skłodowska-Curie fellow of INdAM. 1 1
Funding Information:
The authors express their gratitude to the anonymous referees, whose detailed and insightful comments improved the paper considerably. In the case of the second author, the present study was carried out within the projects ?A New Dawn of Intuitionism: Mathematical and Philosophical Advances? (ID 60842) funded by the John Templeton Foundation, and ?Reducing complexity in algebra, logic, combinatorics - REDCOM? belonging to the programme ?Ricerca Scientifica di Eccellenza 2018? of the Fondazione Cariverona. The second author is member of the Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni (GNSAGA) within the Italian Istituto Nazionale di Alta Matematica (INdAM), and the third author is Marie Sk?odowska-Curie fellow of INdAM.1 The opinions expressed in this paper are those of the authors and do not necessarily reflect the views of those foundations and institutions.
PY - 2022/9/30
Y1 - 2022/9/30
N2 - We give a computational interpretation to an abstract formulation of Krull's theorem, by analysing its classical proof based on Zorn's lemma. Our approach is inspired by proof theory, and uses a form of update recursion to replace the existence of maximal ideals. Our main result allows us to derive, in a uniform way, algorithms which compute witnesses for existential theorems in countable abstract algebra. We give a number of concrete examples of this phenomenon, including the prime ideal theorem and Krull's theorem on valuation rings.
AB - We give a computational interpretation to an abstract formulation of Krull's theorem, by analysing its classical proof based on Zorn's lemma. Our approach is inspired by proof theory, and uses a form of update recursion to replace the existence of maximal ideals. Our main result allows us to derive, in a uniform way, algorithms which compute witnesses for existential theorems in countable abstract algebra. We give a number of concrete examples of this phenomenon, including the prime ideal theorem and Krull's theorem on valuation rings.
KW - Constructive algebra
KW - Krull's theorem
KW - Maximal ideals
KW - Program extraction
UR - http://www.scopus.com/inward/record.url?scp=85110431925&partnerID=8YFLogxK
U2 - 10.1016/j.ic.2021.104761
DO - 10.1016/j.ic.2021.104761
M3 - Article
SN - 0890-5401
VL - 287
JO - Information and Computation
JF - Information and Computation
M1 - 104761
ER -