Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Finite model theory for pseudovarieties and universal algebra: preservation, definability and complexity

Lucy Ham, Marcel Jackson

TL;DR

The paper forges a deep connection between finite model theory and universal algebra by developing toolkit results and constructing concrete examples that separate finite-level definability from classical axiomatisability. It demonstrates a finite algebra whose variety is not finitely axiomatisable in $FO$ but whose finite-membership problem is first-order definable, revealing simultaneous failures of the $S$, $SP_{fin}$ and $HSP_{fin}$ preservation theorems at the finite level and offering a negative solution to a first-order ES formulation. It also shows that CSP problems can be captured by pseudovariety membership in FO and characterizes a rich spectrum of complexity classes arising from fixed template CSP mappings, including $\text{NL}$, $\text{L}$ and $\text{Mod}_p(\text{L})$. Finally, the paper proves undecidability for the finite-level FO definability of pseudovarieties via McKenzie’s $A(\mathcal{T})$ construction, highlighting a sharp boundary between logical definability and algebraic axiomatisability with implications for both theory and complexity.

Abstract

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 Ł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ützenberger 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).

Finite model theory for pseudovarieties and universal algebra: preservation, definability and complexity

TL;DR

The paper forges a deep connection between finite model theory and universal algebra by developing toolkit results and constructing concrete examples that separate finite-level definability from classical axiomatisability. It demonstrates a finite algebra whose variety is not finitely axiomatisable in but whose finite-membership problem is first-order definable, revealing simultaneous failures of the , and preservation theorems at the finite level and offering a negative solution to a first-order ES formulation. It also shows that CSP problems can be captured by pseudovariety membership in FO and characterizes a rich spectrum of complexity classes arising from fixed template CSP mappings, including , and . Finally, the paper proves undecidability for the finite-level FO definability of pseudovarieties via McKenzie’s construction, highlighting a sharp boundary between logical definability and algebraic axiomatisability with implications for both theory and complexity.

Abstract

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 Ł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ützenberger 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 , , , , and infinitely many others (depending on complexity-theoretic assumptions).
Paper Structure (15 sections, 29 theorems, 32 equations)

This paper contains 15 sections, 29 theorems, 32 equations.

Table of Contents

  1. Introduction
  2. Computational complexity.
  3. Universal algebra.
  4. Preservation Theorems
  5. Pseudovarieties
  6. Historical note
  7. Preliminaries
  8. Varieties and other algebraic concepts
  9. First order reductions
  10. Toolkit: principal congruences and subdirect irreducibility
  11. Toolkit: Preservation Theorems
  12. Toolkit: Ehrenfeucht Fraı̈ssé games in finite algebras
  13. A first order definable pseudovariety that is not definable by a $\forall^*\exists^*$ sentence.
  14. Pseudovariety membership complexity: Constraint Satisfaction Problems
  15. Undecidability of complexity of finite membership.

Key Result

Lemma 2.4

Let $\mathscr{K}$ be a uniformly locally finite class of algebras of the same finite signature. Then the pseudovariety generated by $\mathscr{K}$ is also uniformly locally finite.

Theorems & Definitions (67)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Lemma 2.4
  • proof
  • Definition 3.1
  • Theorem 3.2
  • proof
  • Theorem 3.3
  • proof : Proof of Theorem \ref{['thm:TFPC']}.
  • ...and 57 more