Term inequalities in finite algebras

TL;DR

This paper proves that if two terms are separated in any algebra, they are also separated in some finite algebra, and shows that certain universally quantified negated formulas are satisfiable iff they have finite models.

Contribution

It establishes the existence of finite models for separated terms and for universally quantified negated formulas, connecting algebraic separation with finite model theory.

Findings

Separated terms in any algebra are separated in some finite algebra.

Universally quantified negated formulas are satisfiable iff they have finite models.

Abstract

Given an algebra $\mathbf{A}$, and terms $s(x_{1},x_{2},\dots x_{k})$ and $t(x_{1},x_{2},\dots x_{k})$ of the language of ${\mathbf A}$, we say that $s$ and $t$ are {\em separated} in ${\mathbf A}$ iff for all $a_{1},a_{2}\dots a_{k}\in A$, $s(a_{1},a_{2},\dots a_{k})$ and $t(a_{1},a_{2},\dots a_{k})$ are never equal. We prove that given two terms that are separated in any algebra, there exists a finite algebra in which they are separated. As a corollary, we obtain that whenever the sentence $\sigma$ is a universally quantified conjunction of negated atomic formulas, $\sigma$ is consistent iff it has a finite model.