Regular entailment relations
Thierry Coquand, Henri Lombardi (LMB), Stefan Neuwirth (LMB)

TL;DR
This paper introduces regular entailment relations inspired by Lorenzen's work, establishing a key theorem and connecting them with Lorenzen's systems of ideals through a regularisation process, emphasizing constructive and transparent concepts.
Contribution
It defines regular entailment relations, proves a fundamental theorem, and links them with Lorenzen's ideals via regularisation, advancing the theoretical framework.
Findings
Established a crucial theorem for regular entailment relations
Connected regularisation process with Lorenzen's systems of ideals
Provided constructive objects and arguments for clarity
Abstract
Inspired by the work of Lorenzen on the theory of preordered groups in the forties and fifties, we define regular entailment relations and show a crucial theorem for this structure. We also describe equivariant systems of ideals {\`a} la Lorenzen and show that the remarkable regularisation process invented by him yields a regular entailment relation. By providing constructive objects and arguments, we pursue Lorenzen's aim of "bringing to light the basic, pure concepts in their simple and transparent clarity"
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsRings, Modules, and Algebras · Commutative Algebra and Its Applications · Homotopy and Cohomology in Algebraic Topology
