Eine prädikatenlogische Theorie in einer festen algebraischen Signatur, deren Axiome ausschließlich universell quantifizierte Gleichungen zwischen Termen sind und die gegenüber der Folgerungsrelation der Gleichungslogik abgeschlossen ist.

Prinzip

Algebraische Struktur allein durch Identitäten beschreiben; Abschluss unter Substitution, Reflexivität, Symmetrie, Transitivität der Gleichheit und Kongruenzregeln liefert alle gleichunglichen Konsequenzen.

Demonstration

Die Klasse der Monoide wird durch die Gleichungstheorie mit einem binären Symbol · und einer Konstante e axiomatisiert durch (x·y)·z = x·(y·z), e·x = x, x·e = x; jedes Modell, das diese Identitäten erfüllt, ist ein Monoid.

Fehlanwendung

Eine Theorie, die Existenzquantoren verlangt (zum Beispiel 'für jedes Element existiert ein Inverses'), als gleichungstheoretisch bezeichnen, obwohl das Inverse nicht als Funktionssymbol eingeführt ist; oder nicht-gleichungstheoretische Axiome wie Ordnungsrelationen hinzunehmen.

Konsequenz

Die Modellklasse ist eine Varietät: abgeschlossen unter homomorphen Bildern, Teilalgebren und beliebigen direkten Produkten; Gleichungstheorien besitzen freie Algebren und syntaktische Vollständigkeit bezüglich gleichunglicher Folgerung.

Umkehrung

Eine allgemeine prädikatenlogische Theorie, die Relationen, Existenzquantoren oder Disjunktionen verwendet — eine solche Theorie ist nicht gleichungstheoretisch, da ihre Axiome sich nicht ausschließlich als universelle Gleichungen schreiben lassen.

Abgrenzung

Beschränkt auf Signaturen mit Funktionssymbolen und Axiome, die universell quantifizierte Gleichungen sind; schließt Axiome aus, die Existenz behaupten, Ungleichheiten, Ordnungen oder relationale Einschränkungen, die nicht identitätsäquivalent sind.

Semantische Spannung

Zwischen Gleichungstheorien und universellen Horn-Theorien: Jede Gleichungstheorie ist eine universelle Horn-Theorie, aber universelle Horn-Theorien können Implikationen zwischen Gleichungen ausdrücken, die nicht auf reine Identitäten reduzierbar sind.

Synthese

Eine Gleichungstheorie ist das syntaktische Paket von Identitäten, das eine Varietät definiert: die rein gleichungsbasierte Spezifikation, deren Modelle eine nach Homomorphismen, Teilalgebren und Produkten abgeschlossene Klasse bilden und die freie Objekte aus syntaktischen Termen besitzt.