Eine erste‑Ordnung‑Theorie, deren Axiome ausschließlich Gleichungen zwischen Termen über einer Signatur sind; ihre Modelle sind genau die Algebren, in denen die angegebenen Identitäten universell gelten.

Prinzip

Verwende äquationale Axiome (Identitäten) als einzige Form der Behauptung, sodass Schlussfolgerungen auf Substitution, Reflexivität, Symmetrie, Transitivität und Kongruenzregeln für Terme beruhen; äquationale Theorien entsprechen Klassen, die unter den äquationalen Abschlussoperatoren der universellen Algebra stehen.

Demonstration

Die äquationale Theorie der Halbgruppen ist die Menge aller Identitäten der binären Operation, die in jeder Halbgruppe gelten (z. B. Assoziativität als Grundaxiom); die Frage, ob eine gegebene Identität aus der Theorie folgt, lässt sich auf Manipulationen in freien Termalgebren oder auf Wortumformungstechniken für die Signatur zurückführen.

Fehlanwendung

Zu erwarten, äquationale Theorien erfassten Eigenschaften, die Existenzquantoren erfordern (etwa ‚es existiert ein idempotentes Element‘, sofern Idempotenten nicht als Funktionen definiert sind) oder Ordnungsrelationen; der Versuch, solche Eigenschaften allein durch Identitäten zu axiomatisieren, schlägt oft fehl oder erzwingt unnatürliche Kodierungen.

Konsequenz

Äquationale Theorien liefern robuste algebraische Folgen: Sie garantieren die Existenz freier Algebren, erlauben algorithmische Term‑Rewriting‑ und Unifikationsmethoden und erzeugen Kongruenz‑ und Quotientenkonstruktionen, die durch syntaktische Gleichungen gesteuert werden.

Umkehrung

Ersetzt man äquationale Axiome durch beliebige erste‑Ordnungssätze, erhöht sich die Ausdruckskraft (Man kann Existenz und Ordnungs‑Eigenschaften formulieren), aber viele äquationale Vorteile wie unmittelbare freie Konstruktionen und rein syntaktische äquationale Deduktion gehen verloren.

Abgrenzung

Trifft streng auf Axiome zu, die universell quantifizierte Gleichungen zwischen Termen in einer festen Signatur sind; schließt Horn‑Implikationen, die nicht äquivalent zu Mengen von Identitäten sind, Existenzaussagen und wesentlich zweite‑ordentliche Eigenschaften oder nicht‑funktionale Relationen aus, sofern sie nicht als Operationen kodiert werden.

Semantische Spannung

Es besteht Spannung zwischen der entscheidungsfähigen, syntaktischen Natur äquationaler Folgerung und der reicheren Semantik vollständiger erster‑Ordnungstheorien: Manche natürlichen algebraischen Phänomene sind nicht äquational ausdrückbar, was einen Trade‑off zwischen Ausdruckskraft und Einfachheit algebraischer Abschlüsse erzeugt.

Synthese

Eine äquationale Theorie besteht aus Identitäten, die Termoperationen in einer Signatur einheitlich beschränken; ihre Modelle bilden eine äquational abgeschlossene Klasse mit freien Objekten und algorithmischen syntaktischen Methoden zur Herleitung von Identitäten und bilden damit die Basis viel universeller algebraischer Argumentation.