An algorithmic approach to the existence of ideal objects in commutative algebra
Authors:
Thomas Powell,
Peter M Schuster,
Franziskus Wiesnet
Abstract:
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, wh…
▽ More
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, which focuses on the elimination of ideal objects via syntactic methods. In this paper, we take an alternative approach based on Kreisel's no counterexample interpretation and sequential algorithms. We first give a computational interpretation to an abstract maximality principle in the countable setting via an intuitive, state based algorithm. We then carry out a concrete case study, in which we give an algorithmic account of the result that in any commutative ring, the intersection of all prime ideals is contained in its nilradical.
△ Less
Submitted 7 March, 2019;
originally announced March 2019.
Induction in Algebra: a First Case Study
Authors:
Peter M Schuster
Abstract:
Many a concrete theorem of abstract algebra admits a short and elegant proof by contradiction but with Zorn's Lemma (ZL). A few of these theorems have recently turned out to follow in a direct and elementary way from the Principle of Open Induction distinguished by Raoult. The ideal objects characteristic of any invocation of ZL are eliminated, and it is made possible to pass from classical to in…
▽ More
Many a concrete theorem of abstract algebra admits a short and elegant proof by contradiction but with Zorn's Lemma (ZL). A few of these theorems have recently turned out to follow in a direct and elementary way from the Principle of Open Induction distinguished by Raoult. The ideal objects characteristic of any invocation of ZL are eliminated, and it is made possible to pass from classical to intuitionistic logic. If the theorem has finite input data, then a finite partial order carries the required instance of induction, which thus is constructively provable. A typical example is the well-known theorem "every nonconstant coefficient of an invertible polynomial is nilpotent".
△ Less
Submitted 20 September, 2013; v1 submitted 12 August, 2013;
originally announced August 2013.
