BRICS RS-99-33 Aceto et al.: The Max-Plus Algebra has no Finite Basis BRICS

Basic Research in Computer Science

The Max-Plus Algebra of the Natural Numbers has no Finite Equational Basis

Luca Aceto Zoltán Ésik Anna Ingólfsdóttir

BRICS Report Series RS-99-33 ISSN 0909-0878 October 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Luca Aceto & Zoltán Ésik & Anna Ingólfsdóttir.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/33/

The Max-Plus Algebra of the Natural Numbers has no Finite Equational Basis

Luca Aceto^{∗}  Zoltán Ésik^{†}  Anna Ingólfsdóttir^{∗}^{‡}

Abstract

This paper shows that the collection of identities which hold in the algebra N of the natural numbers with constant zero, and binary operations of sum and maximum is not finitely based. Moreover, it is proven that, for every n, the equations in at most n variables that hold in N do not form an equational basis. As a stepping stone in the proof of these facts, several results of independent interest are obtained. In particular, explicit descriptions of the free algebras in the variety generated by N are offered. Such descriptions are based upon a geometric characterization of the equations that hold in N, which also yields that the equational theory of N is decidable in exponential time.

AMS Subject Classification (1991): 08A70, 03C05, 68Q15, 68Q70. CR Subject Classification (1991): D.3.1, F.1.1, F.4.1. Keywords and Phrases: Equational logic, varieties, complete axiomatizations, exponential time complexity.

1 Introduction

Since Birkhoff’s original developments, equational logic has been one of the classic topics of study within universal algebra. (See, e.g., [17, 24, 25] for surveys of results in this area of research.) In particular, the research literature is, among other things, rich in results, both of a positive and negative nature, on the existence of finite bases for equational theories. (We recall that a finite basis for an equational theory is a finite set of axioms for it.) Classic examples of finitely based algebras include any two-element algebra [14], any finite group [20], and any finite lattice (possibly with operators) [15]. Moreover, as proven by Murskiǐ [19], “almost all” finite algebras have a finite basis for their identities. On the other hand, R. McKenzie [16] has recently settled Tarski’s celebrated Finite Basis Problem by proving that there is no algorithm to decide for a finite algebra whether it is finitely based. Examples of algebras whose set of identities is not finitely based may be found in, e.g., [7, 8, 9, 18, 22].

∗BRICS (Basic Research in Computer Science), Centre of the Danish National Research Foundation, Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark. Email: {luca,annai}@cs.auc.dk. Fax: +45 9815 9889.

†Department of Computer Science, A. József University, Árpád tér 2, 6720 Szeged, Hungary. Partially supported by research grants from the National Foundation of Hungary for Scientific Research (grant no. T30511) and the Fukushima Prefecture. Email:

esik@inf.u-szeged.hu. Fax: +36-62-420292.

‡Supported by a research grant from the Danish Research Council.

This paper contributes to the study of equational theories that are not finitely based by showing that the collection of identities which hold in the algebra N of the natural numbers with constant zero, and binary operations of sum and maximum is not finitely based. Our interest in this problem stems from previous work by two of the authors in the field of concurrency theory, see [2]. In op. cit. a collection of results was given to the effect that no fully invariant congruence that includes ready simulation [5, 13] and is included in language equivalence has a finite equational basis over the language of Basic Process Algebra with Iteration (BPA^{∗}) [3]. This should be contrasted with the positive result obtained by Fokkink and Zantema in [11], who showed that bisimulation congruence [21] is finitely based over the language BPA^{∗}.

In [2], it was left open whether trace congruence has a finite equational basis over the language BPA [4] when the alphabet of actions is a singleton, say {a}. Let us recall that, in that case, the signature of BPA contains a constant a, and binary operations of concatenation and choice. Trace congruence equates the BPA terms that generate the same finite, prefixclosed regular language over the letter a. In [2] it was conjectured that the algebra of BPA terms modulo trace congruence is not finitely based. Since that algebra is isomorphic to that of the natural numbers with constant 1 (the action a), and operations of sum and maximum (corresponding to the BPA operations of concatenation and choice, respectively), such a question is closely related to the existence of a finite equational basis for the collection of identities which hold in the algebra N. The main aim of this paper is to provide a negative answer to this intriguing question.

We begin our study of the equational theory of the algebra N by identifying a useful collection of identities that hold in it (Sect. 2). We prove that the collection of equations in at most one variable that hold in N is finitely based, and we provide evidence that the interplay between the operations of sum and maximum leads to some non-trivial equations involving two or more variables. In particular, for each n ≥ 2 we isolate an equation e_{n} in n variables which holds in N. The equations e_{n} will play an important role in the proof of our main result. We then proceed to prove that no finite collection of equations that hold in N can be used to deduce all of the equations of the form e_{n}. The proof of this technical result follows standard lines, but the details are rather challenging. More precisely, for every integer n ≥ 2, we construct an algebra A_{n} satisfying all the equations in at most n − 1 variables that hold in N, but such that e_{n} does not hold in A_{n}. As a consequence of this result, we obtain that not only the equational theory of N is not finitely based, but, for every n, the equations in at most n variables that hold in N do not form an equational basis.

As a stepping stone in the proof of the aforementioned result, we obtain several results which also hold independent interest. In particular, we provide explicit descriptions of the free algebras in the variety generated by N (Sect. 3). Such descriptions are based upon a geometric characterization of the equations that hold in N, and allow us to prove that the equational theory of N is decidable in exponential time via an exponential time reduction to a linear programming problem.

Notation We shall use standard notions and notations from universal algebra that can be found, e.g., in [6, 12]. For each integer n ≥ 0, we use [n] to stand for the set {1, …, n}, so that [0] is another name for the empty set.

2 The Max-Plus Algebra

Let N = (ℕ, ∨, +, 0) denote the algebra of the natural numbers equipped with the usual sum operation +, constant 0 and the operation ∨ for the maximum of two numbers, i.e.,

x ∨ y = max{x, y} .

We study the equational theory of the algebra N—that is, the collection of equations that hold in N. The reader will have no trouble in checking that the following axioms, that express expected properties of the operations of maximum and sum, hold in N:

\begin{matrix}∨1 & x ∨ y = y ∨ x \\ ∨2 & (x ∨ y) ∨ z = x ∨ (y ∨ z) \\ ∨3 & x ∨ 0 = x \end{matrix} \begin{matrix}+1 & x + y = y + x \\ +2 & (x + y) + z = x + (y + z) \\ +3 & x + 0 = x \\ +∨ & (x ∨ y) + z = (x + z) ∨ (y + z) \end{matrix}

This set of equations will be denoted by Ax_{1}. Note that the equation

(x + y) ∨ x = x + y  (1)

is derivable from Ax_{1}, and, using such an equation, it is a simple matter to derive the idempotency law for ∨, i.e.,

∨4 x ∨ x = x .

We denote by Ax_{0} the set consisting of the equations ∨1, ∨2, ∨4, +1–+3 and +∨. Moreover, we let V_{0} stand for the class of all models of Ax_{0}, and V_{1} for the class of all models of the equations in Ax_{1}. Thus, both V_{0} and V_{1} are varieties and, by the above discussion, V_{1} is a subvariety of V_{0}, i.e., V_{1} ⊆ V_{0}.

Since the reduct (A, ∨) of any algebra A = (A, ∨, +, 0) in V_{0} is a semilattice, we can define a partial order ≤ on the set A by a ≤ b if and only if a ∨ b = b, for all a, b ∈ A. This partial order is called the induced partial order. When A is in the variety V_{1}, the constant 0 is the least element of A with respect to ≤. Moreover, for any A ∈ V_{0}, the ∨ and + operations are monotonic with respect to the induced partial order.

The varieties generated by the reducts (ℕ, ∨, 0) and (ℕ, +, 0) of N afford very simple equational axiomatizations. In fact, it is not hard to prove that:

