A universal algorithm for Krull's theorem (Q2672666)

In analyzing integers, it is often useful to take into account that every integer can be uniquely represented as a product of primes. In many other commutative rings, it is not possible to select similar ``prime'' elements, but it turns out to be possible to have a similarly convenient representation by using additional ``ideal'' elements -- known as \textit{ideals}. Formally, an ideal is a set which is closed under addition and multiplication. In the integer case, an integer \(n\) corresponds to the ideal \(n{\mathbb Z}\) of all the integers which are divisible by \(n\). Ideals corresponding to a prime integer \(n\) have the property that if this ideal contains the product \(a\cdot b\), then it contains one of the factors; in the general case, this property is used as the definition of a \textit{prime ideal}. An ideal \(I\) is called \textit{radical} (from \textit{radix} -- the Latin word for root) if it is closed under taking roots, i.e., if whenever \(a^k\in I\) for some \(k\), we also have \(a\in I\). Integers have the following simple property: if a number \(r\) is divisible by all the prime factors of \(n\), then some power of \(r\) is divisible by \(n\); a similar property holds for subsets of \(\mathbb Z\). A natural generalization of this result to general commutative rings \(S\) is known as \textit{Krull's theorem}: for every set \(F\subseteq S\), if an element \(r\) is contained in all prime ideals containing \(F\), then \(r\) is also contained in the radical ideal generated by \(F\) -- i.e., in the intersection of all radical ideals containing \(F\). The usual proof of Krull's theorem is not constructive. The authors provide a constructive proof. Interestingly, this proof works not only for rings, but also in a more general context of an inference-type relation \(A\triangleright a\) between finite subsets \(A\subseteq S\) and elements \(a\in S\) -- namely, a relation for which \(\{a\}\triangleright a\), and for which \(B\triangleright b\) and \(A\cup \{b\}\triangleright a\) imply \(A\cup B\triangleright a\). The \textit{closure} \(\langle U\rangle\) is naturally defined as the set of all \(a\in S\) for which \(A\triangleright a\) for some \(A\subseteq S\). ``Closed'' sets -- i.e., sets for which \(\langle U\rangle=U\) -- are natural analogs of radical ideals and are thus called \textit{\(\triangleright\)-ideals}. Multiplication \(a\circ b\) is a binary operation for which \(A\cup \{a\}\triangleright c\) and \(B\cup \{b\} \triangleright c\) imply that \(A\cup B\cup \{a\circ b\}\triangleright c\). Prime \(\triangleright\)-deals are defined as usual. Then if we replace, in the formulation of Krull's theorem, radical ideals with \(\triangleright\)-ideals, we get a general result which is also true. The authors prove a constructive version of this general result. Specifically, they assume that the underlying set \(S\) is countable, \(S=\{s_0,s_1,\ldots\}\), and that the relation \(A\triangleright a\) has the form \(\exists x\,(A\triangleright_x a)\) for some ternary primitive recursive relation \(A\triangleright_x a\). As usual in constructive math, they interpret implication \(p\to q\) as the existence of an algorithm transforming a witness \(x\) for the condition \(p\) into a witness for the conclusion \(q\). The authors then provide an algorithm that inputs the witness for the condition of the generalized Krull's theorem and generates the witness for the theorem's conclusion. Several interesting particular cases are presented.