Algebraic Gentzen systems for partially ordered algebraic systems

The corresponding notion in logic has been very successful for formulating and implementing decision procedures for a large number of logics.

Quasi-equations rule!

A Gentzen rule is a quasi-inequality of the form

where the   s_i, t_i,   s, t   are terms.

Rules with   n = 0   are called axioms.

Gentzen rules are usually written in the form

s1 ≤ t1, ...,   sn ≤ tn     s ≤ t   name of rule.

A Gentzen system is a finite collection of Gentzen rules, including at least one axiom.

A simple example of a Gentzen system is given by the following four rules:

x ≤ x   Ax

x ≤ z     x ∧ y ≤ z      ∧ -left

y ≤ z     x ∧ y ≤ z      ∧ -left

x ≤ y,   x ≤ z     x ≤ y ∧ z      ∧ -right

These four rules give a decision procedure for the equational theory of semilattices:

If we want to decide if   s(x) ≤ t(x), match any conclusion of these rules to this inequality, and repeat this step with the premises of the rule.

If there is some choice of rules that always ends with instances of the axiom   x ≤ x, the inequality holds, and otherwise it fails.

Of course deciding semilattice equations is trivial, but this set of rules can be easily extended to cover lattices by adding the following three rules:

x ≤ y     x ≤ y ∨ z      ∨ -right

x ≤ z     x ≤ y ∨ z      ∨ -right

x ≤ z,   y ≤ z     x ∨ y ≤ z      ∨ -left

In fact this is a version of Whitman's solution of the word problem in free lattices.