Proposition 2.1 The axiom system ∨1–∨4 completely axiomatizes the variety generated by the algebra (ℕ, ∨, 0), and the axiom system +1–+3 completely axiomatizes the variety generated by the algebra (ℕ, +, 0).

The axiom system Ax_{1} suffices to prove all the equations in at most one variable in the equational theory of N. In the proof of the following result, and in the remainder of this paper, we shall use nx to denote the n-fold sum of x with itself, and we take advantage of the associativity and commutativity of the operations. By convention, nx stands for 0 when n = 0.

Proposition 2.2 The axiom system Ax_{1} completely axiomatizes the collection of equations in at most one variable which hold in the algebra N.

Proof: Using the equations in Ax_{1}, we can prove every term containing at most one variable equal to one of the form nx. To complete the proof, observe that an equation of the form nx = my holds in N if, and only if, n = m and x = y. □

Remark 2.1 The axiom system consisting of ∨1–∨3, +1–+3 and (1) gives an alternative axiomatization of the collection of equations in at most one variable which hold in the algebra N.

The interplay between the operations of maximum and sum, however, generates some non-trivial collections of equations in two or more variables. For example, the following equations e_{n} also hold in N, for each n ≥ 2:

e_{n} : p_{n} ∨ q_{n} = q_{n} ,

where

p_{n} = x_{1} + … + x_{n}
q_{n} = (2x_{1} + x_{3} + x_{4} + … + x_{n−1} + x_{n})
∨ (x_{1} + 2x_{2} + x_{4} + … + x_{n−1} + x_{n})
⋮
∨ (x_{1} + x_{2} + x_{3} + … + x_{n−2} + 2x_{n−1})
∨ (x_{2} + x_{3} + x_{4} + … + x_{n−1} + 2x_{n}) .

All the equations we have mentioned so far are regular, i.e., they have exactly the same variables on both sides. The reader will have no trouble in arguing that all the equations that hold in the algebra N are regular.

3 Explicit Description of the Free Algebras

In this section we begin our investigation of the equational theory of the algebra N by giving an explicit description of the free algebras in the variety V generated by it. Since N satisfies the equations in Ax_{1}, we have:

Proposition 3.1 V is a subvariety of V_{1}, i.e., V ⊆ V_{1}.

We shall describe the finitely generated free algebras in V, since any infinitely generated free algebra is a directed union of the finitely generated free ones.

Let n ≥ 0 denote a fixed integer. The set ℕ^{n} is the collection of all n-dimensional vectors over ℕ. Let P_{f}(ℕ^{n}) denote the collection of all finite non-empty subsets of ℕ^{n}, and define the operations in the following way: for all U, V ∈ P_{f}(ℕ^{n}),

U ∨ V = U ∪ V
U + V = \{\overline{u} + \overline{v} : \overline{u} ∈ U, \overline{v} ∈ V \}
0 = \{\overline{0}\} ,

where \overline{0} stands for the vector whose components are all 0. For U, V ∈ P_{f}(ℕ^{n}), we refer to the set U + V defined above as the complex sum of U and V. For each i ∈ [n], let \overline{u}_{i} denote the ith unit vector in ℕ^{n}, i.e., the vector whose only non-zero component is a 1 in the ith position.

Proposition 3.2 The algebra P_{f}(ℕ^{n}) is freely generated in V_{0} by the n singleton sets \{\overline{u}_{i}\}, i ∈ [n], containing the unit vectors.

Proof: Let A = (A, ∨, +, 0) denote an algebra in V_{0} and let h be a function mapping \{\overline{u}_{i}\} to an element a_{i} ∈ A, for each i ∈ [n]. Each vector \overline{c} = (c_{1}, …, c_{n}) ∈ ℕ^{n} induces a linear function

f\overline{c} : A^{n} → A
\overline{x} = (x_{1}, …, x_{n}) ↦ \overline{c} · \overline{x} = ∑_{i∈[n]} c_{i}x_{i} .  (2)

The unique extension of h to a homomorphism h^{♯} : P_{f}(ℕ^{n}) → A is given by the assignment

U ↦ ⋁_{\overline{c}∈U} f\overline{c}(a_{1}, …, a_{n}), U ∈ P_{f}(ℕ^{n}) .

□

Note that the induced partial order on P_{f}(ℕ^{n}) is given by set inclusion.

Remark 3.3 Let \overline{c} = (c_{1}, …, c_{n}) ∈ ℕ^{n}. Then, in P_{f}(ℕ^{n}), we can write

\{\overline{c}\} = ∑_{i∈[n]} c_{i}\{\overline{u}_{i}\} .

Also, each U ∈ P_{f}(ℕ^{n}) can be written as

U = ⋁_{\overline{c}∈U}\{\overline{c}\} .

Thus, any term t in the variables x_{1}, …, x_{n} can be rewritten, using the equations in Ax_{0}, to the maximum of linear combinations of the variables x_{1}, …, x_{n}, i.e., there are m ≥ 1 and c_{ij} ∈ ℕ, for i ∈ [m] and j ∈ [n], such that the equation

t = ⋁_{i∈[m]}( ∑_{j∈[n]} c_{ij}x_{j})  (3)

holds in V_{0}. (The empty sum is defined to be 0.) We refer to terms like the right-hand side of (3) as normal forms. Thus we may assume that any equation which holds in a given subvariety of V_{0} is in normal form, i.e. of the form t_{1} = t_{2} where t_{1} and t_{2} are normal forms. Furthermore, an equation

t_{1} ∨ … ∨ t_{m} = t′_{1} ∨ … ∨ t′_{m′}

holds in a subvariety of V_{0} if, and only if, for all i ∈ [m] and j ∈ [m′],

t_{i} ≤ t′_{1} ∨ … ∨ t′_{m′} and t′_{j} ≤ t_{1} ∨ … ∨ t_{m}

hold in the subvariety. We refer to an inequation of the form

t ≤ t_{1} ∨ … ∨ t_{m} ,

where t, t_{1}, …, t_{m} are linear combinations of variables, as simple inequations. By the discussion above, we may assume, without loss of generality, that every set of inequations that hold in V consists of simple inequations only.

A simple inequation t ≤ t_{1} ∨ … ∨ t_{m} that holds in V is irredundant if, for every j ∈ [m],

V |̸= t ≤ t_{1} ∨ … ∨ t_{j−1} ∨ t_{j+1} ∨ … ∨ t_{m} .

Remark 3.4 Let t be a term in the variables x_{1}, …, x_{n}. For later use (cf. the proof of Corollary 3.18), we remark here that a simple inductive argument shows that, in the right-hand side of equation (3), the number m of linear combinations of variables is in 2^{O(n)}, and that the length in symbols of each term ∑_{j∈[n]} c_{ij}x_{j} is in O(|t|), where |t| denotes the length in symbols of t.

In order to give an explicit description of the finitely generated free algebras in V_{1}, we need to take into account the effect of equation ∨3. Let ≤ denote the pointwise partial order on ℕ^{n}. As usual, we say that a non-empty set U ⊆ ℕ^{n} is an order ideal, if \overline{u} ≤ \overline{v} and \overline{v} ∈ U jointly imply that \overline{u} ∈ U, for all vectors \overline{u}, \overline{v} ∈ ℕ^{n}. Each set U ⊆ ℕ^{n} is contained in a least ideal (U], the ideal generated by U. The relation that identifies two sets U, V ∈ P_{f}(ℕ^{n}) if (U] = (V] is a congruence relation on P_{f}(ℕ^{n}), and the quotient with respect to this congruence is easily seen to be isomorphic to the subalgebra I_{f}(ℕ^{n}) of P_{f}(ℕ^{n}) consisting of the finite ideals.

