🚀 go-pugleaf

In article <ALTI.92Dec14145206@campay.dcs.ed.ac.uk> alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:
>In article <1g282rINN5ja@eagle.dfki.uni-sb.de> treinen@dfki.uni-sb.de (Ralf Treinen) writes:
>
>   In article <19921208.075322039663.NETNEWS@ALIJKU11>, groda@risc.uni-linz.ac.at (Giovanna Roda) writes:
>   |> Suppose we are given an axiomatization for the theory of groups consisting
>   |> of the following three axioms:
>   |> (x*y)*z=x*(y*z)
>   |> Vy x=y*z
>   |> Vz x=y*z
>   |> (where V is the existential quantifier).
>   |> Is this theory decidable?
>
>   No. This has been proven in
>
>   @InCollection{Tar:groups53,
>   author	= "Alfred Tarski",
>   title	= "Undecidability in the Elementary Theory of Groups",
>   pages	= "75--87",
>   crossref= "TMR:Undecidable53"
>   }
>
>No I am slightly confused. Am I wrong remembering that the followoing
>presentation of groups
>
>	(x*y)*z=x*(y*z)
>	x*e = x
>	e*x = x
>	i(x)*x = e
>	x*i(x) = e
>
>could be completed using the Knuth-Bendix algorithm & therefore is
>decidable. How does this relate to the above mentioned result?

Both are correct.  The former refers to the undecidability of the
universal Horn theory of groups (the "uniform word problem"), the
latter to the decidability of their equational theory.

Background: Given any set G of formulas, consider the theory T(G)
consisting of all first order consequences of G.  For example when G is
the above set of equations, T(G) is the elementary theory of groups.

Now select from T(G) its universal Horn formulas, universally
quantified implications from a conjunction of atomic formulas to a
single atomic formula.  If all members of G are of this form then these
form the universal Horn theory of G, groups in the above example.

Lastly select just the single equations.  If all members of G are
equations then these form the equational theory of G.

Each restriction on the language results in a reduction (not
necessarily strict) in the complexity of the associated decision
problem, since by construction the associated extensions are
conservative, whether or not any axioms of G were discarded.  (This is
in contrast to the more general situation of taking an arbitrary
subtheory; a decidable theory T may well have an undecidable subtheory
T', but in that case T necessarily does not conservatively extend T'.)

Irrelevant to the above, but worth mentioning now that we've come this
far, is that the respective kinds of classes definable by these logical
frameworks are the elementary classes, the quasivarieties (in the case
where the atomic formulas are all equations, as here), and the
varieties.  Each of these classes has an independent characterization
in terms of its closure properties.  An elementary class is one that is
closed under isomorphisms, elementary substructures, and
ultraproducts.  A quasivariety is an pseudoelementary class (one that
is the result of contracting the language of an elementary class) that
is closed under isomorphisms, subalgebras and direct products.  A
variety is a class that is closed under subalgebras, direct products,
and formation of homomorphic images.
-- 
Vaughan Pratt				There's safety in certain numbers.