Peter Schuster: When Irreducibles are Prime

Many an indirect proof with Zorn's Lemma has recently allowed for being turned upside down into a direct proof with Raoult's Open Induction; case studies pertain to commutative rings [1] and Banach algebras [2]. Under sufficiently concrete circumstances this may even yield a constructive proof without any form of the Axiom of Choice. To prepare the ground for a more systematic treatment we now classify the cases that can be found in mathematical practice by way of representative proof patterns. To start with we distill, and prove by Open Induction, a generalised form of the contrapositive of the Separation Lemma or Prime Ideal Theorem that is ascribed to Lindenbaum, Krull, Stone, and Tarski. Our version subsumes not only instances from diverse branches of abstract algebra but also a Henkin-style completeness proof for first-order logic. By recurrence to a theorem of McCoy, Fuchs, and Schmidt on irreducible ideals we further shed light on why prime ideals occur --- and why transfinite methods. (This is joint work in progress with D. Rinaldi, Munich, and is partially based on joint work with N. Gambino, Palermo, and F. Ciraulo, Padua.)

[1] P. Schuster, Induction in algebra: a first case study. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 2012, Dubrovnik, Croatia. IEEE Computer Society Publications (2012) 581-585

[2] M. Hendtlass, P. Schuster, A direct proof of Wiener's theorem. In: S.B. Cooper, A. Dawar, B. Loewe, eds., How the World Computes. Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, Cambridge, UK, June 2012, Proceedings. Springer, Berlin and Heidelberg. Lect. Notes Comput. Sci. 7318 (2012) 294-303