Proving open properties by induction

DOI10.1016/0020-0190(88)90126-3MaRDI QIDQ1112816zbMATH OpenOpenAlexFDO

Authors Jean Claude Raoult

Publication date 1988

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(88)90126-3

zbMATH Keywords

complete partial ordereffective proofnoetherian inductionordered setwell-quasi-order

Mathematics Subject Classification ID

Axiom of choice and related propositions (03E25) Partial orders, general (06A06)

Review text

The author defines a concept of noetherian induction, which generalizes strong induction for natural numbers and transfinite induction, and, in a certain sense, is shown to be the most general type of induction. He also shows that in a complete partial order (every nonempty chain has a least upper bound) for a property which is inductive and open, the set of elements satisfying it is open in the lower topology (in which subsets are closed if they contain the least upper bound of their directed subsets).

Recommendations

• A calculational approach to mathematical induction
• scientific article; zbMATH DE number 5269389
• A uniform approach to inductive posets and inductive closure
• scientific article; zbMATH DE number 1841837
• Recursion, induction and well-founded orders

Cites work

• scientific article; zbMATH DE number 3706504 (Why is no real title available?)
• scientific article; zbMATH DE number 3227055 (Why is no real title available?)
• The varieties of arboreal experience
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(23)

• Eliminating disjunctions by disjunction elimination
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• The computational significance of Hausdorff's maximal chain principle
• On induction principles for partial orders
• Programs from proofs using classical dependent choice
• A universal algorithm for Krull's theorem
• A universal Krull-Lindenbaum theorem
• Certified Kruskal's tree theorem
• Well quasi-orders and the functional interpretation
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Lindenbaum's lemma via open induction
• On the constructive and computational content of abstract mathematics
• Decision procedure of some relevant logics: a constructive perspective
• scientific article; zbMATH DE number 4033743 (Why is no real title available?)
• The equivalence of bar recursion and open recursion
• Syntax for semantics: Krull's maximal ideal theorem
• The Jacobson radical for an inconsistency predicate
• An induction principle over real numbers
• Eliminating disjunctions by disjunction elimination
• Open Induction
• Constructing Gröbner bases for Noetherian rings
• Some new double induction and superinduction principles
• Coq formalization of the higher-order recursive path ordering

Describes a project that uses

Uses Software

• Open Induction

This page was built for publication: Proving open properties by induction

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