Una teoría de primer orden cuyos axiomas son exclusivamente ecuaciones entre términos sobre una firma; sus modelos son precisamente las álgebras en las que las identidades enunciadas se cumplen universalmente.

Principio

Usar axiomas ecuacionales (identidades) como única forma de aserción de modo que las deducciones se basen en sustitución, reflexividad, simetría, transitividad y reglas de congruencia para términos; las teorías ecuacionales corresponden a clases cerradas bajo los operadores de cierre ecuacional del álgebra universal.

Demostración

La teoría ecuacional de los semigrupos es el conjunto de todas las identidades en la operación binaria que son verdaderas en todo semigrupo (por ejemplo, la asociatividad como axioma básico); comprobar si una identidad dada se sigue de la teoría puede reducirse a manipulaciones en álgebras de términos libres o mediante técnicas de reescritura de palabras adaptadas a la firma.

Aplicación incorrecta

Esperar que las teorías ecuacionales capten propiedades que requieren cuantificadores existenciales (como ‘existe un elemento idempotente’ salvo que los idempotentes se definan funcionalmente) o relaciones de orden; intentar axiomatizar tales propiedades solo por identidades suele fallar u obligar a codificaciones artificiosas.

Consecuencia

Las teorías ecuacionales aportan consecuencias algebraicas robustas: garantizan la existencia de álgebras libres, permiten métodos algorítmicos de reescritura y unificación de términos, y generan construcciones de congruencias y cocientes gobernadas por ecuaciones sintácticas.

Inversión

Reemplazar axiomas ecuacionales por oraciones arbitrarias de primer orden aumenta la potencia expresiva (se puede afirmar existencia y propiedades de orden) pero se pierden muchas ventajas ecuacionales como las construcciones libres directas y la deducción ecuacional puramente sintáctica.

Límite

Se aplica estrictamente a axiomas que son ecuaciones universalmente cuantificadas entre términos en una firma fija; excluye implicaciones Horn no equivalentes a conjuntos de identidades, aserciones existenciales y propiedades esencialmente de segundo orden o que impliquen relaciones no funcionales salvo que se codifiquen como operaciones.

Tensión semántica

Existe tensión entre la naturaleza decidible y sintáctica de la consecuencia ecuacional y la semántica más rica de teorías completas de primer orden: algunos fenómenos algebraicos naturales no son expresables ecuacionalmente, forzando un compromiso entre expresividad y simplicidad del cierre algebraico.

Síntesis

Una teoría ecuacional consiste en identidades que restringen de forma uniforme las operaciones por términos en una firma; sus modelos forman una clase cerrada ecuacionalmente con objetos libres y métodos sintácticos algorítmicos para derivar identidades, sosteniendo gran parte del razonamiento en álgebra universal.