A universal algorithm for Krull's theorem

Thomas Powell, Peter Schuster, Franziskus Wiesnet

Research output: Contribution to journalArticlepeer-review

2 Citations (SciVal)
18 Downloads (Pure)


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 languageEnglish
Article number104761
JournalInformation and Computation
Early online date5 May 2021
Publication statusPublished - 30 Sept 2022


  • 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


Dive into the research topics of 'A universal algorithm for Krull's theorem'. Together they form a unique fingerprint.

Cite this