<p> <b>Algebraic Gentzen systems for partially ordered algebraic systems</b><p> The corresponding notion in logic has been very successful for formulating and implementing decision procedures for a large number of logics. <p> <!--In universal algebra there are several methods for showing that an equational theory is decidable. <ol> <li> The finite model property (FMP): Every identity that fails in some model fails in a finite one. Equivalently: the variety is generated by it's finite members. The name comes from logic. <li> The finite embedding property (FEP): Every finite partial algebra that satisfies the identities (whenever both sides are defined) can be embedded in a finite member of the variety. <li> Use the Knuth-Bendix algorithm to derive a confluent terminating rewrite system from a finite equational basis. <li> Find some adhoc normal form. E.g. disjunctive or conjunctive normal form in Boolean algebras. <li> Show that the variety is locally finite with computable upper bound on the size of the `n`-generated free algebra. <li> If the algebras have a definable partial order, give an algorithm for deciding when one term is below another. E.g. Whitman's solution of the word problem in free lattices. </ol> Here we look more closely at the (2nd) last method. Gentzen systems essentially are a general approach for partially ordered algebraic systems.--> <p> <p>  <p>  <p>  <p>  <p>  <p>  <p> <b>Quasi-equations rule!</b> <p> A <em>Gentzen rule</em> is a quasi-inequality of the form <p> <center> `s_1<=t_1 and ... and s_n<=t_n implies s<=t` </center> <p> where the `s_i,t_i`,`s,t` are terms. <p> Rules with `n=0` are called <em>axioms</em>. <p> Gentzen rules are usually written in the form<br> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `s_1<=t_1`, ...,`s_n<=t_n` <hr NOSHADE> `s <= t`<br> </td><td nowrap align=center>name of rule.</td> </table> </td> </table> A <em>Gentzen system</em> is a finite collection of Gentzen rules, including at least one axiom. <p> A simple example of a Gentzen system is given by the following four rules: <p> <table border=2 align=center> <tr> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center>   <hr NOSHADE> `x <= x`<br> </td><td nowrap align=center>Ax</td> </table> </td> </table> </td> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `x<=z` <hr NOSHADE> `x^^y <= z`<br> </td><td nowrap align=center>`^^`-left</td> </table> </td> </table> </td> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `y<=z` <hr NOSHADE> `x^^y <= z`<br> </td><td nowrap align=center>`^^`-left</td> </table> </td> </table> </td> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `x<=y`, `x<=z` <hr NOSHADE> `x <= y^^z`<br> </td><td nowrap align=center>`^^`-right</td> </table> </td> </table> </td> </tr> </table> <p> These four rules give a decision procedure for the equational theory of semilattices: <p> 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. <p> If there is some choice of rules that always ends with instances of the axiom `x<=x`, the inequality holds, and otherwise it fails. <p> Of course deciding semilattice equations is trivial, but this set of rules can be easily extended to cover <b>lattices</b> by adding the following three rules: <p> <table border=2 align=center> <tr> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `x<=y` <hr NOSHADE> `x <= y vv z`<br> </td><td nowrap align=center>`vv`-right</td> </table> </td> </table> </td> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `x<=z` <hr NOSHADE> `x <= y vv z`<br> </td><td nowrap align=center>`vv`-right</td> </table> </td> </table> </td> <td> <table align="center"> <tr><td> <table align="center"> <tr><td nowrap align=center> `x<=z`, `y<=z` <hr NOSHADE> `x vv y <= z`<br> </td><td nowrap align=center>`vv`-left</td> </table> </td> </table> </td> </tr> </table> <p> In fact this is a version of Whitman's solution of the word problem in free lattices.