If finitely many algebraic identities do not imply some identity, is there always a finite counterexample?

Question

This question just popped up while experimenting with Prover9 and Mace4.

Say we have a finite signature and some finite set of identities $E_i$ in the sense of universal algebra, like the axioms for groups.

$$\left\{\begin{matrix}x\cdot(y\cdot z) = (x \cdot y) \cdot z \\ x\cdot 1 = 1 \cdot x = x \\ x\cdot x^{-1} = x^{-1} \cdot x = 1\end{matrix}\right.$$

If some other identity $J$ does not follow from the $E_i$, is there always a counterexample on a finite set? Like if we want to deduce $x\cdot y = y \cdot x$, we have the nonabelian finite counterexample $S_3$, or for $x=y$ we already have $\mathbb Z/(2)$.

This is basically what Mace4 tries to find, so could this approach in theory be always successful? (Even through the counterexample might be too large for a computer to find)

---

My initial suspicion was no, but the counterexamples I was trying don't quite fit the strong restrictions of the question.

• Like for the axioms of a skew field, it does not follow that $xy = yx$, but there is no finite counterexample. However, skew fields cannot be axiomatized by identities only.

• For $\mathbb R$-vector spaces, it does not follow that $x=y$ and there is no finite counterexample. However, signature and axiom set for $\mathbb R$-vector spaces are infinite.

I know if $J$ does not follow from the $E_i$, the set of formulas $\{E_i\} \cup \{\neg J\}$ is consistent, hence does have a model. If it is finite, we're done. If it is infinite, we can assume it to be countable by Löwenheim-Skolem. However in the form of question, where all $E_i$ are universal and just $\neg J$ is a negation of an identity, is there always a finite model?

Thanks for some thoughts

Answer 1

Lattice-ordered groups are all either infinite or trivial ($\forall x\forall y(x = y)$). They can be defined equationally by adding a least upper bound operator $\land$ to the signature of a group and adding to the identities that characterize groups, identities saying that $\land$ is idempotent, commutative and associative and that the group operation distributes through it. Even with unlimited memory and time, a program like Mace4 would not be able to find a counter-example to $x + x = x$.

A theory characterized by a finite set of identities has the property that every identity is either valid or has a counter-example in a finite model, then that theory is decidable: to decide a property, run an attempt to find a proof of it in parallel with an attempt to find a finite counter-example. Provided you schedule the two searches fairly, the parallel search process must terminate with either a proof or a counter-example.