For each i ∈ [n], let (\overline{u}_{i}] denote the principal ideal generated by the unit vector \overline{u}_{i}, i.e., the ideal (\{\overline{u}_{i}\}].

Proposition 3.5 I_{f}(ℕ^{n}) is freely generated in V_{1} by the n principal ideals (\overline{u}_{i}].

Proof: Since I_{f}(ℕ^{n}) is a quotient of P_{f}(ℕ^{n}), it is in V_{0}. Since also ∨3 holds in I_{f}(ℕ^{n}), we have that I_{f}(ℕ^{n}) is in V_{1}. If A = (A, ∨, +, 0) ∈ V_{1} and h maps each (\overline{u}_{i}] to an element a_{i} ∈ A, then consider the unique homomorphism h^{♯} : P_{f}(ℕ^{n}) → A extending the assignment \{\overline{u}_{i}\} ↦ a_{i}, as given in the proof of Proposition 3.2. The restriction of this homomorphism to I_{f}(ℕ^{n}) is the unique homomorphism I_{f}(ℕ^{n}) → A extending h. □

Again, the induced partial order on I_{f}(ℕ^{n}) is the partial order determined by set inclusion.

Remark 3.6 Infinitely generated free algebras in V_{0} and V_{1} have similar concrete descriptions. When α is any cardinal, the free algebra in V_{0} on α generators can be constructed by taking non-empty finite sets of those vectors \overline{u} ∈ ℕ^{α} having a finite number of non-zero components. Again, this algebra contains a subalgebra (the one determined by the finite order ideals) which is free in V_{1}.

We note that, if n ≥ 2, then the equation e_{n} fails in I_{f}(ℕ^{n}), and a fortiori in V_{1}. Since for n ≥ 2 the equation e_{n} holds in N but fails in V_{1}, in order to obtain a concrete description of the free algebras in V we need to make further identifications of the ideals in I_{f}(ℕ^{n}). Technically, we shall start with P_{f}(ℕ^{n}).

Let \overline{v}_{1}, …, \overline{v}_{k} (k ≥ 1) be vectors in ℕ^{n}, and suppose that λ_{i} (i ∈ [k]) are non-negative real numbers with ∑_{i∈[k]} λ_{i} = 1. We call the vector of real numbers ∑_{i∈[k]} λ_{i}\overline{v}_{i} a convex linear combination of the \overline{v}_{i}.

Definition 3.7 We call a non-empty set U ⊆ P_{f}(ℕ^{n}) a convex ideal if for any convex linear combination ∑_{i∈[k]} λ_{i}\overline{v}_{i}, with \overline{v}_{i} ∈ U for all i ∈ [k], and for any \overline{v} ∈ ℕ^{n}, if

\overline{v} ≤ ∑_{i∈[k]} λ_{i}\overline{v}_{i}

in the pointwise order, then \overline{v} ∈ U.

Note that any convex ideal is an ideal. Moreover, the intersection of any number of convex ideals is a convex ideal. Thus, any subset U of ℕ^{n} is contained in a least convex ideal [U], the convex ideal generated by U. When U is finite, so is [U]. For \overline{u} ∈ ℕ^{n}, we shall usually write [\overline{u}] for the convex ideal [\{\overline{u}\}].

Suppose that \overline{c}, \overline{d} ∈ ℕ^{n}. Then, for any \overline{u} ∈ ℕ^{n}, we have \overline{c} · \overline{u} ≤ \overline{d} · \overline{u} iff the two integer vectors \overline{u} and \overline{d} − \overline{c} make a non-obtuse angle. We let \overline{c} ≤ U mean that for each \overline{u} ∈ ℕ^{n} there exists a vector \overline{d} ∈ U such that \overline{c} · \overline{u} ≤ \overline{d} · \overline{u}, or equivalently that the simple inequation

\overline{c} · \overline{x} ≤ ⋁_{\overline{d}∈U} \overline{d} · \overline{x}

holds in N.

Lemma 3.8 Suppose that U ∈ P_{f}(ℕ^{n}) and \overline{c} ∈ ℕ^{n}. Then \overline{c} ∈ [U] iff \overline{c} ≤ U.

Proof: For one part, note that if \overline{c}_{i} ≤ U holds for every i ∈ [k], k ≥ 1, then so does \overline{c} ≤ U for every convex linear combination \overline{c} of \overline{c}_{1}, …, \overline{c}_{k}.

For the other direction, assume that \overline{c} is not in [U]. We proceed to prove that \overline{c} ≤ U does not hold, or equivalently that for some \overline{u} ∈ ℕ^{n}, (\overline{c}−\overline{d})·\overline{u} > 0 for all \overline{d} ∈ U. Below we shall work in the space ℝ^{n} of all n-dimensional real vectors. Denote by H the convex hull of [U], i.e., the least convex set in ℝ^{n} containing [U]. It is clear that \overline{c} is not in H. Let \overline{c}_{0} denote the vector in H closest to \overline{c}. (This exists, since H is a closed set.) Let P denote the hyperplane passing through \overline{c}_{0} and perpendicular to \overline{c} − \overline{c}_{0}. Let P′ denote the hyperplane parallel to P which contains \overline{c}. Now, P divides the space ℝ^{n} into two parts S_{1} and S_{2} with S_{1} containing the origin and \overline{c}_{0}. We claim that the entire set H is a subset of S_{1}. Indeed, if \overline{e} ∈ H and \overline{e} ∉ S_{1}, then take the line passing through \overline{e} and \overline{c}_{0}. Since H is convex, H contains the segment of this line whose endpoints are \overline{c}_{0} and \overline{e}. But this segment contains a point closer to \overline{c} than \overline{c}_{0}, a contradiction. Since the whole set H lies in S_{1}, each point of H is an inner point of the half-space determined by P′ that contains the origin. This means that if \overline{d} is in H, the angle between \overline{x}_{0} = \overline{c} − \overline{c}_{0} and \overline{d} − \overline{c} is obtuse, i.e., (\overline{c} − \overline{d}) · \overline{x}_{0} > 0. Since H is an order ideal included in ℝ_{+}^{n}, it follows that \overline{c}_{0} ≤ \overline{c} with respect to the pointwise ordering; otherwise \overline{c}_{0} is not the point in H with the shortest distance to \overline{c} as assumed.

Next we note that, for all \overline{d} ∈ U, the function \overline{x} ↦ (\overline{c}−\overline{d})·\overline{x} is continuous. Therefore, for each such \overline{d}, there is a real number ε\overline{d} > 0 such that (\overline{c}−\overline{d})·\overline{x} > 0 whenever |\overline{x}_{0} − \overline{x}| < ε\overline{d} (where we use |\overline{x}_{0} − \overline{x}| to denote the length of the vector \overline{x}_{0} − \overline{x}). Now take ε to be smallest amongst the ε\overline{d}’s. (This exists because the set U is finite.) Then, for all \overline{d} ∈ U, it holds that (\overline{c} − \overline{d}) · \overline{x} > 0 whenever |\overline{x}_{0} − \overline{x}| < ε. In particular there must be a vector \overline{x} with positive rational coefficients with this property. From this we derive easily that there must be a \overline{u} ∈ ℕ^{n} with (\overline{c} − \overline{d}) · \overline{u} > 0 for all \overline{d} ∈ U, which was to be shown.

□

