What is the literature on undecidable implications?

Stream: Equational

[Terence Tao]

I was trying to look up the literature on undecidability for implication in equational theories (either for magmas, or more general structures) and am struggling to find a good reference or survey. Most specifically, I am interested in whether the basic question of this project, namely whether an implication EquationX => EquationY from one magma equational law to another, is known to be undecidable in general (if we place no restrictions on the length of the laws). My vague understanding is that this is certainly known and in the literature if one considers equational theories with multiple laws and multiple symbols, but in our setting where there is just one symbol ◇ and one equation, it might not be in the literature (unless there is some sort of general trick to encode theories with many laws and symbols into a single giant law involving a single operation). I'm wondering of any participants here are well versed in universal algebra (or maybe term rewriting systems) and could give some pointers? Thanks!

[Pace Nielsen]

I'm not an expert in this area, but if I'm reading it right, the 1975 paper "On spectra, and the negative solution of the decision problem for identities having a finite nontrivial model" by Ralph McKenzie says that even deciding whether or not a single magma identity is equivalent to x=y is impossible. (Perhaps later papers clarified how many variables are needed for this.)

[Pace Nielsen]

Keith Kearnes may be a good source for information. He has answered questions on similar topics: https://math.stackexchange.com/questions/4387144/is-it-decidable-if-a-finite-set-of-equations-have-only-trivial-models

[Terence Tao]

Thanks! I should hopefully be able to citation search from that paper to get the most recent work in this area.

[Jose Brox]

Terence Tao ha dicho:

unless there is some sort of general trick to encode theories with many laws and symbols into a single giant law involving a single operation

Not an answer, and most probably you already know this, but in the very same paper you mentioned in your blog entry, Unsolvable problems for equational theories by Perkins (1967), in Theorem 14, it is shown how to encode a theory with several operations into a theory of a single binary operation (but with a law for each of the original operations), in a way that the original laws have a model iff the new laws have one.

[Jose Brox]

Jose Brox ha dicho:

Terence Tao ha dicho:

unless there is some sort of general trick to encode theories with many laws and symbols into a single giant law involving a single operation

how to encode a theory with several operations into a theory of a single binary operation (but with a law for each of the original operations), in a way that the original laws have a model iff the new laws have one.

In Perkin's paper, the encoding magma has no constants, but if one could modify his encoding in order to guarantee the existence of the identity element in the magma if the starting algebra has an identity, then any finite number of laws could be encoded into a single one, by iterating the following idea (I write 2 variables for ease): from f1(x,y)=g1(x,y) and f2(x,y)=g2(x,y), produce f1(x,y)·f2(z,w) = g1(x,y)·g2(z,w) (we recover f1=g1 from z=1=w, etc.), and one could use the undecidability result from groups, for example.