Regular entailment relations
Logic
2020-07-27 v2
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"
Keywords
Cite
@article{arxiv.1912.09480,
title = {Regular entailment relations},
author = {Thierry Coquand and Henri Lombardi and Stefan Neuwirth},
journal= {arXiv preprint arXiv:1912.09480},
year = {2020}
}