A universal algorithm for Krull's theorem

Thomas Powell; Peter Schuster; Franziskus Wiesnet

doi:10.1016/j.ic.2021.104761

A universal algorithm for Krull's theorem

Thomas Powell, Peter Schuster, Franziskus Wiesnet

Research output: Contribution to journal › Article › peer-review

3 Citations (SciVal)

93 Downloads (Pure)

Abstract

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.

Original language	English
Article number	104761
Journal	Information and Computation
Volume	287
Early online date	5 May 2021
DOIs	https://doi.org/10.1016/j.ic.2021.104761
Publication status	Published - 30 Sept 2022

Bibliographical note

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.

Funding

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 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

Keywords

Constructive algebra
Krull's theorem
Maximal ideals
Program extraction

ASJC Scopus subject areas

Theoretical Computer Science
Information Systems
Computer Science Applications
Computational Theory and Mathematics

Access to Document

10.1016/j.ic.2021.104761

accepted_manuscript_nonformatted.PDFAccepted author manuscript, 398 KB

Cite this

@article{4196e3a95385440081d6aeaaccb4fd15,

title = "A universal algorithm for Krull's theorem",

abstract = "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.",

keywords = "Constructive algebra, Krull's theorem, Maximal ideals, Program extraction",

author = "Thomas Powell and Peter Schuster and Franziskus Wiesnet",

note = "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{\l}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. ",

year = "2022",

month = sep,

day = "30",

doi = "10.1016/j.ic.2021.104761",

language = "English",

volume = "287",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "Elsevier",

}

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 -

A universal algorithm for Krull's theorem

Abstract

Bibliographical note

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this