Induction in Algebra: a First Case Study

TL;DR

This paper explores how certain algebraic theorems traditionally proved using Zorn's Lemma can instead be derived through the Principle of Open Induction, enabling constructive and intuitionistic proofs especially for finite cases.

Contribution

It introduces a new approach to algebraic proofs by replacing Zorn's Lemma with Open Induction, making some theorems constructively provable and simplifying their logical foundations.

Findings

Finite input data allows constructive induction proofs.

Theorem on nilpotent coefficients of invertible polynomials is constructively proved.

Elimination of classical Zorn's Lemma in favor of Open Induction.

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 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".