Cut elimination for entailment relations

Entailment relations, introduced by Scott in the early 1970s, provide an abstract gen- eralisation of Gentzen’s multi-conclusion logical inference. Originally applied to the study of multi-valued logics, this notion has then found plenty of applications, ranging from computer science to abstract algebra. In particular, an entailment relation can be regarded as a constructive presentation of a distributive lattice and in this guise it has proven to be a useful tool for the constructive reformulation of several classical theorems in commutative algebra. In this paper, motivated by these concrete applica- tions, we state and prove a cut-elimination result for inductively generated entailment relations. We analyse some of its consequences and describe the existing connections with analogous results in the literature.