Algebras (f.o. structures with no relational symbols, in this talk in a finite language) are often classified by the identities they fulfil. For a finite set \(\Sigma\) of identities, the set of identities that follow from \(\Sigma\) is r.e. but not necessarily decidable. However, if \(\Sigma := \operatorname{Th}_{\mathrm{eq}} (\mathbf{A})\) is the equational theory of a single finite algebra \(\mathbf{A}\), then membership in \(\Sigma\) is clearly decidable: Given \(\varphi\), just check whether \(\varphi\) holds in \(\mathbf{A}\). We will discuss a result by Peter Mayr and the speaker that yields the following consequence:
If \(\mathbf{A}\) has a Mal'cev term, i.e., a term operation satisfying \(t(x,x,y) = t (y,x,x) = y\), then for every set \(\Gamma\), the set of consequences of \(\operatorname{Th}_{\mathrm{eq}} (\mathbf{A}) \, \cup \, \Gamma\) is decidable.
The main tool is the representation of \(\Gamma\) by functions on \(\mathbf{A}\).
In contrast, many other properties of a finite algebra, such as the equational theory having a finite basis, have been proven to be undecidable by Ralph McKenzie's construction of finite algebras representing Turing–machines. We will seek advice on how to deal with algebras whose finite basedness is therefore not determined by \(\operatorname{ZFC}\).