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
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.