When U, V ∈ P_{f}(ℕ^{n}), we define U ∼ V iff [U] = [V]. By the previous lemma, it follows that ∼ is a congruence relation on P_{f}(ℕ^{n}). Moreover, the quotient P_{f}(ℕ^{n})/∼ is in V. Indeed, if [U] ≠ [V], then, by Lemma 3.8, there is some \overline{c} ∈ U with \overline{c} ≰ V, say. Thus, for some \overline{x} = (x_{1}, …, x_{n}) ∈ ℕ^{n}, f\overline{c}(\overline{x}) ≰ ∨_{\overline{d}∈V} f\overline{d}(\overline{x}), so that h(U) ≰ h(V) for the unique homomorphism P_{f}(ℕ^{n}) → N determined by the assignment \{\overline{u}_{i}\} ↦ x_{i}, i ∈ [n]. (Recall that the singleton sets containing the unit vectors are the free generators of P_{f}(ℕ^{n}).) Furthermore Lemma 3.8 implies that for such an h, it holds that h(U) = h(V) if [U] = [V]. Thus, any two not ∼-equivalent sets in P_{f}(ℕ^{n}) can be separated by a homomorphism P_{f}(ℕ^{n}) → N. It follows that P_{f}(ℕ^{n})/∼ embeds in a direct power of N, showing P_{f}(ℕ^{n})/∼∈ V.

It is immediate to see that the quotient algebra P_{f}(ℕ^{n})/ ∼ is isomorphic to the following algebra CI_{f}(ℕ^{n}) = (CI_{f}(ℕ^{n}), ∨, +, 0) of all finite convex ideals in P_{f}(ℕ^{n}). For any two I, J ∈ CI_{f}(ℕ^{n}),

I + J = [\{\overline{u} + \overline{v} : \overline{u} ∈ I, \overline{v} ∈ J\}]
I ∨ J = [I ∪ J]
0 = \{\overline{0}\} .

Indeed, an isomorphism P_{f}(ℕ^{n})/ ∼ → CI_{f}(ℕ^{n}) is given by the mapping U/∼ ↦ [U].

Recall that, for each i ∈ [n], \overline{u}_{i} denotes the ith unit vector in ℕ^{n}. For each i ∈ [n], the set [\overline{u}_{i}] = (\overline{u}_{i}] = \{\overline{u}_{i}, \overline{0}\} is the least convex ideal containing \overline{u}_{i}.

Theorem 3.9 CI_{f}(ℕ^{n}) is freely generated by the n convex ideals [\overline{u}_{i}] in the variety V.

Proof: We have already noted that CI_{f}(ℕ^{n}) is in V. Thus, since V is the variety generated by N, and since CI_{f}(ℕ^{n}) is generated by the [\overline{u}_{i}], to complete the proof we need to show that any mapping h : \{[\overline{u}_{1}], …, [\overline{u}_{n}]\} → N extends to a homomorphism CI_{f}(ℕ^{n}) → N. But by Proposition 3.2 there is a homomorphism h′ : P_{f}(ℕ^{n}) → N with h′(\{\overline{u}_{i}\}) = h([\overline{u}_{i}]), for all i ∈ [n]. By Lemma 3.8, the congruence relation ∼ is included in the kernel of h′, so that h′ factors through the quotient map P_{f}(ℕ^{n}) → P_{f}(ℕ^{n})/ ∼. Since P_{f}(ℕ^{n})/∼ and CI_{f}(ℕ^{n}) are isomorphic, the result follows. □

Remark 3.10 The same proof shows that each CI_{f}(ℕ^{n}) is free in the variety generated by the structure (ℝ_{+}, ∨, +, 0), defined on the non-negative real numbers. Thus, V is also generated by the structure ℝ_{+} (which is not elementarily equivalent to N).

Note that the induced partial order on CI_{f}(ℕ^{n}) is again the subset order.

Remark 3.11 It is well-known that, for each non-negative integer n, the free algebra on n generators in the variety generated by an algebra A may be constructed as an algebra of all n-ary term functions of A. When A is the structure N, each term function is the pointwise maximum of a finite non-empty set of linear functions, induced as in (2) by the vectors in a finite non-empty set in P_{f}(ℕ^{n}), or convex ideal in CI_{f}(ℕ^{n}).

Remark 3.12 When n = 1, the algebras I_{f}(ℕ) and CI_{f}(ℕ) are both isomorphic to N, yielding another proof of Proposition 2.2.

Remark 3.13 Another representation of the n-generated free algebra in V consists of all bounded convex ideals of ℝ_{+}^{n}. The advantage of this representation is that, in this free model, the sum operation is complex addition.

Remark 3.14 When α is a cardinal, the free algebra in V on α generators may be described by using finite convex ideals of vectors in ℕ^{α} having a finite number of non-zero components.

Corollary 3.15 For every n ≥ 1 and equation e, we have

CI_{f}(ℕ^{n}) ⊧ e ⇔ V ⊧ e .

Proof: If V ⊧ e then CI_{f}(ℕ^{n}) ⊧ e, since CI_{f}(ℕ^{n}) is in V. Also, the convex ideals in CI_{f}(ℕ^{n}) containing vectors whose components are all 0 except possibly for the first one, determine a subalgebra of CI_{f}(ℕ^{n}) isomorphic to N. Thus, if CI_{f}(ℕ^{n}) ⊧ e then N ⊧ e, so that V ⊧ e. □

As a corollary of Theorem 3.9, we obtain the following characterization of the simple inequations which hold in the variety V.

Corollary 3.16 Let \overline{c}, \overline{d}_{j} (j ∈ [m], m ≥ 1) be vectors in ℕ^{n}. Then \overline{c} ≤ \{\overline{d}_{1}, …, \overline{d}_{m}\} iff there are λ_{1}, …, λ_{m} ≥ 0 such that λ_{1} + … + λ_{m} = 1 and \overline{c} ≤ λ_{1}\overline{d}_{1} + … + λ_{m}\overline{d}_{m} with respect to the pointwise ordering. Moreover, if \overline{c} ≤ \{\overline{d}_{1}, …, \overline{d}_{m}\} is irredundant, then λ_{1}, …, λ_{m} > 0.

Proof: Use the fact that t ≤ t_{1} ∨ … ∨ t_{m} holds in V iff

t([\overline{u}_{1}], …, [\overline{u}_{n}]) ≤ ⋁_{i∈[m]} t_{i}([\overline{u}_{1}], …, [\overline{u}_{n}])

holds in CI_{f}(ℕ^{n}). □

The above result offers a geometric characterization of the simple inequations in the equational theory of N, viz. an inequation \overline{c} · \overline{x} ≤ \overline{d}_{1} · \overline{x} ∨ … ∨ \overline{d}_{m} · \overline{x} (where \overline{x} = (x_{1}, …, x_{n}) is a vector of variables) holds in N iff the vector \overline{c} lies in the ideal generated by the convex hull of the vectors \overline{d}_{1}, …, \overline{d}_{m}.

Corollary 3.17 It is decidable in polynomial time whether a simple inequation holds in V.

Proof: Let c_{1}x_{1} + … + c_{n}x_{n} ≤ ⋁_{i∈[m]}(∑_{j∈[n]} d_{ij}x_{j}) be a simple inequation. In light of Corollary 3.16, it holds in N iff there is a non-negative solution (over the real numbers) to the following system of linear equations in the unknowns λ_{i}, γ_{j} (i ∈ [m], j ∈ [n]):

( ∑_{i∈[m]} d_{ij}λ_{i}) − γ_{j} = c_{j} (j ∈ [n])
∑_{i∈[m]} λ_{i} = 1 .

Thus our original problem can be restated as asking if there is a feasible solution to the linear programming problem with the above equality constraints and non-negativity conditions. It is well-known that linear programming problems are solvable in polynomial time [23]. □

Corollary 3.18 The equational theory of V is decidable in exponential time.

Proof: Immediate from Remark 3.4 and Corollary 3.17. □

