Induction in algebra: a first case study

DOI10.2168/LMCS-9(3:20)2013MaRDI QIDQ2848365zbMATH OpenOpenAlexWikidataFDO

Authors Peter Schuster

Publication date 26 September 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1308.2690

zbMATH Keywords

constructive algebraHilbert's programmeintuitionistic logicopen inductionZorn's lemma

Mathematics Subject Classification ID

Axiom of choice and related propositions (03E25) Other constructive mathematics (03F65) Lattice ideals, congruence relations (06B10) Noether lattices (06F10) Computational aspects of associative rings (general theory) (16Z05) Symbolic computation and algebraic computation (68W30)

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

Recommendations

• Induction in algebra: a first case study
• Proofs by induction in equational theories with constructors
• Constructive algebra
• scientific article; zbMATH DE number 4074451
• Automatic proofs by induction in theories without constructors

Cited in

(23)

• Eliminating disjunctions by disjunction elimination
• Dynamic evaluation of integrity and the computational content of Krull's lemma
• Maximal ideals in countable rings, constructively
• The computational significance of Hausdorff's maximal chain principle
• A universal algorithm for Krull's theorem
• A direct proof of Wiener's theorem
• Induction in algebra: a first case study
• Lindenbaum's lemma via open induction
• Syntax for semantics: Krull's maximal ideal theorem
• The Jacobson radical for an inconsistency predicate
• Resolving finite indeterminacy. A definitive constructive universal prime ideal theorem
• Eliminating disjunctions by disjunction elimination
• Constructive analysis of maximal ideals in \(\mathbb{Z}[X]\) by the material interpretation
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• Defining long words succinctly in FO and MSO
• On the first-order parts of problems in the Weihrauch degrees
• Algorithmically random series
• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• Lower bounds on () and other properties of -register machines
• Reifying dynamical algebra: maximal ideals in countable rings, constructively
• The basic Zariski topology

This page was built for publication: Induction in algebra: a first case study

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848365)