Do "equational theories" include sequents?

Question

In equational logic, which of the following best describes the term "equational theory"?

1. A collection of identities.
2. A collection of quasi-identities, by which I mean sequents of the form $\varphi_0, \cdots, \varphi_{n-1} \vdash \psi,$ where the greek letters represent equations.

For example, suppose I say: let $T$ denote the equational theory of groups. Does $T$ just include the identities of group theory, like $(xy)^{-1} = y^{-1}x^{-1}$ or does it also include the sequents, like $xy = yx \vdash xxyy=yyxx$??

Answer 1

See as a reference Burris and Sankappanavar A Course in Universal Algebra (http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html) on page 92. An equational theory over some variable $X$ is a subset $\Sigma \subseteq \operatorname{Id}(X)$ if there is a class of algebra $K$ such that $\Sigma = \operatorname{Id}_K(X)$, where $\operatorname{Id}(X)$ is the set of all identities generated of a type $\mathcal{F}$ over a set of variables $X$.

Answer 2

The denotation of "equation" and "equational" in such universal algebra nomenclature does not normally include conditional equations such as Horn formulas. See for example the excerpt below for standard nomenclature.

We assume that a first-order language is correlated with each class of algebras of a given similarity type.

A formula in such a language is open if it has no quantifiers. An open formula that is the disjunction of one equation with a (possibly empty) collection of negations of equations is called a conditional equation or quasi-equation or strict universal Horn formula.

The universal closure of an open formula, a conditional equation, and an equation are called, respectively, a universal sentence, a strict universal Horn sentence or quasi-identity, and an identity.

The class of all models (in a given similarity type) of a set of formulas (or, equivalently, a set of sentences), a set of open formulas (or, equivalently, a set of universal sentences), a set of conditional equations, and a set of equations, is called, respectively, an elementary class, a universal class, a strict universal Horn class or quasi-variety, and an equational class or variety.

The set of all open formulas, all conditional equations, and all equations true of a class $\rm K$ of algebras is called the open or universal theory, the conditional equational or strict universal Horn theory, and the equational theory of $\rm K$. The equational theory of $\rm K$ is denoted by ${\scr Eq}(\rm K)$.

Excerpted from p. 3 of Decision Problems for Equational Theories of Relation Algebras, Issue 604 By H. Andréka, Steven R. Givant, I. Németi.