It is interesting to compare the above result on the complexity of the equational theory of N with the classic results by Fischer and Rabin [10] on the complexity of the first-order theory of the real numbers under addition, and of Presburger arithmetic—the first-order theory of addition on the natural numbers. There is a fixed constant c > 0 such that for every (nondeterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2^{cn} steps. In the case of Presburger arithmetic, the corresponding lower bound is 2^{2^{cn}}. These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized. Such complexity results apply mutatis mutandis to the first-order theory of the algebra N.

4 The Variety V is not Finitely Based

We now proceed to apply the results that we have developed so far to the study of the axiomatizability of the equational theory of the algebra N.

The main aim of this paper is to prove the following result to the effect that the variety V has no finite equational basis.

Theorem 4.1 The variety V has no finite (equational) axiomatization, i.e., there is no finite set E of equations, which hold in V, and such that for all terms t_{1}, t_{2},

V ⊧ t_{1} = t_{2} iff E ⊧ t_{1} = t_{2} .

To prove Theorem 4.1 we shall define a sequence of algebras A_{n} (n ≥ 2) in V_{1} such that following holds:

For any finite set E of equations which hold in V, there is an n ≥ 2 such that

A_{n} ⊧ E but A_{n} |̸= e_{n} .

The equations e_{n}, n ≥ 2, were defined in Sect. 2.

In fact, as we shall see in due course, the algebra construction that we now proceed to present also yields the following stronger result.

Theorem 4.2 There exists no natural number n such that the collection of all equations in at most n variables that hold in V forms an equational basis for V.

Using Theorem 4.2, it is a simple matter to prove Theorem 4.1.

Proof of Theorem 4.1: Given a finite set E of equations that hold in V, let n denote an integer larger than the number of variables in any equation belonging to E. Since the equations in at most n variables that hold in V do not form an equational basis for V, the equations in E do not give an equational axiomatization of V either. □

Remark 4.3 Another view of the non-existence of a finite basis for the variety V is offered in [1]. Ibidem we show that the collection of equations in two variables that hold in V has no finite equational axiomatization.

5 The Models

Before defining our models, we need some preparation. The weight of a vector \overline{u} ∈ ℕ^{n}, n ≥ 1, is defined as the sum of its components, and the weight of a finite non-empty set U ⊆ ℕ^{n} is the maximum of the weights of its members.

Lemma 5.1 Let \overline{v} = λ_{1}\overline{v}_{1}+…+λ_{k}\overline{v}_{k}, k ≥ 1, be a convex linear combination of the vectors \overline{v}_{i} ∈ ℕ^{n} and let \overline{u} ≤ \overline{v}, where \overline{u} ∈ ℕ^{n}. Then the weight of \overline{u} is at most the maximum of the weights of the \overline{v}_{i}. Moreover, if every λ_{i} (i ∈ [k]) is positive, then the weight of \overline{u} equals the maximum of the weights of the \overline{v}_{i} iff all the vectors \overline{v}_{i} (i ∈ [k]) have equal weight.

The proof is straightforward and is therefore omitted.

For each n ≥ 2, let us say that a vector \overline{u} ∈ ℕ^{n} is n-ok if no component of \overline{u} is greater than 2, and at most one of the components of \overline{u} is equal to 2. Moreover, if a component is 2, then it is followed by a 0. Of course, it is understood that the last component is followed by the first. Moreover, we say that a non-empty set U ⊆ ℕ^{n} is n-ok if so are all of its members. Note that each n-ok set in ℕ^{n} is finite and that there are only a finite number of n-ok sets. We introduce the following notation for some n-ok vectors related to the equation e_{n}:

\overline{δ} = (1, …, 1)
\overline{γ}_{1} = (2, 0, 1, 1, …, 1, 1)
\overline{γ}_{2} = (1, 2, 0, 1, …, 1, 1)
⋮
\overline{γ}_{n−1} = (1, 1, 1, 1, …, 2, 0)
\overline{γ}_{n} = (0, 1, 1, 1, …, 1, 2) ,

so that in \overline{γ}_{i}, the 2 is on the ith position and is followed by a 0. All other components are 1’s. Thus, \overline{δ} and the \overline{γ}_{i} are the only n-ok vectors of weight n, and the weight of any other n-ok vector is strictly less than n. In fact, if \overline{u} is n-ok, then either there exists an i ∈ [n] such that \overline{u} ≤ \overline{γ}_{i} in the pointwise order, or \overline{u} = \overline{δ}. Note that

\overline{δ} = \frac{1}{n}\overline{γ}_{1} + … + \frac{1}{n}\overline{γ}_{n} .  (4)

Thus, \overline{δ} belongs to the convex ideal generated by the vectors \overline{γ}_{i} (i ∈ [n]).

Lemma 5.2 The system consisting of any n of the vectors \overline{δ}, \overline{γ}_{1}, …, \overline{γ}_{n} is linearly independent.

Proof: By (4), and because of the symmetry of the vectors \overline{γ}_{i} and \overline{δ}, it is sufficient to show that the determinant of the matrix M whose ith row is \overline{γ}_{i}, for i ∈ [n − 1], and whose nth row is \overline{δ}, is non-zero. To this end, let us subtract the last row of M from the first n − 1 rows. It is easy to show by induction on n that the determinant of the resulting matrix is n. □

Lemma 5.3 Suppose that U is a non-empty set of n-ok vectors. Then:

1. The convex ideal [U] consists of n-ok vectors.

2. If \overline{δ} ∈ [U] then either \overline{δ} ∈ U or \overline{γ}_{i} ∈ U for all i ∈ [n].

3. If \overline{γ}_{i} ∈ [U], for some i ∈ [n], then \overline{γ}_{i} ∈ U.

Proof: As for the first claim, it suffices to show that, for any convex linear combination λ_{1}\overline{γ}_{1} + … + λ_{n}\overline{γ}_{n} and for all \overline{u} ∈ ℕ^{n}, if \overline{u} ≤ λ_{1}\overline{γ}_{1} + … + λ_{n}\overline{γ}_{n}, then \overline{u} is n-ok. But by Lemma 5.1 it is clear that the weight of \overline{u} is at most n, since each of the \overline{γ}_{i} is of weight n. Also, any component of \overline{u} lies between the minimum and the maximum of the corresponding components of the \overline{γ}_{i}, so that no component of \overline{u} is greater than 2. If for some i, the ith component of \overline{u} is 2, then necessarily λ_{i} = 1 and λ_{j} = 0, for all j ≠ i, completing the proof.

Suppose now that \overline{δ} ∈ [U]. Since the weight of \overline{δ} is n and the weight of any vector in U is at most n, it follows by Lemma 5.1 that \overline{δ} is the convex linear combination of vectors of weight n in U. Recall that the only n-ok vectors of weight n are \overline{δ} and the \overline{γ}_{i}. To complete the proof, we need to show that it is not possible to construct \overline{δ} as a (convex) linear combination of a proper subcollection of the \overline{γ}_{i}. But this is immediate, since by Lemma 5.2 the system consisting of \overline{δ} and any n − 1 of the \overline{γ}_{i} is linearly independent.

The proof of the last claim is similar. One uses the fact that none of the vectors \overline{γ}_{i} is a convex linear combination of the vectors \overline{δ} and \overline{γ}_{j} with i ≠ j.

□

We define:

Γ = [\{\overline{γ}_{1}, …, \overline{γ}_{n}\}]
Δ = Γ − \{\overline{δ}\} ,

so that Γ is the convex ideal consisting of all of the n-ok vectors. By (4), the set Δ is not a convex ideal.

Corollary 5.4 The set \{\overline{γ}_{1}, …, \overline{γ}_{n}\} is the unique minimal generating set of the convex ideal Γ.

Corollary 5.5 If J is a convex ideal properly included in Γ, then J − \{\overline{δ}\} is also a convex ideal.

Proof: If J − \{\overline{δ}\} is not a convex ideal, then \overline{δ} is in [J − \{\overline{δ}\}]. But by Lemma 5.3, this is possible only if J contains all of the \overline{γ}_{i}, contradicting the assumption that J is properly included in Γ. □

Corollary 5.6 The set consisting of Δ and all n-ok convex ideals is closed under intersection.

Proof: Suppose that I and J are n-ok convex ideals. Then I ∩ J is also an n-ok convex ideal. If I is properly included in Γ, then I ∩ Δ = I − \{\overline{δ}\} is an n-ok convex ideal by Corollary 5.5. □

Lemma 5.7 Suppose that n ≥ 3. Then there exist no non-trivial convex ideals I and J with I + J = Γ.

Proof: Assume, towards a contradiction, that n ≥ 3, I and J are convex ideals with I + J = Γ but I, J ≠ \{\overline{0}\}. Let k denote the weight of I and ℓ the weight of J. Then k, ℓ > 0 and k +ℓ = n. Let I′ denote the set of all vectors of weight k in I, and define J′ ⊆ J in the same way. By Corollary 5.4, the complex sum K of I′ and J′ contains all vectors \overline{γ}_{i}, i ∈ [n].

Suppose that I′, say, contains a vector \overline{u} which has a component equal to 2. Then there exists an i ∈ [n] such that \overline{u} + \overline{v} = \overline{γ}_{i} for all \overline{v} ∈ J′. Hence J′ contains a unique vector and \overline{γ}_{i} is the only element of \{\overline{γ}_{1}, …, \overline{γ}_{n}\} contained in K, contradicting Corollary 5.4. Thus, I′ contains no vector having a component equal to 2, and similarly for J′.

Since the complex sum of I′ and J′ contains the vectors \overline{γ}_{1} and \overline{γ}_{2}, there are vectors \overline{w}_{1}, \overline{w}_{2} ∈ I′ and \overline{v}_{1}, \overline{v}_{2} ∈ J′ such that

\overline{w}_{1} + \overline{v}_{1} = \overline{γ}_{1} and \overline{w}_{2} + \overline{v}_{2} = \overline{γ}_{2} .

This means that, for some b_{3}, …, b_{n} ∈ {0, 1},

\overline{w}_{1} = (1, 0, b_{3}, …, b_{n}) and
\overline{v}_{1} = (1, 0, b̃_{3}, …, b̃_{n}) ,

where b̃ denotes the complement of b, for every b ∈ {0, 1}. Similarly, since n ≥ 3, there are c_{1}, c_{4}, …, c_{n} ∈ {0, 1} such that

\overline{w}_{2} = (c_{1}, 1, 0, c_{4}, …, c_{n}) and
\overline{v}_{2} = (c̃_{1}, 1, 0, c̃_{4}, …, c̃_{n}) .

It is now easy to see that if \overline{w}_{1} + \overline{v}_{2} is in Γ, then \overline{w}_{2} + \overline{v}_{1} is not. Indeed, if \overline{w}_{1} + \overline{v}_{2} is in Γ, then c̃_{1} = 0, so that c_{1} = 1. Thus the first two components of \overline{w}_{2} + \overline{v}_{1} are 2 and 1, respectively. This contradicts our assumption that I + J is equal to Γ. □

We now define our models.

Definition 5.8 For each n ≥ 2, let A_{n} consist of the convex ideals of ndimensional vectors included in Γ, the set Δ, and a top element ⊤. The constant 0 is the set \{\overline{0}\}, containing the n-dimensional zero vector. Let I, J ∈ A_{n}. If I or J is ⊤, then we define I ∨ J = I + J = ⊤. If both I and J are different from ⊤, then I ∨ J is the smallest set in A_{n} containing I ∪ J. This set exists by Corollary 5.6. To define I + J, let K be the complex sum \{\overline{u} + \overline{v} : u ∈ I, \overline{v} ∈ J\}. If K is not n-ok, we define I + J = ⊤. If K is n-ok, then we let I + J be the smallest set in A_{n} containing K. We have defined the algebra A_{n} = (A_{n}, ∨, +, 0).

Remark 5.9 For later use, let us note that if n ≥ 3, then neither Δ nor Γ has a non-trivial representation as the sum of two non-zero elements of A_{n}. Indeed, if I + J ∈ {Δ, Γ} in A_{n} and I, J ≠ 0, then both I and J are different from Δ, and I + J = Γ in CI_{f}(ℕ^{n}). This contradicts Lemma 5.7.

When n = 2, the set Δ does not have a non-trivial representation as the sum of two non-zero elements of A_{n}, but we have

[{(1, 0), (0, 1)}] + [{(1, 0), (0, 1)}] = Γ

both in A_{n} and in CI_{f}(ℕ^{n}).

Lemma 5.10 Suppose that I, J ∈ A_{n}, and I, J ≠ ⊤. Then:

1. If \overline{δ} ∉ I ∪ J and \{\overline{γ}_{1}, …, \overline{γ}_{n}\} ⊆ I ∪ J then I ∨ J = Δ. Otherwise I ∨ J = [I ∪ J].

2. Let K denote the complex sum of I and J and suppose that K is nok. If one of I and J is Δ (so that the other is 0), then I + J = Δ. Otherwise I + J = [K].

Proof: Suppose that \overline{δ} ∉ I ∪ J and \{\overline{γ}_{1}, …, \overline{γ}_{n}\} ⊆ I ∪ J. Then Δ and Γ are the only two sets in A_{n} containing I ∪ J. Since Δ ⊂ Γ, we have I ∨ J = Δ. Conversely, if I ∨ J = Δ in A_{n}, then \overline{δ} ∉ I ∪ J and [I ∪ J] = Γ. Thus, by Corollary 5.4, each \overline{γ}_{i} is in I ∪ J. For the second claim, note that if I + J = Δ in A_{n} with I, J ≠ 0, then it would have to be the case that n ≥ 3 and I + J = Γ in CI_{f}(ℕ^{n}), so that the result follows from Lemma 5.7. □

Corollary 5.11 The equivalence relation ∼ that collapses Δ and Γ, and is the identity relation otherwise, is a congruence relation over A_{n}. Moreover, the quotient algebra of A_{n} with respect to this congruence is isomorphic to that quotient of CI_{f}(ℕ^{n}) which identifies any two not n-ok convex ideals.

As a consequence of the above result, since A_{n}/∼ ∈ V, if for some terms t = t(x_{1}, …, x_{n}) and t′ = t′(x_{1}, …, x_{n}) in the variables x_{1}, …, x_{n} and for some I_{1}, …, I_{n} ∈ A_{n} we have N ⊧ t = t′ but t(I_{1}, …, I_{n}) = I ≠ I′ = t′(I_{1}, …, I_{n}) in A_{n}, then I, I′ ∈ {Δ, Γ}.

Lemma 5.12 Suppose that t = t(x_{1}, …, x_{n}) is a term containing exactly the variables x_{1}, …, x_{n}, and suppose furthermore that I_{i} ∈ A_{n}, i ∈ [n]. For each i, define J_{i} = I_{i}, if I_{i} is a convex ideal, and J_{i} = Γ, if I_{i} = Δ. Moreover, let J_{i} be any not n-ok convex ideal if I_{i} = ⊤. Denote I = t(I_{1}, …, I_{n}) in A_{n} and J = t(J_{1}, …, J_{n}) in CI_{f}(ℕ^{n}). Then:

1. I = ⊤ iff J is not n-ok. Moreover, if I_{i} = ⊤, for some i ∈ I, then I = ⊤.

2. I ∈ {Δ, Γ} iff J = Γ. Moreover, I ⊆ J.

3. If I ∉ {⊤, Δ, Γ}, then I = J.

Proof: All the statements follow by a straightforward induction argument using Lemma 5.10. □

Proposition 5.13 For each n ≥ 2, A_{n} ∈ V_{1}.

Proof: The facts that both ∨ and + are commutative and that 0 is a neutral element for both operations are obvious. The associativity of ∨ is immediate from its definition and Corollary 5.6. To establish the associativity of the sum operation, by Corollary 5.11, or by Lemma 5.12, we only need to show that for all I, J, K ∈ A_{n} such that I, J, K ≠ ⊤, it holds that I +(J +K) = Δ iff (I + J) + K = Δ. But this is immediate by Lemma 5.10. Finally, we check that for all I, J, K ∈ A_{n},

(I ∨ J) + K = Δ ⇔ (I + K) ∨ (J + K) = Δ .  (5)

If (I ∨ J) + K = Δ, then, by Lemma 5.10, either I ∨ J = Δ and K = 0, or I = J = 0 and K = Δ. In either case, (I + K) ∨ (J + K) = Δ. Assume now that the right-hand side of (5) is Δ. If one of I, J, K is Δ then the other two are 0 and the claim follows. If none of I, J, K is Δ, then, by Lemma 5.12, all of them are convex ideals and (I + K) ∨ (J + K) = Γ in CI_{f}(ℕ^{n}). But then, since CI_{f}(ℕ^{n}) is in V_{1}, (I ∨ J) + K = Γ holds in CI_{f}(ℕ^{n}). Thus, by Lemma 5.7 and the fact that (I + K) ∨ (J + K) = Δ in A_{n}, one of the following two cases applies:

- K = 0, or

- n = 2 and I ∨ J = K = [{(1, 0), (0, 1)}].

In the former case, (I ∨ J) + K = Δ in A_{n}. In the latter, (I + K) ∨ (J + K) would be Γ in A_{n}. □

Lemma 5.14 Let I_{1}, …, I_{k} ∈ A_{n} − {Δ}, k ≥ 1. The following statements hold in A_{n}.

1. I_{1} ∨ … ∨ I_{k} is the smallest set in A_{n} which contains I_{1} ∪ … ∪ I_{k}.

2. If the complex sum

K = \{\overline{u}_{1} + … + \overline{u}_{k} : \overline{u}_{i} ∈ I_{i}\}

is n-ok, then I = I_{1} + … + I_{k} is the smallest set in A_{n} which contains K.

Proof: The first claim is immediate from the definition of the ∨ operation and Corollary 5.6. For the second claim, we distinguish between two cases. If I ≠ Δ, Γ, then by Lemma 5.12, I is the same as the sum of the I_{i} in CI_{f}(ℕ^{n}), i.e., the smallest convex ideal containing K. It is clear that I is also the smallest set in A_{n} which contains K. If I = Δ, or if I = Γ and n ≥ 3, then by Remark 5.9, except for one, all the I_{i} are zero, so that the result is immediate. If n = 2 and I = Γ, then two cases arise. The case that all the I_{i} are 0, except for one, is handled as before. The second case is that, for some j ∈ [k],

I_{1} + … + I_{j} = I_{j+1} + … + I_{k} = [{(1, 0), (0, 1)}] .

But in that case K is also Γ. □

Note that ⊤ is the top element of A_{n} in the induced partial order, and for all elements I, J ∈ A_{n} other than ⊤, I is below J in the induced partial order if and only if I ⊆ J.

Proposition 5.15 For each n ≥ 2, A_{n} satisfies any equation in at most n − 1 variables which holds in N.

Proof: It suffices to show that A_{n} ⊧ t ≤ t′ for any irredundant simple inequation t ≤ t′ such that N ⊧ t ≤ t′ and both t and t′ contain the same m < n variables, so that t = t(x_{1}, …, x_{m}) and t′ = t′(x_{1}, …, x_{m}), say. By Propositions 2.2 and 5.13, we only need consider the case m > 1. (Note that, in this case, n ≥ 3.) Moreover, by Corollary 5.11, or by Lemma 5.12, we only need to show that for all I_{1}, …, I_{m} in A_{n}, it is not possible that \overline{δ} ∈ I and Δ = J, where I = t(I_{1}, …, I_{m}) and J = t′(I_{1}, …, I_{m}).

Assume, towards a contradiction, that for some I_{i}, i ∈ [m], we have \overline{δ} ∈ I and Δ = J, and that t ≤ t′ is a simple inequation in fewest variables for which this holds. Note that this implies that I_{i} ≠ 0 for every i ∈ [m]. Let us write

t′ = t_{1} ∨ … ∨ t_{k} ,

where the t_{j} are distinct simple terms, and define

J_{j} = t_{j}(I_{1}, …, I_{m}) ,

for all j ∈ [k]. It is not possible that one of the I_{i} is Δ, for that would imply t = x_{1} and m = 1. Thus, all of the I_{i} are convex ideals. Also, since Γ has no non-trivial representation as the sum of two non-zero elements of A_{n} (see Remark 5.9), we have I ≠ Γ. (Thus, since \overline{δ} ∈ I, I is a convex ideal and I = t(I_{1}, …, I_{m}) also holds in CI_{f}(ℕ^{n}).)

Let us write

t = c_{1}x_{1} + … + c_{m}x_{m}
t_{j} = c_{j1}x_{1} + … + c_{jm}x_{m} ,

for all j ∈ [k]. Here, we allow that some of the c_{jl} are 0. On the other hand no c_{i} is 0, and for each l there is a j such that c_{jl} is non-zero. Also, at most one of the c_{i} is equal to two, for otherwise by Lemma 5.12 we would have I = ⊤. Similarly, for each j, at most one of the c_{jl} is 2. Thus, without loss of generality, it is sufficient to consider the following two cases.

Case 1: t = x_{1} + … + x_{m}. Since \overline{δ} ∈ I, by Lemmas 5.3 and 5.14 there exist vectors \overline{w}_{i} ∈ I_{i}, i ∈ [m], with \overline{δ} = \overline{w}_{1} + … + \overline{w}_{m}. Since the operations are monotonic, we may also assume that I_{i} = [\overline{w}_{i}], for all i ∈ [m]. Indeed,

\overline{δ} ∈ t([\overline{w}_{1}], …, [\overline{w}_{m}])

and

\overline{δ} ∉ t′([\overline{w}_{1}], …, [\overline{w}_{m}]) ,

since t′([\overline{w}_{1}], …, [\overline{w}_{m}]) ⊆ t′(I_{1}, …, I_{m}) = Δ. But if t′([\overline{w}_{1}], …, [\overline{w}_{m}]) is not Δ, then it is a convex ideal, and by Lemma 5.12 we may infer that

t([\overline{w}_{1}], …, [\overline{w}_{m}]) ⊆ t′([\overline{w}_{1}], …, [\overline{w}_{m}]) ,

contradicting the fact that \overline{δ} ∈ t([\overline{w}_{1}], …, [\overline{w}_{m}]) and \overline{δ} ∉ t′([\overline{w}_{1}], …, [\overline{w}_{m}]). Thus, t′([\overline{w}_{1}], …, [\overline{w}_{m}]) = Δ.

Consider the vector \overline{w}_{1} and suppose that its first component is 1, say. Then, since \overline{w}_{1} +…+\overline{w}_{m} = \overline{δ}, the first components of the vectors \overline{w}_{i}, i ≠ 1, are all 0. Since \overline{γ}_{1} is in Δ, it follows from Lemma 5.3 that there exists some j with c_{j1} = 2. But then no other component of \overline{w}_{1} is 1, or else J would be ⊤. In a similar way, it follows that each \overline{w}_{i} has exactly one component equal to 1, a contradiction, since m < n.

Case 2: t = 2x_{1} + x_{2} + … + x_{m}. In this case, we may assume that there exist \overline{w}_{1}, …, \overline{w}_{m} and \overline{v}_{1} with \overline{v}_{1} + \overline{w}_{1} + … + \overline{w}_{m} = \overline{δ}, I_{1} = [\overline{w}_{1}, \overline{v}_{1}] and I_{j} = [\overline{w}_{j}], j ≥ 2. Again, we can conclude that \overline{v}_{1} and each \overline{w}_{j} have exactly one non-zero component, which is a 1. Using this, a contradiction is reached as follows. Since the simple irredundant inequation t ≤ t′ holds in N, by our assumptions some t_{j} is of the form

2x_{1} + 2x_{i} + t′′ ,

for some term t′′ and i ∈ [m] with i ≠ 1. However, in that case J would be ⊤. □

6 Proof of the Main Result

We are now ready to prove Theorem 4.2 stated in Section 4.

Proof of Theorem 4.2: Given an integer n ≥ 2, consider the algebra A_{n} and the simple inequation p_{n} ≤ q_{n}, where the terms p_{n} and q_{n} were defined in Sect. 2. For each i ∈ [n], let \overline{u}_{i} denote the ith n-dimensional unit vector whose components are all 0 except for a 1 in the ith position. By Lemma 5.14, we have

p_{n}([\overline{u}_{1}], …, [\overline{u}_{n}]) = [\overline{δ}]
q_{n}([\overline{u}_{1}], …, [\overline{u}_{n}]) = Δ

in A_{n}. Thus A_{n} |̸= p_{n} ≤ q_{n}, i.e., A_{n} |̸= e_{n}. On the other hand e_{n} holds in V, and moreover, by Proposition 5.15, A_{n} satisfies all identities in at most n − 1 variables that hold in V. Hence, the collection of identities in at most n − 1 variables that hold in V does not prove e_{n}. □

Acknowledgements: The results of this paper were in part obtained while the second author was visiting at the University of Aizu. He would like to thank the University of Aizu for providing excellent working conditions, and Satoshi Okawa for his kind hospitality. The third author’s work on this paper partly took place while she was visiting the Institute of Software of the Chinese Academy of Sciences, and she would like to thank that institution and Huimin Lin for their hospitality. Finally, the first and third authors thank Wan Fokkink for the joint work [2] which prompted them to study the problem considered in this paper. Comments from two anonymous referees led to improvements in the presentation of our results.

References

[1] L. Aceto, Z. Ésik and A. Ingólfsdóttir, On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers, BRICS Report RS–99–22, August 1999. Available at the URL

    http://www.brics.dk/RS/99/22/index.html.

[2] L. Aceto, W. J. Fokkink, and A. Ingólfsdóttir, A menagerie of non-finitely based process semantics over BPA*—from ready simulation to completed traces, Mathematical Structures in Computer Science, 8 (1998), pp. 193–230.

[3] J. Bergstra, I. Bethke, and A. Ponse, Process algebra with iteration and nesting, Computer Journal, 37 (1994), pp. 243–258.

[4] J. Bergstra and J. W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

[5] B. Bloom, S. Istrail, and A. R. Meyer, Bisimulation can’t be traced, J. Assoc. Comput. Mach., 42 (1995), pp. 232–268.

[6] S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Springer-Verlag, New York, 1981.

[7] J. H. Conway, Regular Algebra and Finite Machines, Mathematics Series (R. Brown and J. De Wet eds.), Chapman and Hall, London, United Kingdom, 1971.

[8] S. Crvenković, I. Dolinka, and Z. Ésik, The variety of Kleene algebras with conversion is not finitely based, 1999. To appear in Theoretical Computer Science.

[9] Z. Ésik and M. Bertol, Nonfinite axiomatizability of the equational theory of shuffle, Acta Inform., 35 (1998), pp. 505–539.

[10] M. J. Fischer and M. O. Rabin, Super-exponential complexity of Presburger arithmetic, in Complexity of Computation (Proc. SIAM-AMS Symposium, New York, 1973), vol. VII of SIAM-AMS Proceedings, Providence, R.I., 1974, American Mathematical Society, pp. 27– 41.

[11] W. J. Fokkink and H. Zantema, Basic process algebra with iteration: Completeness of its equational axioms, Computer Journal, 37 (1994), pp. 259–267.

[12] G. Grätzer, Universal Algebra, Springer-Verlag, second ed., 1979.

[13] K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Information and Computation, 94 (1991), pp. 1–28.

[14] R. Lyndon, Identities in two-valued calculi, Trans. Amer. Math. Soc., 71 (1951), pp. 457–465.

[15] R. McKenzie, Equational bases for lattice theories, Math. Scand., 27 (1970), pp. 24–38.

[16] R. McKenzie, Tarski’s finite basis problem is undecidable, International J. Algebra Computation, 6 (1996), pp. 49–104.

[17] G. McNulty, A field guide to equational logic, J. Symbolic Computation, 14 (1992), pp. 371–397.

[18] V. L. Murskiǐ, The existence in three-valued logic of a closed class with finite basis, not having a finite complete system of identities, Doklady Akademii Nauk SSSR, 163 (1965), pp. 815–818. English translation in: Soviet Mathematics Doklady, 6:1020-1024, 1965.

[19] V. L. Murskiǐ, The existence of a finite basis and some other properties of “almost all” finite algebras, Problemy Kibernet, 30 (1975), pp. 43–56.

[20] S. Oates and M. B. Powell, Identical relations in finite groups, J. Algebra, 1 (1965), pp. 11–39.

[21] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

[22] R. E. Park, Equational Classes of Non-Associative Ordered Algebras, PhD thesis, University of California at Los Angeles, 1976.

[23] A. Schrijver, Theory of Linear and Integer Programming, John Wiley and Sons, 1986.

[24] W. Taylor, Equational logic, in Contributions to Universal Algebra, North-Holland Publishing Co., Amsterdam, 1977, pp. 465–501. Proceedings of the Colloquium held in Szeged, 1975. Colloquia Mathematica Societatis János Bolyai, vol. 17.

[25] , Equational logic, in [12], Appendix 4, pp. 378–400.

Recent BRICS Report Series Publications

RS-99-33 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. The Max-Plus Algebra of the Natural Numbers has no Finite Equational Basis. October 1999. 25 pp.

RS-99-32 Luca Aceto and François Laroussinie. Is your Model Checker on Time? — On the Complexity of Model Checking for Timed Modal Logics. October 1999. 11 pp. Appears in Kuty�owski, Pacholski and Wierzbicki, editors, Mathematical Foundations of Computer Science: 24th International Symposium, MFCS ’99 Proceedings, LNCS 1672, 1999, pages 125–136.

RS-99-31 Ulrich Kohlenbach. Foundational and Mathematical Uses of Higher Types. September 1999. 34 pp.

RS-99-30 Luca Aceto, Willem Jan Fokkink, and Chris Verhoef. Structural Operational Semantics. September 1999. 128 pp. To appear in Bergstra, Ponse and Smolka, editors, Handbook of Process Algebra, 1999.

RS-99-29 Søren Riis. A Complexity Gap for Tree-Resolution. September 1999. 33 pp.

RS-99-28 Thomas Troels Hildebrandt. A Fully Abstract Presheaf Semantics of SCCS with Finite Delay. September 1999. 37 pp. To appear in Category Theory and Computer Science: 8th International Conference, CTCS ’99 Proceedings, ENTCS, 1999.

RS-99-27 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. September 1999. 57 pp. To appear in the November 2000 issue of Theoretical Computer Science. This revised report supersedes the earlier BRICS report RS-98-54.

RS-99-26 Jesper G. Henriksen. An Expressive Extension of TLC. September 1999. 20 pp. To appear in Thiagarajan and Yap, editors, Fifth Asian Computing Science Conference, ASIAN ’99 Proceedings, LNCS, 1999.

RS-99-25 Gerth Stølting Brodal and Christian N. S. Pedersen. Finding Maximal Quasiperiodicities in Strings. September 1999. 20 pp.

RS-99-24 Luca Aceto, Willem Jan Fokkink, and Chris Verhoef. Conservative Extension in Structural Operational Semantics. September 1999. 23 pp. To appear in the Bulletin of the EATCS.