7
$\begingroup$

Suppose we are given a variety in the universal algebra sense.

For concreteness, suppose that we have two binary operations $+,\cdot$, three unary operations $-,\ast,'$, and two zeroary operations $0,1$. Also, we have the (unital, associative, noncommutative) ring identities, as well as the identities of a $\ast$-ring, together with the four identities $$ xx'x=x,\ x'xx'=x',\ (xx')^{\ast}=xx',\ (x'x)^{\ast}=x'x. $$

There is another, specific identity that I wonder if it is a consequence of the given identities, namely setting $x:=a' + (1 - a'a)(1 + a)'(1 - aa')$, then I wonder if $$ xx'=1. $$

My question is whether there is some computer algebra system (in actual existence, I already know that such a system can exist abstractly) that searches for a proof of this new identity (and perhaps, as an added benefit, searches for disproofs too). In other words, is there a decent (hopefully freely available) automatic theorem prover that does the given task; something similar to the program used to show how Robbin's identity in Boolean algebras can be used to get the other identities.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
9
$\begingroup$

The general problem is undecidable, as is shown in

Peter Perkins
Unsolvable problems for equational theories
Notre Dame Journal of Formal Logic
Volume VIII, Number 3, July 1967

Perkins shows that one cannot decide whether an arbitrary finite set of equations in one binary operation symbol entails $x\approx y$.

But there is software that searches for equational proofs. I have been meaning to experiment with Prover9, but haven't gotten around to it yet. It is supposed to be able to produce readable proofs in equational logic. Prover9 is used together with Mace4, which searches for countermodels.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I tried downloading the GUI for Prover9 from your given link, but that didn't work. I found another place to download the GUI, but after installation the program wouldn't run. $\endgroup$
    – Pace Nielsen
    Commented Jan 1, 2023 at 21:52
6
$\begingroup$

It is not completely clear from the question whether you view the finite set of identities as part of the input or not. @KeithKearnes answer has the finite list as part of the input (and the identity to be a consequence is fixed). Murskii proved (V. L. Murskii, “Some examples of semigroup varieties,” Mat. Zametki, 3, No. 6, 663-670 (1968)) that there is a fixed finite set of semigroup identities so that the consequences of that fixed set of identities is undecidable. The corresponding result for varieties of group was given in Yu. G. KLEIMAN, Identities and some algorithmic problems in groups, Doklady Akademii Nauk SSSR, vol. 244 (1979), pp. 814-818.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I've tried to clarify. I do have access to the identities of the variety, as well as the identity I hope is a consequence. I'm aware of the recursive enumerability (without full decidability) issues involved. My question is whether there is a (hopefully freely available, decent) computer algebra system to look for derivations of the hoped identity. $\endgroup$
    – Pace Nielsen
    Commented Jan 1, 2023 at 22:01
  • 1
    $\begingroup$ The reformulation of course takes decidability out since you have a single instance of the problem. $\endgroup$
    – Benjamin Steinberg
    Commented Jan 2, 2023 at 1:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .