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
JournalInformation and Computation
Publication statusAcceptance date - 31 Mar 2021

Cite this