A universal algorithm for Krull's theorem

Thomas Powell, Peter Schuster, Franziskus Wiesnet

Research output: Contribution to journalArticlepeer-review


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 statusE-pub ahead of print - 5 May 2021


  • 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