We explore new interactions between finite model theory and a number of classical streams of universal algebra and semigroup theory. A key result is an example of a finite algebra whose variety is not finitely axiomatisable in first order logic, but which has first order definable finite membership problem. This algebra witnesses the simultaneous failure of the {\L}os-Tarski Theorem, the SP-preservation theorem and Birkhoff's HSP-preservation theorem at the finite level as well as providing a negative solution to a first order formulation of the long-standing Eilenberg Sch\"utzenberger problem. The example also shows that a pseudovariety without any finite pseudo-identity basis may be finitely axiomatisable in first order logic. Other results include the undecidability of deciding first order definability of the pseudovariety of a finite algebra and a mapping from any fixed template constraint satisfaction problem to a first order equivalent variety membership problem, thereby providing examples of variety membership problems complete in each of the classes $\texttt{L}$, $\texttt{NL}$, $\texttt{Mod}_p(\texttt{L})$, $\texttt{P}$, and infinitely many others (depending on complexity-theoretic assumptions).
翻译:我们探索了有限模型理论与泛代数及半群理论中若干经典分支之间的新交互。关键结果是一个有限代数的实例,其簇在一阶逻辑中不是有限可公理化的,但其有限成员判定问题是一阶可定义的。该代数同时见证了Łos-Tarski定理、SP保持定理和Birkhoff的HSP保持定理在有限层级的失效,并为长期存在的Eilenberg-Schützenberger问题的一阶形式化给出了否定解。该实例还表明,无有限伪等式基的伪变种可能在一阶逻辑中有限可公理化。其他结果包括:判定有限代数的伪变种是否为一阶可定义的问题是不可判定的,以及从任意固定模板约束满足问题到一阶等价的簇成员判定问题的映射,从而在类$\texttt{L}$、$\texttt{NL}$、$\texttt{Mod}_p(\texttt{L})$、$\texttt{P}$及无限多个其他类(依赖于复杂性理论假设)中各提供了完备的簇成员判定问题实例。