Complexity of the Universal Theory of Residuated Ordered Groupoids

Abstract

We study the computational complexity of the universal theory of residuated ordered groupoids, which are algebraic structures corresponding to Nonassociative Lambek Calculus. We prove that the universal theory is co$\textsf {NP}$-complete which, as we observe, is the lowest possible complexity for a universal theory of a non-trivial class of structures. The universal theories of the classes of unital and integral residuated ordered groupoids are also shown to be co$\textsf {NP}$-complete. We also prove the co$\textsf {NP}$-completeness of the universal theory of classes of residuated algebras, algebraic structures corresponding to Generalized Lambek Calculus.

1 Introduction

Residuated ordered groupoids¹ (Fuchs, 1963; Blyth & Janowitz, 1972), for short $\textit{rog}$s, are algebraic models of the Nonassociative Lambek Calculus NL (Lambek, 1961), a version of the Lambek Calculus (Lambek, 1958) obtained by dropping the implicit rule of associativity. The atomic theory of $\textit{rog}$s, that is, the set of sentences of the form $\forall x_1 \ldots \forall x_n (s \leqslant t)$ valid on every $\textit{rog}$, is, in essence, a notational variant of NL, with atomic sentences corresponding to sequents $s \vdash t$. Similarly, the Horn theory of $\textit{rog}$s, which is the set of Horn sentences $\forall x_1 \ldots \forall x_n (u_1 \leqslant v_1 \& \dots \& \, u_m \leqslant v_m \Rightarrow s \leqslant t)$ valid on every $\textit{rog}$, is a notational variant of NL with nonlogical axioms (Buszkowski, 2005). In this modification of NL, proofs are allowed that commence not only with identity sequents, but also with nonlogical assumptions $u \vdash v$, where u and v are arbitrary formulas. These assumptions correspond to the algebraic inequalities $u \leqslant v$ that are premisses of the corresponding Horn sentence. It is worth noting that, in contrast with NL, the cut-rule is, in general, not eliminable in NL with nonlogical axioms.

The universal theory of $\textit{rog}$s is the set of sentences of the form $\forall x_1 \ldots \forall x_n \varphi$, where $\varphi$ is a Boolean combination of algebraic inequalities, valid on every $\textit{rog}$. The universal theory is a natural extension of the Horn theory; a proof-theoretic analog thereof would be a deductive system allowing deductions of a disjunctively interpreted set of sequents from a conjunctively interpreted set of sequents. Such deductive formalisms, in the guise of multi-conclusion systems (Sambin et al., 2000; Jeřábek, 2009; Iemhoff, 2015, 2016; Bezhanishvili et al., 2016; Jalali, 2021) and hypersequents (Avron, 1996; Lellmann, 2016), have recently received considerable attention, even though no such system capturing the universal theory of $\textit{rog}$s has, as far as we know, yet been constructed.

Both the atomic and Horn theory of $\textit{rog}$s are decidable in polynomial time, as shown by Aarts and Trautwein (1995) and Buszkowski (2005), respectively. The universal theory of $\textit{rog}$s is shown to be decidable by Farulewski (2008), however, the complexity has, to date, not been established. In the present paper we fill this gap by showing that the universal theory of $\textit{rog}$s is co$\textsf {NP}$-complete which, as we observe, is the lowest possible complexity for a universal theory of a non-trivial class of structures.

In addition to $\textit{rog}$s we consider two variations of $\textit{rog}$s that have attracted attention, namely unital and integral $\textit{rog}$s. By a unital residuated ordered groupoid, or $\textit{urog}$, we mean a $\textit{rog}$ that has an identity for the groupoid operation. The class of $\textit{urog}$s is an algebraic semantics for NL with unit. It is shown by Bulińska (2009) that the Horn and, hence, atomic theory of $\textit{urog}$s is decidable in polynomial time. By an integral residuated ordered groupoid, or $\textit{irog}$, we mean a $\textit{urog}$ in which the identity is the greatest element with respect to the order. The class of $\textit{irog}$s is considered by Blok and Van Alten (2005), where it is shown to have the ‘finite embeddability property’, or fep, meaning that every finite partial substructure of an $\textit{irog}$ is embeddable into a finite $\textit{irog}$. The fep, together with finite axiomatizability, implies decidability of the universal theory of $\textit{irog}$s. In the present paper, we show that the universal theory of both $\textit{urog}$s and $\textit{irog}$s is co$\textsf {NP}$-complete. We note that decidability of the universal theory of $\textit{rog}$s was established by Farulewski (2008) by proving the fep for the class of $\textit{rog}$s. It is shown there that NL has the strong finite model property, from which the fep for the class of rogs then follows by Blok and Van Alten (2002).

We shall also consider classes of residuated algebras. These algebras were introduced by Buszkowski (1989) as algebraic semantics for the Generalized Lambek Calculus [see also (Buszkowski, 1998; Kołowska-Gawiejnowicz, 1997; Kandulski, 1997; Jäger, 2004)]. It is shown by Buszkowski (2005) that the Horn and, hence, atomic theory of each class of residuated algebras is decidable in polynomial time. The fep, and hence decidability of the universal theory, for each class of residuated algebras is proved by Buszkowski (2011). In this paper, we extend the methods used for residuated ordered groupoids to show that the universal theory of each class of residuated algebras is co$\textsf {NP}$-complete.

The upper complexity bounds obtained herein are established using a technique of partial structures described by Van Alten (2013). For rogs, for example, the technique requires an intrinsic characterization of partial substructures of $\textit{rog}$s, or ‘partial $\textit{rog}$s’. A universal sentence fails to hold in some $\textit{rog}$ if, and only if, it fails to hold in some partial $\textit{rog}$ of size not greater than the size of the given universal sentence. The characterization of partial $\textit{rog}$s presented in Theorem 1 can be checked in polynomial time for a given partial structure; hence, if an arbitrary partial structure is guessed, it can be decided in polynomial time if it is a partial $\textit{rog}$. In this way we obtain a non-deterministic polynomial-time algorithm for deciding if a partial structure is a partial $\textit{rog}$, from which it follows that the universal theory of $\textit{rog}$s is in co$\textsf {NP}$—the full details are given in Sect. 4. For the lower complexity bounds we use the observation, stated in Theorem 4, that the universal theory of any non-trivial class of structures is co$\textsf {NP}$-hard.

2 Residuated Ordered Groupoids

We consider structures corresponding to the signature $\sigma$ containing binary operation symbols $\circ$, $\backslash$ and /, as well as a binary relation symbol $\leqslant$; we call such structures $\sigma$-structures. We assume throughout the paper that terms are built out of a fixed countable set $\textit{Var}$ of variables, whose members are typically denoted by $x, y, z, x_1, y_1, \ldots \,$.

A residuated ordered groupoid, or $\textit{rog}$, is a $\sigma$-structure $\textbf{A}= \langle A, \circ , \backslash , /, \leqslant \rangle$, where $\langle A, \leqslant \rangle$ is a partially ordered set and $\circ$, $\backslash$ and / are binary operations on A such that, for all $a, b, c \in A$,

$$\begin{aligned} a \circ b \leqslant c\, \Longleftrightarrow \, b \leqslant a \backslash c\, \Longleftrightarrow \, a \leqslant c / b. \end{aligned}$$

(1)

The class of all $\textit{rog}$s is denoted by $\mathcal {ROG}$. It follows from (1) that $\circ$ is order-preserving in both coordinates, $\backslash$ is order-reversing in the first coordinate and order-preserving in the second, while / is order-preserving in the first coordinate and order-reversing in the second.

If $\textbf{A}= \langle A, \circ ^\textbf{A}, \backslash ^\textbf{A}, /^\textbf{A}, \leqslant ^\textbf{A}\rangle$ and $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, \leqslant ^\textbf{B}\rangle$ are $\textit{rog}$s, then by an embedding of $\textbf{B}$ into $\textbf{A}$ we mean a map $\alpha : B \rightarrow A$ such that $a \leqslant ^\textbf{B}b$ if, and only if, $\alpha (a) \leqslant ^\textbf{A}\alpha (b)$, and $\alpha (a \star ^\textbf{B}b) = \alpha (a) \star ^\textbf{A}\alpha (b)$ for every $\star \in \{ \circ , \backslash , / \}$ and all $a, b \in B$. Observe that every embedding is injective since, for all $a, b \in B$, if $a \ne b$ then either $a \not \leqslant ^\textbf{B}b$ or $b \not \leqslant ^\textbf{B}a$, so $\alpha (a) \not \leqslant ^\textbf{A}\alpha (b)$ or $\alpha (b) \not \leqslant ^\textbf{A}\alpha (a)$; in particular, $\alpha (a) \ne \alpha (b)$.

We shall use the following terminology and notation. Let $\langle Q, \leqslant \rangle$ be a partially ordered set. A subset X of Q is called an upset of $\langle Q, \leqslant \rangle$ if $a \in X$ and $a \leqslant b$ imply $b \in X$, for all $a, b \in Q$. If the order relation on Q is clear from the context, we shall use U(Q) to denote the set of all upsets of $\langle Q, \leqslant \rangle$ and, for $a \in Q$, by the principal upset of a, we shall mean the set $[a) := \{ b \in Q \mid a \leqslant b \}$.

We shall rely on the frame representation theory for $\textit{rog}$s due to Dunn (1993). A $\textit{rog}$-frame is a structure $\mathfrak {F} = \langle P, \leqslant , R \rangle$, where $\langle P, \leqslant \rangle$ is a partially ordered set and R is a ternary relation on P that is monotone in the last coordinate and antitone in the first two coordinates, i.e., such that, for all $f, f', g, g', h, h' \in P$,

$$ \begin{aligned} R(f,g,h) ~ \& ~ f' \leqslant f ~ \& ~ g' \leqslant g ~ \& ~ h \leqslant h' \Longrightarrow R(f',g',h'). \end{aligned}$$

(2)

Starting from a $\textit{rog}$-frame $\mathfrak {F} = \langle P, \leqslant , R \rangle$, we obtain a $\textit{rog}$ that has as its universe the set U(P), as follows. Define, for all $X, Y \in U(P)$,

$$ \begin{aligned} X \circ Y&:= \{ h \in P \mid (\exists f, g \in P)\, [f \in X ~ \& ~ g \in Y~ \& ~R(f,g,h)] \}; \end{aligned}$$

(3)

$$ \begin{aligned} X \backslash Y&: = \{ g \in P \mid (\forall f,h \in P)\, [f \in X ~ \& ~ R(f,g,h) \Longrightarrow h \in Y] \}; \end{aligned}$$

(4)

$$ \begin{aligned} Y / X&:= \{ f \in P \mid (\forall g,h \in P)\, [g \in X ~ \& ~ R(f,g,h) \Longrightarrow h \in Y] \}. \end{aligned}$$

(5)

Since $\mathfrak {F}$ satisfies (2), so defined $\circ$, $\backslash$ and / are operations on U(P). The definitions (3–5) ensure that (1) is satisfied with respect to the partial order $\subseteq$ on U(P). Thus, $\textbf{A}_\mathfrak {F} = \langle U(P), \circ , \backslash , /, \subseteq \rangle$ is a $\textit{rog}$, which we call the $\textit{rog}$ associated with $\mathfrak {F}$.

Conversely, starting from a $\textit{rog}$ $\textbf{A}= \langle A, \circ , \backslash , /, \leqslant \rangle$, we can obtain a $\textit{rog}$-frame, as follows. Define a ternary relation R on U(A) by

$$ \begin{aligned} R(f,g,h) \;\Longleftrightarrow \; (\forall a, b \in A)\, [a \in f ~ \& ~ b \in g \Longrightarrow a \circ b \in h]. \end{aligned}$$

(6)

Then R and $\subseteq$ satisfy condition (2), hence $\mathfrak {F}_\textbf{A}= \langle U(A), \subseteq , R \rangle$ is a $\textit{rog}$-frame. Thus, we may obtain $\textbf{A}_{\mathfrak {F}_\textbf{A}}$, the $\textit{rog}$ associated with $\mathfrak {F}_\textbf{A}$. It is straightforward to check that the map $\mu :A \rightarrow U(U(A))$ defined by $\mu (a) = \{ f \in U(A) \mid a \in f \}$ is an embedding of $\textbf{A}$ into $\textbf{A}_{\mathfrak {F}_\textbf{A}}$.

3 Partial $\sigma$-Structures and Partial $\textit{rog}$s

In this section, we introduce partial $\textit{rog}$s and obtain an intrinsic characterization thereof; this characterization will play a key role in establishing our complexity results.

A partial $\sigma$ -structure is a structure $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, \leqslant ^{\textbf{B}} \rangle$, where $\leqslant ^{\textbf{B}}$ is a binary relation on B and $\circ ^{\textbf{B}}$, $\backslash ^{\textbf{B}}$ and $/^{\textbf{B}}$ are partial binary operations on B, i.e., partial functions from $B \times B$ into B. The domains of $\circ ^{\textbf{B}}$, $\backslash ^{\textbf{B}}$ and $/^{\textbf{B}}$ are denoted by, respectively, ${{\,\textrm{dom}\,}}(\circ ^{\textbf{B}})$, ${{\,\textrm{dom}\,}}(\backslash ^{\textbf{B}})$ and ${{\,\textrm{dom}\,}}(/^{\textbf{B}})$. For clarity, we note that for each $\star \in \{\circ , \backslash , /\}$, ${{\,\textrm{dom}\,}}(\star ^\textbf{B}) \subseteq B \times B$.

A partial $\textit{rog}$ is a partial $\sigma$-structure $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, \leqslant ^{\textbf{B}} \rangle$ which is a partial substructure of a $\textit{rog}$, that is, for which there exists a $\textit{rog}$ $\textbf{A}= \langle A, \circ ^\textbf{A}, \backslash ^\textbf{A}, /^\textbf{A}, \leqslant ^\textbf{A}\rangle$ such that $B \subseteq A$, $\leqslant ^\textbf{B}= {\leqslant ^\textbf{A}} \!\!\restriction _B$ and $a \star ^{\textbf{B}} b = a \star ^\textbf{A}b$ for each $\star \in \{\circ , \backslash , /\}$ and $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\star ^{\textbf{B}})$.

We note that if $\textbf{B}$ is a partial $\textit{rog}$ that is a partial substructure of a $\textit{rog}$ $\textbf{A}$, then $\star ^\textbf{B}$ is not necessarily the restriction of $\star ^\textbf{A}$ to B; that is, there may exist $a, b \in B$ and $\star \in \{\circ , \backslash , /\}$ for which $a \star ^\textbf{A}b \in B$ but $\langle a, b \rangle \notin {{\,\textrm{dom}\,}}(\star ^\textbf{B})$. This definition is consistent with that of partial substructure used by Van Alten (2013), but contrasts with the closely related notion of partial subalgebra used, for example, by Blok and Van Alten (2002).

By an embedding of a partial $\sigma$-structure $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, \leqslant ^\textbf{B}\rangle$ into a $\sigma$-structure $\textbf{A}= \langle A, \circ ^\textbf{A}, \backslash ^\textbf{A}, /^\textbf{A}, \leqslant ^\textbf{A}\rangle$ we mean a map $\alpha : B \rightarrow A$ such that $a \leqslant ^\textbf{B}b$ if, and only if, $\alpha (a) \leqslant ^\textbf{A}\alpha (b)$, and $\alpha (a \star ^\textbf{B}b) = \alpha (a) \star ^\textbf{A}\alpha (b)$ for each $\star \in \{ \circ , \backslash , / \}$ and $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\star ^\textbf{B})$.

Observe that if $\textbf{B}$ is a partial $\sigma$-structure and there exists an embedding of $\textbf{B}$ into a $\textit{rog}$ $\textbf{A}$, then $\textbf{B}$ is isomorphic to a partial substructure of $\textbf{A}$, that is, $\textbf{B}$ is (isomorphic to) a partial $\textit{rog}$. Using this observation, in the following theorem we give an intrinsic characterization of partial $\textit{rog}$s. The construction used in the proof of the theorem resembles the construction of the $\textit{rog}$ associated with $\mathfrak {F}_\textbf{A}$, i.e., $\textbf{A}_{\mathfrak {F}_\textbf{A}}$, from a $\textit{rog}$ $\textbf{A}$.

Theorem 1

A partial $\sigma$-structure $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, \leqslant ^\textbf{B}\rangle$ is a partial $\textit{rog}$ if, and only if, it satisfies the following conditions:

• (i) $\langle B, \leqslant ^\textbf{B}\rangle$ is a partially ordered set;

• (ii) $(\forall \langle a, b \rangle , \langle c, d \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))\, [a \leqslant ^\textbf{B}c ~ \& ~ b \leqslant ^\textbf{B}d \Longrightarrow a \circ ^\textbf{B}b \leqslant ^\textbf{B}c \circ ^\textbf{B}d]$;

• (iii) $(\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))(\forall \langle c, d \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))\,$ $[a \leqslant ^\textbf{B}c ~ \& ~ b \leqslant ^\textbf{B}c \backslash ^\textbf{B}d \Longrightarrow a \circ ^\textbf{B}b \leqslant ^\textbf{B}d]$;

• (iv) $(\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))(\forall \langle c, d \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))\,$ $[a \leqslant ^\textbf{B}c /^\textbf{B}d \& b \leqslant ^\textbf{B}d \Longrightarrow a \circ ^\textbf{B}b \leqslant ^\textbf{B}c]$;

• (v) $(\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))(\forall \langle c, d \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))\,$ $[a \leqslant ^\textbf{B}c \& c \circ ^\textbf{B}d \leqslant ^\textbf{B}b \Longrightarrow d \leqslant ^\textbf{B}a \backslash ^\textbf{B}b]$;

• (vi) $(\forall \langle a, b \rangle , \langle c, d \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))\, [a \leqslant ^\textbf{B}c ~ \& ~ d \leqslant ^\textbf{B}b \Longrightarrow c \backslash ^\textbf{B}d \leqslant ^\textbf{B}a \backslash ^\textbf{B}b]$;

• (vii) $(\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))(\forall \langle c, d \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))\,$ $[a \leqslant ^\textbf{B}c /^\textbf{B}d ~ \& ~ c \leqslant ^\textbf{B}b \Longrightarrow d \leqslant ^\textbf{B}a \backslash ^\textbf{B}b]$;

• (viii) $(\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))(\forall \langle c, d \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))\,$ $[b \leqslant ^\textbf{B}d ~ \& ~ c \circ ^\textbf{B}d \leqslant ^\textbf{B}a \Longrightarrow c \leqslant ^\textbf{B}a /^\textbf{B}b]$;

• (ix) $(\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))(\forall \langle c, d \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))\,$ $[d \leqslant ^\textbf{B}a ~ \& ~ b \leqslant ^\textbf{B}c \backslash ^\textbf{B}d \Longrightarrow c \leqslant ^\textbf{B}a /^\textbf{B}b]$;

• (x) $(\forall \langle a, b \rangle , \langle c, d \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))\, [c \leqslant ^\textbf{B}a ~ \& ~ b \leqslant ^\textbf{B}d \Longrightarrow c /^\textbf{B}d \leqslant ^\textbf{B}a /^\textbf{B}b]$.

Proof

It is straightforward to check that conditions (i–x) hold in every $\textit{rog}$. Since these conditions are universal sentences with quantifiers relativized by the domains of the partial operations, it follows that (i–x) hold in every partial $\textit{rog}$.

Conversely, suppose $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, \leqslant ^{\textbf{B}} \rangle$ is a partial $\sigma$-structure satisfying (i–x). We construct a $\textit{rog}$ into which $\textbf{B}$ is embeddable. Define a ternary relation $R^\textbf{B}$ on the set U(B) of all upsets of $\langle B, \leqslant ^\textbf{B}\rangle$ by:

$$ \begin{aligned} R^\textbf{B}(f,g,h)&\iff (\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))\, [a \in f ~ \& ~ b \in g \Longrightarrow a \circ ^\textbf{B}b \in h]\, \\&\quad ~ \& ~ (\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))\, [a \in f ~ \& ~ a \backslash ^\textbf{B}b \in g \Longrightarrow b \in h]\,\\&\quad ~ \& ~ (\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))\, [a /^\textbf{B}b \in f ~ \& ~ b \in g \Longrightarrow a \in h]. \end{aligned}$$

It is straightforward to check that the structure $\mathfrak {F} = \langle U(B), \subseteq , R^\textbf{B}\rangle$ is a $\textit{rog}$-frame. Let $\textbf{A}_\mathfrak {F} = \langle U(U(B)), \circ , \backslash , /, \subseteq \rangle$ be the $\textit{rog}$ associated with $\mathfrak {F}$ and let $\mu :B \rightarrow U(U(B))$ be the map defined by $\mu (a) = \{ f \in U(B) \mid a \in f \}$. We show that $\mu$ is an embedding of $\textbf{B}$ into $\textbf{A}_\mathfrak {F}$.

If $a, b \in B$ with $a \leqslant ^\textbf{B}b$, then every element of $\mu (a)$ contains b; hence, $\mu (a) \subseteq \mu (b)$. If $a \not \leqslant ^\textbf{B}b$, then the principal upset [a) belongs to $\mu (a)$ but not to $\mu (b)$; hence $\mu (a) \not \subseteq \mu (b)$. Thus, $a \leqslant ^\textbf{B}b$ if, and only if, $\mu (a) \subseteq \mu (b)$.

Let $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$. We show that $\mu (a \circ ^\textbf{B}b) = \mu (a) \circ \mu (b)$, where

$$\begin{aligned} \mu (a \circ ^\textbf{B}b) = \{ h \in U(B) \mid a \circ ^\textbf{B}b \in h \} \end{aligned}$$

and

$$ \begin{aligned} \mu (a) \circ \mu (b) = \{ h \in U(B) \mid (\exists f,g \in U(B))\, [a \in f ~ \& ~ b \in g ~ \& ~ R^\textbf{B}(f,g,h)] \}. \end{aligned}$$

Assume $h \in \mu (a) \circ \mu (b)$. Then there exist $f,g \in U(B)$ such that $a \in f$, $b \in g$ and $R^\textbf{B}(f,g,h)$. It follows from the definition of $R^\textbf{B}$ that $a \circ ^\textbf{B}b \in h$, hence $h \in \mu (a \circ ^\textbf{B}b)$. Thus, $\mu (a) \circ \mu (b) \subseteq \mu (a \circ ^\textbf{B}b)$.

Next, assume $h \in \mu (a \circ ^\textbf{B}b)$, i.e., $a \circ ^\textbf{B}b \in h$. Let $f := [a)$ and $g := [b)$. Clearly, $f, g \in U(B)$, $a \in f$ and $b \in g$. We show that $R^\textbf{B}(f,g,h)$. Suppose that c and d are arbitrary elements of B for which $\langle c, d \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$, $c \in f$ and $d \in g$. Then, $a \leqslant ^\textbf{B}c$ and $b \leqslant ^\textbf{B}d$, hence, by (ii), $a \circ ^\textbf{B}b \leqslant ^\textbf{B}c \circ ^\textbf{B}d$. Since $a \circ ^\textbf{B}b \in h$ and h is an upset, $c \circ ^\textbf{B}d \in h$. Suppose that c and d are arbitrary elements of B for which $\langle c, d \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B})$, $c \in f$ and $c \backslash ^\textbf{B}d \in g$. Then, $a \leqslant ^\textbf{B}c$ and $b \leqslant ^\textbf{B}c \backslash ^\textbf{B}d$, hence, by (iii), $a \circ ^\textbf{B}b \leqslant ^\textbf{B}d$, whence $d \in h$. Lastly, suppose that c and d are arbitrary elements of B for which $\langle c, d \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B})$, $c /^\textbf{B}d \in f$ and $d \in g$. Then, $a \leqslant ^\textbf{B}c /^\textbf{B}d$ and $b \leqslant ^\textbf{B}d$, hence, by (iv), $a \circ ^\textbf{B}b \leqslant ^\textbf{B}c$, whence $c \in h$. Thus, $R^\textbf{B}(f,g,h)$. Since $a \in f$ and $b \in g$, we obtain $h \in \mu (a) \circ \mu (b)$, hence $\mu (a \circ ^\textbf{B}b) \subseteq \mu (a) \circ \mu (b)$.

Let $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B})$. We show that $\mu (a \backslash ^\textbf{B}b) = \mu (a) \backslash \mu (b)$, where

$$\begin{aligned} \mu (a \backslash ^\textbf{B}b) = \{ g \in U(B) \mid a \backslash ^\textbf{B}b \in g \} \end{aligned}$$

and

$$ \begin{aligned} \mu (a) \backslash \mu (b) = \{ g \in U(B) \mid (\forall f, h \in U(B))\, [a \in f ~ \& ~ R^\textbf{B}(f,g,h) \Longrightarrow b \in h] \}. \end{aligned}$$

Assume $g \in \mu (a \backslash ^\textbf{B}b)$, i.e., $a \backslash ^\textbf{B}b \in g$. Suppose that, for some $f,h \in U(B)$, both $a \in f$ and $R^\textbf{B}(f,g,h)$. Since $a \backslash ^\textbf{B}b \in g$, by definition of $R^\textbf{B}$, we obtain $b \in h$ and so $g \in \mu (a) \backslash \mu (b)$. Thus, $\mu (a \backslash ^\textbf{B}b) \subseteq \mu (a) \backslash \mu (b)$.

Next, assume $g \notin \mu (a \backslash ^\textbf{B}b)$, i.e., $a \backslash ^\textbf{B}b \notin g$. To prove that $g \notin \mu (a) \backslash \mu (b)$, we show that there exist $f, h \in U(B)$ such that $a \in f$ and $R^\textbf{B}(f,g,h)$, but $b \notin h$. Let $f := [a)$ and $h := \{ e \in B\, \mid \, e \not \leqslant ^\textbf{B}b \}$. Clearly, $f, h \in U(B)$, $a \in f$ and $b \notin h$. We show that $R^\textbf{B}(f,g,h)$. Suppose that c and d are arbitrary elements of B for which $\langle c, d \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$, $c \in f$ and $d \in g$. Then, $a \leqslant ^\textbf{B}c$. Since g is an upset and $a \backslash ^\textbf{B}b \notin g$, surely $d \not \leqslant ^\textbf{B}a \backslash ^\textbf{B}b$, hence, by (v), $c \circ ^\textbf{B}d \not \leqslant ^\textbf{B}b$, and so $c \circ ^\textbf{B}d \in h$. Suppose that c and d are arbitrary elements of B for which $\langle c, d \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B})$, $c \in f$ and $c \backslash ^\textbf{B}d \in g$. Then $a \leqslant ^\textbf{B}c$ and $c \backslash ^\textbf{B}d \not \leqslant ^\textbf{B}a \backslash ^\textbf{B}b$, hence, by (vi), $d \not \leqslant ^\textbf{B}b$, and so $d \in h$. Lastly, suppose that c and d are arbitrary elements of B for which $\langle c, d \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B})$, $c /^\textbf{B}d \in f$ and $d \in g$. Then, $a \leqslant ^\textbf{B}c /^\textbf{B}d$ and $d \not \leqslant ^\textbf{B}a /^\textbf{B}b$, hence, by (vii), $c \not \leqslant ^\textbf{B}b$, and so $c \in h$. Thus, $R^\textbf{B}(f,g,h)$. Since $a \in f$ and $b \notin h$, we obtain $g \notin \mu (a) \backslash \mu (b)$ hence $\mu (a) \backslash \mu (b) \subseteq \mu (a \backslash ^\textbf{B}b)$.

For $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B})$, the proof that $\mu (a /^\textbf{B}b) = \mu (a) / \mu (b)$, which relies on conditions (viii–x), is analogous.

Thus, $\mu$ is an embedding of $\textbf{B}$ into $\textbf{A}_\mathfrak {F}$. It follows that $\textbf{B}$ is a partial $\textit{rog}$, which completes the proof. $\square$

4 Complexity of the Universal Theory of $\mathcal {ROG}$

In this section, we consider the universal theory of $\mathcal {ROG}$ and prove its co$\textsf {NP}$-completeness.

We recall that universal $\sigma$-sentences are formulas of the form $\forall x_1 \ldots \forall x_n \varphi$, where $\varphi$ is a quantifier-free (first-order) $\sigma$-formula, i.e., a formula defined by the BNF expression

$$ \begin{aligned} \varphi := (t \leqslant t) \mid \textsf {not}\, \varphi \mid (\varphi ~ \& ~ \varphi ) \mid (\varphi ~\textsf {or}~ \varphi ), \end{aligned}$$

with t ranging over $\sigma$-terms, and containing no variables other than $x_1, \ldots , x_n$.

We omit parentheses around formulas where this does not lead to ambiguity. Henceforth, given a quantifier-free $\sigma$-formula $\varphi$, we write $\varphi (x_1, \dots , x_n)$ to indicate that $\varphi$ contains no variables except $x_1, \dots , x_n$. We denote by $\textit{Var}(\varphi )$ and $\textit{Ter}(\varphi )$ the sets of, respectively, variables and terms occurring in $\varphi$.

An assignment on a $\textit{rog}$ $\textbf{A}$ is a map $v : \textit{Var} \rightarrow A$. The definition of the satisfaction relation $\textbf{A}\models ^v \varphi$ between $\textit{rog}$s $\textbf{A}$, assignments v and quantifier-free $\sigma$-formulas $\varphi$ is standard—see, e.g., Chang and Keisler (1990). A quantifier-free $\sigma$-formula $\varphi$ is satisfiable in $\mathcal {ROG}$ if $\textbf{A}\models ^v \varphi$ for some $\textit{rog}$ $\textbf{A}$ and some assignment v on $\textbf{A}$; $\varphi$ is valid on $\mathcal {ROG}$ if $\textbf{A}\models ^v \varphi$ for every $\textit{rog}$ $\textbf{A}$ and every assignment v on $\textbf{A}$. A universal $\sigma$-sentence $\forall x_1 \ldots \forall x_n \varphi$ is valid on $\mathcal {ROG}$ if $\varphi$ is valid on $\mathcal {ROG}$. The universal theory of $\mathcal {ROG}$ is the set of all universal $\sigma$-sentences valid on $\mathcal {ROG}$. Clearly, a universal sentence $\forall x_1 \ldots \forall x_n \varphi$ is valid on $\mathcal {ROG}$ if, and only if, $\textsf {not}\, \varphi$ is not satisfiable in $\mathcal {ROG}$. Thus, satisfiability of quantifier-free $\sigma$-formulas in $\mathcal {ROG}$ and validity of universal $\sigma$-sentences on $\mathcal {ROG}$ (i.e., membership in the universal theory of $\mathcal {ROG}$) are complementary computational problems.

We shall also need the notion of satisfaction of a quantifier-free $\sigma$-formula in a partial $\textit{rog}$ under a partial assignment, i.e., a partial function from $\textit{Var}$ into the universe of a partial $\textit{rog}$.

For a partial assignment v on a partial $\textit{rog}$ $\textbf{B}$, we recursively define, for every $\sigma$-term t, the relation $\textbf{B}\, {\downarrow }\, v(t)$ (“the value of t in $\textbf{B}$ is defined under v”) as follows:

$$\begin{aligned}&\textbf{B}\, {\downarrow }\, v(x_i)~~~~~~~~~~~~ \Longleftrightarrow ~~~~~~~~~~ x_i \in {{\,\textrm{dom}\,}}(v); \\&\textbf{B}\, {\downarrow }\, v(t_1 \star t_2) ~~~~~~~~ \Longleftrightarrow ~~~~~~~~~~ \textbf{B}\, {\downarrow }\, v(t_1), \textbf{B}\, {\downarrow }\, v(t_2) \hbox {and} \langle v(t_1), v(t_2) \rangle \in {{\,\textrm{dom}\,}}(\star ^\textbf{B}),\\&~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \text{ where }\, \star \in \{\circ , \backslash , /\}. \end{aligned}$$

Next, for a partial assignment v on a partial $\textit{rog}$ $\textbf{B}$, we recursively define, for every quantifier-free $\sigma$-formula $\varphi$, the relations $\textbf{B}\models ^v \varphi$ (“$\varphi$ is satisfied in $\textbf{B}$ under v”), $\textbf{B}\not \models ^v \varphi$ (“$\varphi$ is not satisfied in $\textbf{B}$ under v”) and (“the truth value of $\varphi$ in $\textbf{B}$ under v is undefined”) as follows:

We say that a quantifier-free $\sigma$-formula $\varphi$ is satisfiable in a partial $\textit{rog}$ $\textbf{B}$ if there exists a partial assignment v on $\textbf{B}$ such that $\textbf{B}\models ^v \varphi$.

Intuitively, $\textbf{B}\models ^v \varphi$ (respectively, $\textbf{B}\not \models ^v \varphi$) means that the relation $\textbf{B}\, {\downarrow }\, v(t)$ holds for enough terms $t \in \textit{Ter}(\varphi )$ for us to be able to compute the ‘truth value’ of $\varphi$ in $\textbf{B}$ under v as true (respectively, false).

More precisely, we use, in metalanguage, a 3-valued logic with the values ‘true’, ‘false’ and ‘undefined’ (for short, u). The 3-valued logic we use agrees with the 3-valued Łukasiewicz logic in the definitions of not, & and or, but differs in the definition of implication: $u \rightarrow u$ is u in the logic we use, but true in the Łukasiewicz logic. In our earlier papers (Shkatov & Van Alten, 2019, 2020, 2021), satisfaction in partial structures was defined slightly differently, in effect using a 3-valued logic where the result of a logical operation is undefined whenever at least one of the operands is undefined. The difference between the two approaches has no impact on any of our results.

We shall use the following observation in the proof of Theorem 2 below. Let $\textbf{B}$ be a partial rog, $\varphi$ a quantifier-free $\sigma$-formula and v be a partial assignment on $\textbf{B}$ such that $\textbf{B}\models ^{v} \varphi$. Let $v'$ be a (full) assignment on $\textbf{B}$ extending v. Observe that, if $x \notin \textit{Var}(\varphi )$, then the value of x under $v'$ is irrelevant to the satisfaction of $\varphi$ in $\textbf{B}$ under $v'$. Also observe that, if $x \in \textit{Var}(\varphi )$, but $x \notin dom(v)$, then the value of x under $v'$ is, again, irrelevant to the satisfaction of $\varphi$ in $\textbf{B}$ under $v'$. Formally, it can be shown by induction that if $\textbf{B}\models ^{v} \varphi$ (respectively, $\textbf{B}\not \models ^{v} \varphi$), then $\textbf{B}\models ^{v'} \varphi$ (respectively, $\textbf{B}\not \models ^{v'} \varphi$).

We now relate satisfiability in $\textit{rog}$s and partial $\textit{rog}$s. We define the size of a quantifier-free $\sigma$-formula $\varphi$, denoted $size(\varphi )$, to be the number of variables in $\varphi$ plus the total number of occurrences of operation symbols in $\varphi$. To be consistent with the literature, we use the standard measure of the complexity of an input formula $\varphi$, its length, defined in the standard way as the number of occurrences of symbols in $\varphi$, and denoted by $len(\varphi )$. The running time of our algorithms is, however, more appropriately measured by the size of a formula. Since, evidently, $size(\varphi ) \leqslant len(\varphi )$, whenever we prove the existence of an algorithm running in $\mathcal {O} (f(size(\varphi )))$ we, thereby, establish the existence an algorithm running in $\mathcal {O} (f(len(\varphi )))$, whatever function f is.

The following theorem is a special case of Van Alten (2013, Theorem 2.1); we include a proof of this special case for the reader’s convenience.

Theorem 2

A quantifier-free $\sigma$-formula $\varphi$ is satisfiable in $\mathcal {ROG}$ if, and only if, it is satisfiable in a partial $\textit{rog}$ whose cardinality does not exceed $size(\varphi )$.

Proof

Assume $\textbf{A}\models ^v \varphi$ for some $\textit{rog}$ $\textbf{A}= \langle A, \circ ^\textbf{A}, \backslash ^\textbf{A}, /^\textbf{A}, \leqslant ^\textbf{A}\rangle$ and some assignment v on $\textbf{A}$. Let $B = \{ v(t) \mid \, t \in \textit{Ter}(\varphi ) \}$. Observe that $|B| \leqslant size(\varphi )$. For all $a, b \in B$ and $\star \in \{\circ , \backslash , /\}$, let $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\star ^{\textbf{B}})$ if there exists $t_1 \star t_2 \in \textit{Ter}(\varphi )$ with $a = v(t_1)$ and $b = v(t_2)$. Then, for every $\star \in \{\circ , \backslash , /\}$ and all $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\star ^{\textbf{B}})$, set $a \star ^{\textbf{B}} b := a \star ^\textbf{A}b$. Lastly, set $\leqslant ^{\textbf{B}} = {\leqslant ^\textbf{A}} \!\!\restriction _B$. Then $\textbf{B}:= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, \leqslant ^{\textbf{B}} \rangle$ is a partial $\textit{rog}$. Let $w := v \!\restriction _{\textit{Var} (\varphi )}$. It should be clear that $\textbf{B}\models ^{w} \varphi$. Thus, $\varphi$ is satisfiable in a partial $\textit{rog}$ of the required cardinality.

Conversely, assume $\textbf{B}\models ^{v} \varphi$ for some partial $\textit{rog}$ $\textbf{B}$ and some partial assignment v on $\textbf{B}$. Then $\textbf{B}$ is a partial substructure of some $\textit{rog}$, say $\textbf{A}$. Let $v'$ be a (full) assignment on $\textbf{B}$ extending v. Then, as observed above, $\textbf{B}\models ^{v'} \varphi$. Since $\textbf{B}$ is a partial substructure of $\textbf{A}$, it follows that $\textbf{A}\models ^{v'} \varphi$. $\square$

Using the above theorem, together with the characterization of partial $\textit{rog}$s given in Theorem 1, we obtain the upper bound for complexity of satisfiability in $\mathcal {ROG}$ and hence also of the universal theory of $\mathcal {ROG}$.

Theorem 3

Satisfiability of quantifier-free $\sigma$-formulas in $\mathcal {ROG}$ is in $\textsf {NP}$. The universal theory of $\mathcal {ROG}$ is in co$\textsf {NP}$.

Proof

Let $\varphi$ be a quantifier-free $\sigma$-formula. Due to Theorem 2, to determine whether $\varphi$ is satisfiable in $\mathcal {ROG}$ it suffices to check if it is satisfiable in a partial $\textit{rog}$ of cardinality not exceeding $size(\varphi )$. To that end, we use the following nondeterministic algorithm.

Guess a partial $\sigma$-structure $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, \leqslant ^\textbf{B}\rangle$ with $|B| \leqslant size(\varphi )$ and a partial assignment v on $\textbf{B}$. Check whether $\textbf{B}$ is a partial rog and whether $\textbf{B}\models ^v \varphi$. If both checks succeed, return “yes”; otherwise, return “no.”

In view of Theorem 1, to check whether $\textbf{B}$ is a partial $\textit{rog}$ it suffices to check properties (i–x), which can be done in time polynomial in |B| and, hence, $size(\varphi )$. Checking whether $\textbf{B}\models ^v \varphi$ can be done in time polynomial in $size(\varphi )$. Thus, the outlined algorithm runs in time polynomial in $size(\varphi )$.

Satisfiability of quantifier-free $\sigma$-formulas in $\mathcal {ROG}$ is, therefore, in $\textsf {NP}$. Since, as we have observed, membership of universal $\sigma$-sentences in the universal theory of $\mathcal {ROG}$ is a complementary problem, the universal theory of $\mathcal {ROG}$ is in co$\textsf {NP}$. This completes the proof. $\square$

For the lower bound, we use the following observation stating a simple condition under which the universal theory of a class of structures is co$\textsf {NP}$-hard. We say that a k-ary predicate P on a structure with domain A is non-trivial if $P \ne \varnothing$ and $P \ne A^k$; we say that a structure is non-trivial if it has a non-trivial predicate definable in its signature.

Theorem 4

Let $\mathcal {K}$ be a class of structures that contains a non-trivial structure. Then, satisfiability of quantifier-free first-order formulas in $\mathcal {K}$ is $\textsf {NP}$-hard and the universal theory of $\mathcal {K}$ is co$\textsf {NP}$-hard.

Proof

The proof is by reduction from the $\textsf {NP}$-hard satisfiability problem for Boolean formulas (Cook, 1971).

Let $\textbf{A}$ be a non-trivial structure in $\mathcal K$ with non-trivial k-ary predicate P. Then there exist $a_1, \dots , a_k, b_1, \dots , b_k$ in the domain of $\textbf{A}$ with $\langle a_1, \ldots , a_k \rangle \in P$ and $\langle b_1, \ldots , b_k \rangle \not \in P$, that is, $P(a_1, \dots , a_k)$ is true and $P(b_1, \dots , b_k)$ is false.

Let $\beta (p_1, \dots , p_n)$ be a Boolean formula. For every $i \in \{ 1, \dots , n \}$ and every $j \in \{ 1, \dots , k \}$, let $q_j^i$ be a new variable. Recursively define the translation $\cdot ^*$:

$$ \begin{aligned} p_i^*:= & {} P(q_1^i, \dots , q_k^i), \quad \text{ for } \text{ every } i \in \{1, \ldots , n\}; \\ (\lnot \gamma _1)^*:= & {} \textsf {not}\, \gamma _1^*; \\ (\gamma _1 \wedge \gamma _2)^*:= & {} \gamma _1^*~ \& ~\gamma _2^*; \\ (\gamma _1 \vee \gamma _2)^*:= & {} \gamma _1^*~\textsf {or}~\gamma _2^*. \end{aligned}$$

Then $\beta ^*$ is a quantifier-free formula in the signature of $\mathcal {K}$. We show that $\beta$ is satisfiable in the two-element Boolean algebra if, and only if, $\beta ^*$ is satisfiable in $\mathcal {K}$.

Assume $\beta$ is satisfiable in the two-element Boolean algebra $\textbf{2}$ with universe $\{0, 1\}$ under assignment v. Let w be an assignment on $\textbf{A}$ such that, for all $i \in \{1, \ldots , n\}$ and $j \in \{1, \ldots , k\}$,

$$\begin{aligned} w(q_j^i) :={\left\{ \begin{array}{ll} a_j ~~ \text{ if } v(p_i) = 1; \\ b_j ~~ \text{ if } v(p_i) = 0. \end{array}\right. } \end{aligned}$$

Then, $\textbf{A}\models ^{w} p_i^*$ if $v(p_i) = 1$, and $\textbf{A}\not \models ^{w} p_i^*$ if $v(p_i) = 0$. It follows, recursively, that $\textbf{A}\models ^{w} \beta ^*$.

Conversely, suppose $\beta ^*$ is satisfiable in $\mathcal K$. Then, $\textbf{B}\models ^{w} \beta ^*$ for some $\textbf{B}\in \mathcal {K}$ and assignment w on $\textbf{B}$. Let v be an assignment on the Boolean algebra $\textbf{2}$ such that

$$\begin{aligned} v(p_i) := {\left\{ \begin{array}{ll} 1 ~~ \text{ if } \textbf{B}\models ^w P(q_1^i, \dots , q_k^i); \\ 0 ~~ \text{ if } \textbf{B}\not \models ^w P(q_1^i, \dots , q_k^i). \end{array}\right. } \end{aligned}$$

It follows that $\textbf{2} \models ^{v} \beta$, as required. $\square$

From Theorems 3 and 4, which is applicable since the signature $\sigma$ contains the relation symbol $\leqslant$, we obtain the following:

Theorem 5

Satisfiability of quantifier-free $\sigma$-formulas in $\mathcal {ROG}$ is $\textsf {NP}$-complete. The universal theory of $\mathcal {ROG}$ is co$\textsf {NP}$-complete.

5 Unital and Integral Residuated Ordered Groupoids

In this section we extend the methods of the previous sections to show that the universal theories of the classes of unital and integral $\textit{rog}$s are co$\textsf {NP}$-complete.

We denote by $\sigma '$ the signature that extends the signature $\sigma$ by a constant 1. A unital residuated ordered grouopid, or $\textit{urog}$, is a $\sigma '$-structure $\textbf{A}= \langle A, \circ , \backslash , /, 1, \leqslant \rangle$, where $\langle A, \circ , \backslash , /, \leqslant \rangle$ is a $\textit{rog}$ and 1 is an identity for $\circ$, i.e., $\textbf{A}$ satisfies $x \circ 1 = x = 1 \circ x$. The class of all $\textit{urog}$s is denoted by $\mathcal {UROG}$. An integral residuated ordered grouopid, or $\textit{irog}$, is a $\textit{urog}$ satisfying $x \leqslant 1$. The class of all $\textit{irog}$s is denoted by $\mathcal {IROG}$.

An embedding of a $\textit{urog}$ (respectively, $\textit{irog}$) into another $\textit{urog}$ (respectively, $\textit{irog}$) is an embedding of an underlying $\textit{rog}$ that, additionally, preserves the identity.

We extend the frame representation theory for $\textit{rog}$s given in Sect. 2 to $\textit{urog}$s and $\textit{irog}$s.

First, we consider $\textit{urog}$s. A $\textit{urog}$-frame is a structure $\mathfrak {F} = \langle P, e, \leqslant , R \rangle$, where $\langle P, \leqslant , R \rangle$ is a $\textit{rog}$-frame and $e \in P$ such that the following hold:

$$ \begin{aligned}&(\forall f \in P)[R(f, e, f) \; \& \; R(e, f, f)]; \end{aligned}$$

(7)

$$\begin{aligned}&(\forall f, h \in P) [R(f, e, h) \Longrightarrow f \leqslant h]; \end{aligned}$$

(8)

$$\begin{aligned}&(\forall g, h \in P)[R(e, g, h) \Longrightarrow g \leqslant h]. \end{aligned}$$

(9)

Let $\langle P, e, \leqslant , R \rangle$ be a $\textit{urog}$-frame. Since $\langle P, \leqslant , R \rangle$ is a $\textit{rog}$-frame we may construct, as in Sect. 3, the $\textit{rog}$ associated with it, that is, $\langle U(P), \circ , \backslash , /, \subseteq \rangle$, where the operations $\circ$, $\backslash$ and / are as defined in (3–5). We observe the following result.

Lemma 1

If $\langle P, e, \leqslant , R \rangle$ be a $\textit{urog}$-frame, then [e) is the identity for the operation $\circ$ on U(P) defined in (3).

Proof

Let $X \in U(P)$; then by (3),

$$\begin{aligned} X \circ [e) = \{ h \in P \mid (\exists f \in X)(\exists g \in [e)) \, R(f, g, h) \}. \end{aligned}$$

If $h \in X \circ [e)$, then there exists $f \in X$ and $g \in [e)$ such that R(f, g, h). Since $e \leqslant g$ we have R(f, e, h), by (2), hence $f \leqslant h$, by (8). Thus, $h \in X$, so $X \circ [e) \subseteq X$. Conversely, if $h \in X$, then, since $e \in [e)$ and R(h, e, h), by (7), we get that $h \in X \circ [e)$. Thus, $X \subseteq X \circ [e)$. Therefore, $X \circ [e) = X$. We can show, similarly, that $[e) \circ X = X$, so [e) is an identity for $\circ$. By standard algebraic methods it follows that [e) is the unique identity for $\circ$. $\square$

Thus, if $\mathfrak {F} = \langle P, e, \leqslant , R \rangle$ is a $\textit{urog}$-frame, then $\textbf{A}_\mathfrak {F} := \langle U(P), \circ , \backslash , /, [e), \subseteq \rangle$ is a $\textit{urog}$ (with $[e) = 1$); we call it the $\textit{urog}$ associated with $\mathfrak {F}$.

If $\textbf{A}= \langle A, \circ , \backslash , /, 1, \leqslant \rangle$ is a $\textit{urog}$, then we can obtain a $\textit{urog}$-frame, as follows. Let R be the ternary relation on U(A) defined as in (6). Then the structure $\langle U(A), \subseteq , R \rangle$ is a $\textit{rog}$-frame. It is straightforward to check that $\mathfrak {F}_\textbf{A}:= \langle U(A), [1), \subseteq , R \rangle$ satisfies (7–9); hence, it is a $\textit{urog}$-frame.

We next consider the class of $\textit{irog}$s. An $\textit{irog}$-frame is a $\textit{urog}$-frame $\mathfrak {F} = \langle P, e, \leqslant , R \rangle$ satisfying

$$\begin{aligned} (\forall f \in P)[e \leqslant f]. \end{aligned}$$

(10)

For any $\textit{irog}$-frame $\mathfrak {F} = \langle P, e, \leqslant , R \rangle$, the $\textit{urog}$ associated with $\mathfrak {F}$, namely, $\textbf{A}_\mathfrak {F} = \langle U(P), \circ , \backslash , /, [e), \subseteq \rangle$, has $[e) = P$, by (10), which is clearly the greatest element of U(P). Thus, $\textbf{A}_\mathfrak {F}$ is an $\textit{irog}$, which we call the $\textit{irog}$ associated with $\mathfrak {F}$.

Let $\textbf{A}= \langle A, \circ , \backslash , /, 1, \leqslant \rangle$ be an $\textit{irog}$. Let $U'(A)$ be the set of all nonempty elements of U(A) and R the ternary relation on $U'(A)$ defined as in (6). Then $\mathfrak {F}'_\textbf{A}= \langle U'(A), \{ 1 \}, \subseteq , R \rangle$ is a $\textit{urog}$-frame. As for $\textit{urog}$s, the constant element e of $\mathfrak {F}'_\textbf{A}$ is [1), which is just $\{ 1 \}$ in this case. In addition, every non-empty upset of A contains 1, so $\{ 1 \}$ is the smallest element of $U'(A)$. Thus, $\mathfrak {F}'_\textbf{A}$ satisfies (10), hence it is an irog-frame.

A partial $\sigma '$ -structure is a structure $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, 1^\textbf{B}, \leqslant ^{\textbf{B}} \rangle$, where $\leqslant ^{\textbf{B}}$ is a binary relation on B, while $\circ ^{\textbf{B}}$, $\backslash ^{\textbf{B}}$ and $/^{\textbf{B}}$ are partial binary operations on B and $1^\textbf{B}\in B$. (Note that the partiality of the binary operations on $\textbf{B}$ does not apply to the constant $1^\textbf{B}$ which is always assumed to be an element of B.) A partial $\textit{urog}$ is a partial $\sigma '$-structure $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, 1^\textbf{B}, \leqslant ^{\textbf{B}} \rangle$ that is a partial substructure of a $\textit{urog}$, i.e., for which there exists a $\textit{urog}$ $\textbf{A}= \langle A, \circ ^\textbf{A}, \backslash ^\textbf{A}, /^\textbf{A}, 1^\textbf{A}, \leqslant ^\textbf{A}\rangle$ such that $B \subseteq A$, $\leqslant ^{\textbf{B}} = {\leqslant ^\textbf{A}} \!\restriction _B$, $1^\textbf{B}= 1^\textbf{A}$ and $a \star ^{\textbf{B}} b = a \star ^\textbf{A}b$ for each $\star \in \{\circ , \backslash , /\}$ and $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\star ^{\textbf{B}})$. Partial $\textit{irog}$s are defined analogously.

An embedding of a partial $\sigma '$-structure $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, \leqslant ^\textbf{B}\rangle$ into a $\sigma '$-structure $\textbf{A}= \langle A, \circ ^\textbf{A}, \backslash ^\textbf{A}, /^\textbf{A}, \leqslant ^\textbf{A}\rangle$ is a map $\alpha : B \rightarrow A$ such that: $a \leqslant ^\textbf{B}b$ if, and only if, $\alpha (a) \leqslant ^\textbf{A}\alpha (b)$, $\alpha (1^\textbf{B}) = 1^\textbf{A}$ and $\alpha (a \star ^\textbf{B}b) = \alpha (a) \star ^\textbf{A}\alpha (b)$ for each $\star \in \{ \circ , \backslash , / \}$ and $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\star ^\textbf{B})$. As in the case of $\textit{rog}$s, embeddings can easily be shown to be injective. In addition, if $\textbf{B}$ is a partial $\sigma '$-structure and there exists an embedding of $\textbf{B}$ into a $\textit{urog}$ (respectively, $\textit{irog}$) $\textbf{A}$, then $\textbf{B}$ is isomorphic to a partial substructure of $\textbf{A}$, that is, $\textbf{B}$ is a partial $\textit{urog}$ (respectively, $\textit{irog}$).

In the following two theorems we give intrinsic characterizations of, respectively, partial $\textit{urog}$s and partial $\textit{irog}$s.

Theorem 6

A partial $\sigma '$-structure $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, 1^\textbf{B}, \leqslant ^\textbf{B}\rangle$ is a partial $\textit{urog}$ if, and only if, it satisfies conditions (i–x) of Theorem 1 and

• (xi) $(\forall a \in B)[\langle a, 1^\textbf{B}\rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}) \Longrightarrow a \circ ^\textbf{B}1^\textbf{B}= a]$;

• (xii) $(\forall a \in B)[\langle 1^\textbf{B}, a \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}) \Longrightarrow 1^\textbf{B}\circ ^\textbf{B}a = a]$.

Proof

As observed in the proof of Theorem 1, conditions (i–x) hold in every partial $\textit{rog}$, hence also in every partial $\textit{urog}$. Conditions (xi) and (xii) hold in every $\textit{urog}$; since they are universal sentences with quantifiers relativized by the domains of the partial operations, it follows that they hold in every partial $\textit{urog}$.

Conversely, suppose $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, 1^\textbf{B}, \leqslant ^{\textbf{B}} \rangle$ is a partial $\sigma '$-structure satisfying the requirements of the theorem. For every $a \in B$, if $\langle 1^\textbf{B}, a \rangle \notin {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$, then we extend the domain of $\circ ^\textbf{B}$ to include $\langle 1^\textbf{B}, a \rangle$ and set $1^\textbf{B}\circ ^\textbf{B}a = a$. We deal similarly with every $a \in B$ for which $\langle a, 1^\textbf{B}\rangle \notin {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$. Then, by (xi) and (xii), $a \circ ^\textbf{B}1^\textbf{B}= a = 1^\textbf{B}\circ ^\textbf{B}a$ for every $a \in B$.

As in Theorem 1, we define a ternary relation $R^\textbf{B}$ on U(B) as follows:

$$ \begin{aligned} R^\textbf{B}(f,g,h)&\iff (\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}))\, [a \in f ~ \& ~ b \in g \Longrightarrow a \circ ^\textbf{B}b \in h]\, \\&\quad \quad \quad ~ \& ~ (\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B}))\, [a \in f ~ \& ~ a \backslash ^\textbf{B}b \in g \Longrightarrow b \in h]\,\\&\quad \quad \quad ~ \& ~ (\forall \langle a, b \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B}))\, [a /^\textbf{B}b \in f ~ \& ~ b \in g \Longrightarrow a \in h]. \end{aligned}$$

Let $\mathfrak {F} := \langle U(B), [1^\textbf{B}), \subseteq , R^\textbf{B}\rangle$; we show that $\mathfrak {F}$ is a $\textit{urog}$-frame. As noted in the proof of Theorem 1, $\langle U(B), \subseteq , R^\textbf{B}\rangle$ is a $\textit{rog}$-frame. We next show that $\mathfrak {F}$ is a $\textit{urog}$-frame, that is, it satisfies (7–9).

To see that $\mathfrak {F}$ satisfies (7), let $f \in U(B)$; we must show that $R^\textbf{B}(f, [1^\textbf{B}), f)$ and $R^\textbf{B}([1^\textbf{B}), f, f)$. Suppose that $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B}$) for some $a \in f$ and $b \in [1^\textbf{B})$. Then, $1^\textbf{B}\leqslant ^\textbf{B}b$, so $a \circ ^\textbf{B}1^\textbf{B}\leqslant ^\textbf{B}a \circ ^\textbf{B}b$, by (ii), hence $a \leqslant ^\textbf{B}a \circ ^\textbf{B}b$, so $a \circ ^\textbf{B}b \in f$. Next, suppose that $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(\backslash ^\textbf{B})$, where $a \in f$ and $a \backslash ^\textbf{B}b \in [1^\textbf{B})$. By an application of (iii), since $a \leqslant ^\textbf{B}a$ and $1^\textbf{B}\leqslant ^\textbf{B}a \backslash ^\textbf{B}b$, we obtain that $a \circ ^\textbf{B}1^\textbf{B}\leqslant ^\textbf{B}b$, i.e., $a \leqslant ^\textbf{B}b$. Thus, $b \in f$, as required. Lastly, suppose that $\langle a, b \rangle \in {{\,\textrm{dom}\,}}(/^\textbf{B})$, where $a /^\textbf{B}b \in f$ and $b \in [1^\textbf{B})$. By an application of (iv) , since $a /^\textbf{B}b \leqslant ^\textbf{B}a /^\textbf{B}b$ and $1^\textbf{B}\leqslant ^\textbf{B}b$, we obtain that $(a /^\textbf{B}b) \circ ^\textbf{B}1^\textbf{B}\leqslant ^\textbf{B}a$, i.e., $a /^\textbf{B}b \leqslant ^\textbf{B}a$. Thus, $a \in f$, as required. This show shows that $R^\textbf{B}(f, [1^\textbf{B}), f)$; a similar proof shows that $R^\textbf{B}([1^\textbf{B}), f, f)$.

To see that $\mathfrak {F}$ satisfies (8), let $f, h \in U(B)$ such that $R^\textbf{B}(f, [1^\textbf{B}),h)$; we must show that $f \subseteq h$. Let $a \in f$. Since $1^\textbf{B}\in [1^\textbf{B})$ and $\langle a, 1^\textbf{B}\rangle \in {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$, we get that $a \circ ^\textbf{B}1^\textbf{B}\in h$. Since $a \circ ^\textbf{B}1^\textbf{B}= a$, it follows that $a \in h$, as required. A similar argument shows that $\mathfrak {F}$ satisfies (9).

Let $\textbf{A}_\mathfrak {F} = \langle U(U(B)), \circ , \backslash , /, [[1^\textbf{B})), \subseteq \rangle$ be the $\textit{urog}$ associated with $\mathfrak {F}$. It can be shown, as in the proof of Theorem 1, that the map $\mu :B \rightarrow U(U(B))$ defined by $\mu (a) = \{ f \in U(B) \mid a \in f \}$ is an embedding of $\textbf{B}$ into $\textbf{A}_\mathfrak {F}$; we need only check additionally that $\mu (1^\textbf{B}) = [[1^\textbf{B}))$, which is immediate. This completes the proof. $\square$

Theorem 7

A partial $\sigma '$-structure $\textbf{B}= \langle B, \circ ^\textbf{B}, \backslash ^\textbf{B}, /^\textbf{B}, 1^\textbf{B}, \leqslant ^\textbf{B}\rangle$ is a partial $\textit{irog}$ if, and only if, it satisfies conditions (i–x) of Theorem 1, conditions (xi) and (xii) of Theorem 6 and

• (xiii) $(\forall a \in B)[a \leqslant ^\textbf{B}1^\textbf{B}]$.

Proof

Conditions (i–xiii) hold in any $\textit{irog}$, hence also in every partial $\textit{irog}$.

Conversely, suppose $\textbf{B}= \langle B, \circ ^{\textbf{B}}, \backslash ^{\textbf{B}}, /^{\textbf{B}}, 1^\textbf{B}, \leqslant ^{\textbf{B}} \rangle$ is a partial $\sigma '$-structure satisfying the requirements of the theorem. For every $a \in B$, if $\langle 1^\textbf{B}, a \rangle \notin {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$, then we extend the domain of $\circ ^\textbf{B}$ to include $\langle 1^\textbf{B}, a \rangle$ and set $1^\textbf{B}\circ ^\textbf{B}a = a$. We deal similarly with every $a \in B$ for which $\langle a, 1^\textbf{B}\rangle \notin {{\,\textrm{dom}\,}}(\circ ^\textbf{B})$.

Let $U'(B)$ be the set of all nonempty upsets of $\langle B, \leqslant ^\textbf{B}\rangle$. Define a ternary relation $R^\textbf{B}$ on $U'(B)$ as in Theorems 1 and 6. It can be shown, as in the proof of Theorem 6, that $\mathfrak {F}' = \langle U'(B), \{ 1^\textbf{B}\}, \subseteq , R^\textbf{B}\rangle$ is a $\textit{urog}$-frame. By (xiii), every element of $U'(B)$ contains $1^\textbf{B}$, hence $\{ 1^\textbf{B}\}$ is the smallest set in $U'(P)$, that is, $\mathfrak {F}'$ satisfies (10); hence, $\mathfrak {F}'$ is an $\textit{irog}$-frame.

Let $\textbf{A}_\mathfrak {F'} = \langle U(U'(B)), \circ , \backslash , /, [\{ 1^\textbf{B}\}), \subseteq \rangle$ be the $\textit{irog}$ associated with $\mathfrak {F}'$. Then the map $\mu :B \rightarrow U(U'(B))$ defined by $\mu (a) = \{ f \in U'(B) \mid a \in f \}$ is an embedding of $\textbf{B}$ into $\textbf{A}'_\mathfrak {F}$. This follows as in the proofs of Theorems 1 and 6; we need only check additionally that the upsets utilised in the proofs are nonempty. In the proof of Theorem 1, where it is shown that $g \notin \mu (a \backslash ^\textbf{B}b)$ implies $g \notin \mu (a) \backslash \mu (b)$, the set $h = \{ e \in B \mid e \not \leqslant ^\textbf{B}b \}$ is used. This set is empty in the case that $b = 1^\textbf{B}$, however, we show that it will never be the case that $g \notin \mu (a \backslash ^\textbf{B}1^\textbf{B})$. Using property (v), since $a \le ^\textbf{B}a$ and $a \circ ^\textbf{B}1^\textbf{B}\leqslant ^\textbf{B}1^\textbf{B}$, we get $1^\textbf{B}\leqslant ^\textbf{B}a \backslash ^\textbf{B}1^\textbf{B}$. Thus, $a \backslash ^\textbf{B}1^\textbf{B}= 1^\textbf{B}$, so $a \backslash ^\textbf{B}1^\textbf{B}\in g$ for every nonempty upset g, and so $g \in \mu (a \backslash ^\textbf{B}1^\textbf{B})$. A similar situation exists for $/^\textbf{B}$. $\square$

Quantifier-free $\sigma '$-formulas and universal $\sigma '$-sentences are defined analogously to quantifier-free $\sigma$-formulas and universal $\sigma$-sentences; these may contain the constant 1. The notations and conventions used in this section agree with those introduced in Sect. 4.

Assignments on $\textit{urog}$s and $\textit{irog}$s, as well as partial assignments on partial $\textit{urog}$s and $\textit{irog}$s, are required to assign the identity of the structure to the constant 1. The definitions of satisfaction of quantifier-free $\sigma '$-formulas in $\textit{urog}$s and $\textit{irog}$s, as well as in partial $\textit{urog}$s and $\textit{irog}$s, are analogous to those given in Sect. 4 for $\textit{rog}$s.

The size of a quantifier-free $\sigma '$-formula $\varphi$, denoted $size(\varphi )$, is the number of variables in $\varphi$ plus the total number of occurrences of operation symbols in $\varphi$, plus one (for the constant). The following result is an analogue of Theorem 2.

Theorem 8

A quantifier-free $\sigma '$-formula $\varphi$ is satisfiable in $\mathcal {UROG}$ (respectively, $\mathcal {IROG}$) if, and only if, it is satisfiable in a partial $\textit{urog}$ (respectively, $\textit{irog}$) whose cardinality does not exceed $size(\varphi )$.

Relying on the characterizations of partial $\textit{urog}$s and partial $\textit{irog}$s from Theorems 6 and 7, we obtain the $\textsf {NP}$-upper bound for satisfiability in $\mathcal {UROG}$ and $\mathcal {IROG}$ using an argument analogous to the proof of Theorem 5. The $\textsf {NP}$-lower bound for satisfiability in $\mathcal {UROG}$ and $\mathcal {IROG}$ follows from Theorem 4.

Theorem 9

Satisfiability of quantifier-free $\sigma '$-formulas in both $\mathcal {UROG}$ and $\mathcal {IROG}$ is $\textsf {NP}$-complete. The universal theory of both $\mathcal {UROG}$ and $\mathcal {IROG}$ is co$\textsf {NP}$-complete.

6 Residuated k-Algebras

In this section and the next, we consider generalizations of $\textit{rog}$s in which the $\circ$ operation is replaced by an operation $\textbf{t}$ of arity k, where $k \geqslant 1$, and $\backslash$, / are replaced by k operations $\textbf{r}_1, \dots , \textbf{r}_k$ of arity k, such that k-ary versions of the residuation property (1) hold. We shall refer to such a $\textbf{t}$ as a (k-ary) ‘fusion’ operation and $\textbf{r}_1, \dots , \textbf{r}_k$ as its ‘residuals’. In Sect. 8 we shall consider ‘residuated algebras’ that may contain finitely many fusion operations of varying arities together with their residuals. Such algebras were originally defined by Buszkowski (1989) [see also (Buszkowski, 1998, 2011; Kołowska-Gawiejnowicz, 1997; Kandulski, 1997; Jäger, 2004)].

Let k be an integer with $k \geqslant 1$. We use $\sigma _k$ to denote the signature consisting of $k+1$ operation symbols $\textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k$, each of arity k, together with a binary relation symbol $\leqslant$. A residuated k -algebra, or $\textit{ra}_k$, is a $\sigma _k$-structure $\textbf{A}= \langle A, \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k, \leqslant \rangle$, where $\langle A, \leqslant \rangle$ is a partially ordered set and $\textbf{A}$ satisfies the following k-ary residuation property: for all $a_1, \ldots , a_k, c \in A$ and every $j \in \{1, \ldots , k\}$,

$$\begin{aligned} \textbf{t}(a_1, \dots , a_k) \leqslant c\, \; \Longleftrightarrow \,\; a_j \leqslant \textbf{r}_j(a_1, \dots , a_{j-1}, c, a_{j+1}, \dots , a_k). \end{aligned}$$

(11)

To make the representation of the properties of $\textit{ra}_k$s briefer, we use the following notation: given a non-empty set A, a tuple $\textbf{a} \in A^k$, as well as $i \in \{1, \ldots , k\}$ and $c \in A$, we denote by $\textbf{a}\, [i := c]$ the k-tuple obtained from $\textbf{a}$ by replacing its $i^{\textrm{th}}$ component $a_i$ by c, i.e., the k-tuple $\langle a_1, \ldots , a_{i-1}, c, a_{i+1}, \ldots , a_k \rangle$. Then (11) can be written as

$$\begin{aligned} \textbf{t}(\textbf{a}) \leqslant c\, \Longleftrightarrow \, a_j \leqslant \textbf{r}_j (\textbf{a}\,[j := c]). \end{aligned}$$

First, we prove some properties of residuated k-algebras.

Lemma 2

Let $\textbf{A}= \langle A, \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k, \leqslant \rangle$ be a $\textit{ra}_k$. Then the following hold.

• (a) $\textbf{t}$ is monotone in each coordinate, i.e., for any $b \in A$, $\textbf{a} \in A^k$ and $i \in \{1, \ldots , k\}$,

  $$\begin{aligned} b \leqslant a_i\, \Longrightarrow \, \textbf{t}(\textbf{a}\, [i := b]) \leqslant \textbf{t}(\textbf{a}). \end{aligned}$$

• (b) For every $j \in \{1, \ldots , k\}$, $\textbf{r}_j$ is monotone in the $j^{\textrm{th}}$ coordinate, i.e., for any $b \in A$ and $\textbf{a} \in A^k$,

  $$\begin{aligned} a_j \leqslant b \, \Longrightarrow \, \textbf{r}_j(\textbf{a}) \leqslant \textbf{r}_j(\textbf{a}\, [j := b]). \end{aligned}$$

• (c) For every $j \in \{1, \ldots , k\}$ and $\textbf{a} \in A^k$,

  $$\begin{aligned} \textbf{t} (\textbf{a}\, [j := \textbf{r}_j (\textbf{a})] ) \leqslant a_j. \end{aligned}$$

• (d) For every $j \in \{1, \ldots , k\}$ and $i \in \{1, \ldots , k\} - \{j\}$, $\textbf{r}_j$ is antitone in the $i^{\textrm{th}}$ coordinate, i.e., for any $b \in A$ and $\textbf{a} \in A^k$,

  $$\begin{aligned} b \leqslant a_i\, \Longrightarrow \, \textbf{r}_j(\textbf{a}) \leqslant \textbf{r}_j(\textbf{a}\, [i := b]). \end{aligned}$$

Proof

(a) Observe that $\textbf{t}(\textbf{a}) \leqslant \textbf{t}(\textbf{a})$ implies, by (11), $a_i \leqslant \textbf{r}_i (\textbf{a}\, [i := \textbf{t}(\textbf{a})])$, whence $b \leqslant \textbf{r}_i (\textbf{a}\, [i := \textbf{t}(\textbf{a})])$, and so, by (11), $\textbf{t}(\textbf{a}\, [i := b]) \leqslant \textbf{t}(\textbf{a})$.

(b) Observe that $\textbf{r}_j(\textbf{a}) \leqslant \textbf{r}_j(\textbf{a})$ implies, by (11), $\textbf{t}(\textbf{a}\, [j := \textbf{r}_j(\textbf{a})]) \leqslant a_j$, whence $\textbf{t}(\textbf{a}\, [j := \textbf{r}_j(\textbf{a})]) \leqslant b$, and so, by (11), $\textbf{r}_j(\textbf{a}) \leqslant \textbf{r}_j(\textbf{a}\, [j := b])$.

(c) Observe that $\textbf{r}_j(\textbf{a}) \leqslant \textbf{r}_j(\textbf{a})$ implies, by (11), $\textbf{t} (\textbf{a}\, [j := \textbf{r}_j (\textbf{a})] ) \leqslant a_j$.

(d) If $b \leqslant a_i$ then, by (a), $\textbf{t}(\textbf{a}\, [j := \textbf{r}_j(\textbf{a})] [i := b]) \leqslant \textbf{t}(\textbf{a}\, [j := \textbf{r}_j(\textbf{a})])$, hence, by (c), $\textbf{t}(\textbf{a}\, [j := \textbf{r}_j(\textbf{a})] [i := b] ) \leqslant a_j$. Thus, by (11), $\textbf{r}_j(\textbf{a}) \leqslant \textbf{r}_j (\textbf{a}\, [i := b])$. $\square$

Henceforth, given $i, j, \ell \in \{1, \ldots , k\}$, we often write, for brevity, $i \ne j$ instead of $i \in \{1, \ldots , k\} - \{j\}$ and $i \ne j, i \ne \ell$ instead of $i \in \{1, \ldots , k\} - \{j, \ell \}$.

Lemma 3

Let k be an integer with $k \geqslant 1$ and $\textbf{A}= \langle A, \textbf{t}, \textbf{r}_1, \dots , \textbf{r}_k, \leqslant \rangle$ a $\textit{ra}_k$. Then, for all $\textbf{a}, \textbf{c} \in A^k$ and $j, \ell \in \{1, \ldots , k\}$,

• (a) $\mathop { \& }\limits _{i = 1}^k\, a_i \leqslant c_i \Longrightarrow \textbf{t}(\textbf{a}) \leqslant \textbf{t}(\textbf{c})$;

• (b) $\mathop { \& }\limits _{i\ne j} a_i \leqslant c_i ~ \& ~ a_j \leqslant \textbf{r}_j (\textbf{c}) \Longrightarrow \textbf{t} (\textbf{a}) \leqslant c_j$;

• (c) $\mathop { \& }\limits _{i\ne j} a_i \leqslant c_i ~ \& ~ \textbf{t}(\textbf{c}) \leqslant a_j \Longrightarrow c_j \leqslant \textbf{r}_j(\textbf{a})$;

• (d) $\mathop { \& }\limits _{i\ne j} a_i \leqslant c_i ~ \& ~ c_j \leqslant a_j \Longrightarrow \textbf{r}_j(\textbf{c}) \leqslant \textbf{r}_j(\textbf{a})$;

• (e) $\mathop { \& }\limits _{i\ne j, i \ne \ell } \, a_i \leqslant c_i ~ \& ~ a_\ell \leqslant \textbf{r}_\ell (\textbf{c}) ~ \& ~ c_\ell \leqslant a_j \Longrightarrow c_j \leqslant \textbf{r}_j(\textbf{a})$.

Proof

(a) This follows by repeated applications of Lemma 2(a).

(b) By the assumptions and Lemma 2(a), $\textbf{t}(\textbf{a}) \leqslant \textbf{t} (\textbf{c}\, [j := \textbf{r}_j (\textbf{c})] )$. Since, by Lemma 2(c), $\textbf{t} (\textbf{c}\, [j := \textbf{r}_j (\textbf{c})] ) \leqslant c_j$, it follows that $\textbf{t}(\textbf{a}) \leqslant c_j$.

(c) By the assumptions and Lemma 2(a), $\textbf{t}(\textbf{a}\, [j := c_j]) \leqslant \textbf{t} (\textbf{c})$. Thus, by (11), $c_j \leqslant \textbf{r}_j (\textbf{a}\, [j := \textbf{t}(\textbf{c})])$. By the assumption that $\textbf{t}(\textbf{c}) \leqslant a_j$ and Lemma 2(b), $\textbf{r}_j (\textbf{a}\, [j := \textbf{t}(\textbf{c})]) \leqslant \textbf{r}_j(\textbf{a})$. Thus, $c_j \leqslant \textbf{r}_j(\textbf{a})$.

(d) This follows by applications of Lemma 2(b) and Lemma 2(d).

(e) From the assumption that $c_i \leqslant a_i$, for every $i \in \{1, \ldots , k\} - \{j, \ell \}$, we obtain, by Lemma 2(b), $\textbf{r}_\ell (\textbf{c}) \leqslant \textbf{r}_\ell (\textbf{a}\, [{j} := c_{j}] [\ell := c_\ell ])$. Since, by assumption, $a_\ell \leqslant \textbf{r}_\ell (\textbf{c})$, we obtain $a_\ell \leqslant \textbf{r}_\ell (\textbf{a}\, [{j} := c_{j}] [\ell := c_\ell ] )$, hence, by (11), $\textbf{t}(\textbf{a}\, [{j} := c_{j}]) \leqslant c_\ell$. Since, by assumption $c_\ell \leqslant a_{j}$, we obtain $\textbf{t}(\textbf{a}\, [{j} := c_{j}]) \leqslant a_{j}$, hence, by (11), $c_j \leqslant \textbf{r}_j(\textbf{a})$. $\square$

We extend to $\textit{ra}_k$s the frame representation theory for $\textit{rog}$s outlined in Sect. 2. A $\textit{ra}_k$-frame is a structure $\mathfrak {F} = \langle P, \leqslant , R \rangle$, where $\langle P, \leqslant \rangle$ is a partially ordered set and R is a $(k+1)$-ary relation on P monotone in the last coordinate and antitone in the other coordinates, i.e., such that, for all $f_1, f'_1, \dots , f_k, f'_k, h, h' \in P$,

$$ \begin{aligned} R(f_1, \dots , f_k, h) ~ \& ~ \mathop { \& }\limits _{i=1}^{k} f'_i \leqslant f_i ~ \& ~ h \leqslant h' \Longrightarrow R(f'_1, \dots , f'_k, h'). \end{aligned}$$

(12)

Let $\mathfrak {F} = \langle P, \leqslant , R \rangle$ be a $\textit{ra}_k$-frame and define, for all $X_1, \ldots , X_k \in U(P)$ and $j \in \{1, \ldots , k\}$,

$$ \begin{aligned} \textbf{t}(X_1, \dots , X_k) := \{ h \in P \mid (\exists f_1, \ldots , f_k \in P)\, [ \mathop { \& }\limits _{i=1}^{k} f_i \in X_i ~ \& ~ R(f_1, \ldots , f_k,h)] \}; \end{aligned}$$

and

$$ \begin{aligned}{} & {} \textbf{r}_j(X_1, \ldots , X_k) := \{ f_j \in P \mid (\forall f_{i \ne j}, h \in P) \\{} & {} \quad \mathop { \& }\limits _{i \ne j} f_i \in X_i ~ \& ~ R(f_1,\ldots , f_k, h) \Longrightarrow h \in X_j ] \}. \end{aligned}$$

Since $\mathfrak {F}$ satisfies (12), so defined $\textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k$ are operations on U(P). The definitions of $\textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k$ ensure that (11) is satisfied with respect to the partial order $\subseteq$ on U(P). Thus, $\textbf{A}_\mathfrak {F} = \langle U(P), \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k, \subseteq \rangle$ is a $\textit{ra}_k$, which we call the $\textit{ra}_k$ associated with $\mathfrak {F}$.

If $\textbf{A}= \langle A, \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k, \leqslant \rangle$ is a $\textit{ra}_k$, then we may obtain a $\textit{ra}_k$-frame as follows. Define a $(k+1)$-ary relation R on U(A) by

$$ \begin{aligned} R(f_1, \dots , f_k, h) \;\, \Longleftrightarrow \;\, (\forall \textbf{a} \in A^k)\, \left[ \mathop { \& }\limits _{i=1}^{k} a_i \in f_i \Longrightarrow \textbf{t}(\textbf{a}) \in h\right] . \end{aligned}$$

Then $\mathfrak {F}_\textbf{A}= \langle U(A), \subseteq , R \rangle$ is a $\textit{ra}_k$-frame.

7 Partial $\sigma _k$-Structures and Partial $\textit{ra}_k$s

Let k be an integer with $k \geqslant 1$. A partial $\sigma _k$ -structure is a structure $\textbf{B}= \langle B, \textbf{t}^{\textbf{B}}, \textbf{r}_1^{\textbf{B}}, \ldots , \textbf{r}_k^{\textbf{B}}, \leqslant ^{\textbf{B}} \rangle$, where $\leqslant ^{\textbf{B}}$ is a binary relation on B and $\textbf{t}^{\textbf{B}}$ and $\textbf{r}_j^{\textbf{B}}$, for every $j \in \{1, \ldots , k\}$, are partial k-ary operations on B, i.e., partial functions from $B^k$ into B. The domains of $\textbf{t}^{\textbf{B}}$ and $\textbf{r}_j^{\textbf{B}}$, for every $j \in \{1, \ldots , k\}$, are denoted by, respectively, ${{\,\textrm{dom}\,}}(\textbf{t}^{\textbf{B}})$ and ${{\,\textrm{dom}\,}}(\textbf{r}_j^{\textbf{B}})$. A partial $\textit{ra}_k$ is a partial $\sigma _k$-structure $\textbf{B}= \langle B, \textbf{t}^{\textbf{B}}, \textbf{r}_1^{\textbf{B}}, \ldots , \textbf{r}_k^{\textbf{B}}, \leqslant ^{\textbf{B}} \rangle$ that is a partial substructure of a $\textit{ra}_k$, i.e., for which there exists a $\textit{ra}_k$ $\textbf{A}= \langle A, \textbf{t}^\textbf{A}, \textbf{r}_1^\textbf{A}, \ldots , \textbf{r}_k^\textbf{A}, \leqslant ^\textbf{A}\rangle$ such that $B \subseteq A$, $\leqslant ^{\textbf{B}} = {\leqslant ^\textbf{A}}\!\restriction _B$ and

• $\textbf{t}^{\textbf{B}} (\textbf{a}) = \textbf{t}^\textbf{A}(\textbf{a})$ for all $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{t}^{\textbf{B}})$;

• $\textbf{r}_j^{\textbf{B}} (\textbf{a}) = \textbf{r}_j^\textbf{A}(\textbf{a})$ for every $j \in \{1, \ldots , k\}$ and all $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^{\textbf{B}})$.

By an embedding of a partial $\sigma _k$-structure $\textbf{B}= \langle B, \textbf{t}^\textbf{B}, \textbf{r}_1^\textbf{B}, \ldots , \textbf{r}_k^\textbf{B}, \leqslant ^\textbf{B}\rangle$ into a $\sigma _k$-structure $\textbf{A}= \langle A, \textbf{t}^\textbf{A}, \textbf{r}_1^\textbf{A}, \ldots , \textbf{r}_k^\textbf{A}, \leqslant ^\textbf{A}\rangle$ we mean a map $\alpha : B \rightarrow A$ such that $a \leqslant ^{\textbf{B}} b$ if, and only if, $\alpha (a) \leqslant ^\textbf{A}\alpha (b)$, and

• $\alpha (\textbf{t}^{\textbf{B}} (\textbf{a})) = \textbf{t}^\textbf{A}(\alpha (\textbf{a}))$ for all $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{t}^{\textbf{B}})$;

• $\alpha (\textbf{r}_j^{\textbf{B}} (\textbf{a})) = \textbf{r}_j^\textbf{A}(\alpha (\textbf{a}))$ for every $j \in \{1, \ldots , k\}$ and all $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^{\textbf{B}})$,

  where $\alpha (\textbf{a})$ denotes $\langle \alpha (a_1), \dots , \alpha (a_k) \rangle$.

For clarity we note that the last condition in the above definition of an embedding is necessary as it does not follow from the other conditions.

We now give an intrinsic characterization of partial $\textit{ra}_k$s, similar to the characterization of partial $\textit{rog}$s given in Theorem 1.

Theorem 10

Let k be an integer with $k \geqslant 1$. A partial $\sigma _k$-structure $\textbf{B}= \langle B, \textbf{t}^{\textbf{B}}, \textbf{r}_1^{\textbf{B}}, \ldots , \textbf{r}_k^{\textbf{B}}, \leqslant ^\textbf{B}\rangle$ is a partial $\textit{ra}_k$ if, and only if, it satisfies the following conditions, for all $j, \ell \in \{1, \ldots , k\}$:

• $(i^{\prime })$ $\langle B, \leqslant ^\textbf{B}\rangle$ is a partially ordered set;

• $(ii^{\prime })$ $(\forall \textbf{a}, \textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B}))\, [ \mathop { \& }\limits _{i = 1}^k\, a_i \leqslant ^\textbf{B}c_i \Longrightarrow \textbf{t}^\textbf{B}(\textbf{a}) \leqslant ^\textbf{B}\textbf{t}^\textbf{B}(\textbf{c})]$;

• $(iii^{\prime })$ $(\forall \textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B}))(\forall \textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B}))\,$ $[\mathop { \& }\limits _{i\ne j} a_i \leqslant ^\textbf{B}c_i ~ \& ~ a_j \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{c}) \Longrightarrow \textbf{t}^\textbf{B}(\textbf{a}) \leqslant ^\textbf{B}c_j]$;

• $(iv^{\prime })$ $(\forall \textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B}))(\forall \textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B}))\,$ $[\mathop { \& }\limits _{i\ne j} a_i \leqslant ^\textbf{B}c_i ~ \& ~ \textbf{t}^\textbf{B}(\textbf{c}) \leqslant ^\textbf{B}a_j \Longrightarrow c_j \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{a})]$;

• $(v^{\prime })$ $(\forall \textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B}))(\forall \textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B}))\,$ $[\mathop { \& }\limits _{i\ne j} a_i \leqslant ^\textbf{B}c_i ~ \& ~ c_j \leqslant ^\textbf{B}a_j \Longrightarrow \textbf{r}_j^\textbf{B}(\textbf{c}) \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{a})]$;

• $(vi^{\prime })$ $(\forall \textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_\ell ^\textbf{B})) (\forall \textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B})) (\forall \textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_\ell ^\textbf{B}))\,$ $[\mathop { \& }\limits _{i\ne j, i \ne \ell } \, a_i \leqslant ^\textbf{B}c_i ~ \& ~ a_\ell \leqslant ^\textbf{B}\textbf{r}_\ell ^\textbf{B}(\textbf{c}) ~ \& ~ c_\ell \leqslant ^\textbf{B}a_j \Longrightarrow c_j \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{a})]$.

Proof

By Lemma 3, conditions (i’–vi’) hold in every $\textit{ra}_k$, hence also in every partial $\textit{ra}_k$.

Conversely, suppose $\textbf{B}= \langle B, \textbf{r}_1^{\textbf{B}}, \ldots , \textbf{r}_k^{\textbf{B}}, \leqslant ^\textbf{B}\rangle$ is a partial $\sigma _k$-structure satisfying (i’–vi’). Define a $(k+1)$-ary relation $R^\textbf{B}$ on U(B) by

$$ \begin{aligned} R^\textbf{B}(f_1, \dots , f_k, h) \iff (\forall \textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B}))[\mathop { \& }\limits _{i=1}^k a_i \in f_i \Longrightarrow \textbf{t}^\textbf{B}(\textbf{a}) \in h]\, ~ \& ~ \\ \mathop { \& }\limits _{j=1}^k(\forall \textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B})) [ \mathop { \& }\limits _{i \ne j} a_i \in f_i ~ \& ~ \textbf{r}_j^\textbf{B}(\textbf{a}) \in f_j \Longrightarrow a_j \in h]. \end{aligned}$$

It is straightforward to check that $\mathfrak {F} = \langle U(B), \subseteq , R^\textbf{B}\rangle$ is a $\textit{ra}_k$-frame. Let $\textbf{A}= \langle U(U(B)), \textbf{t}, \textbf{r}_1, \dots , \textbf{r}_k \rangle$ be the $\textit{ra}_k$ associated with $\mathfrak {F}$, and let $\mu :B \rightarrow U(U(B))$ be the map defined by $\mu (a) = \{ f \in U(B) \mid a \in f \}$. We show that $\mu$ is an embedding of $\textbf{B}$ into $\textbf{A}$. For brevity, for $\textbf{a} \in B^k$, we write $\mu (\textbf{a})$ instead of $\langle \mu (a_1), \ldots , \mu (a_k) \rangle$.

The proof that $a \leqslant ^\textbf{B}b$ if, and only if, $\mu (a) \subseteq \mu (b)$ is as in the proof of Theorem 1. Let $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B})$. We show that $\mu (\textbf{t}^\textbf{B}(\textbf{a})) = \textbf{t}(\mu (\textbf{a}))$, where

$$\begin{aligned} \mu (\textbf{t}^\textbf{B}(\textbf{a})) = \{ h \in U(B) \mid \textbf{t}^\textbf{B}(\textbf{a}) \in h \} \end{aligned}$$

and

$$ \begin{aligned} \textbf{t}(\mu (\textbf{a})) = \{ h \in U(B) \mid (\exists f_1, \ldots , f_k \in U(B))\, [\mathop { \& }\limits _{i = 1}^k a_i \in f_i ~ \& ~ R^\textbf{B}(f_1, \ldots , f_k, h)] \}. \end{aligned}$$

First, assume $h \in \textbf{t}(\mu (\textbf{a}))$. Then there exist $f_1, \ldots , f_k \in U(B)$ such that $a_i \in f_i$, for every $i \in \{1, \ldots , k\}$, and $R^\textbf{B}(f_1, \ldots , f_k,h)$. Thus, by definition of $R^\textbf{B}$, we obtain $\textbf{t}^\textbf{B}(\textbf{a}) \in h$ and so $h \in \mu (\textbf{t}^\textbf{B}(\textbf{a}))$. Therefore, $\textbf{t}(\mu (\textbf{a})) \subseteq \mu (\textbf{t}^\textbf{B}(\textbf{a}))$.

Conversely, assume $h \in \mu (\textbf{t}^\textbf{B}(\textbf{a}))$, i.e., $\textbf{t}^\textbf{B}(\textbf{a}) \in h$. Let $f_i := [a_i)$, for every $i \in \{1, \ldots , k\}$; these sets are clearly in U(B). We show that $R^\textbf{B}(f_1, \ldots , f_k, h)$. Suppose $\textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B})$ and $c_i \in f_i$, for every $i \in \{1, \ldots , k\}$. Then, $a_i \leqslant ^\textbf{B}c_i$, for every $i \in \{1, \ldots , k\}$; hence, by (ii’), $\textbf{t}^\textbf{B}(\textbf{a}) \leqslant ^\textbf{B}\textbf{t}(\textbf{c})$. Since $\textbf{t}^\textbf{B}(\textbf{a}) \in h$ and $h \in U(B)$, we obtain $\textbf{t}^\textbf{B}(\textbf{c}) \in h$. Suppose $j \in \{1, \ldots , k\}$, $\textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B})$, as well as $c_i \in f_i$, for every $i \ne j$, and $\textbf{r}_j^\textbf{B}(\textbf{c}) \in f_j$. Then, $a_i \leqslant c_i$, for every $i \ne j$, and $a_j \leqslant \textbf{r}_j^\textbf{B}(\textbf{c})$, hence, by (iii’), $\textbf{t}^\textbf{B}(\textbf{a}) \leqslant c_j$, whence $c_j \in h$. Thus, $R^\textbf{B}(f_1, \dots , f_k,h)$. Since $a_i \in f_i$, for every $i \in \{1, \ldots , k\}$, we obtain $h \in \textbf{t}(\mu (\textbf{a}))$. Therefore, $\mu (\textbf{t}^\textbf{B}(\textbf{a})) \subseteq \textbf{t}(\mu (\textbf{a}))$.

Let $j \in \{1, \ldots , k\}$ be fixed and let $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B})$. We show that $\mu (\textbf{r}_j^\textbf{B}(\textbf{a})) = \textbf{r}_j(\mu (\textbf{a}))$, where

$$\begin{aligned} \mu (\textbf{r}_j^\textbf{B}(\textbf{a})) = \{ f_j \in U(B) \mid \textbf{r}_j^\textbf{B}(\textbf{a}) \in f_j \} \end{aligned}$$

and

$$ \begin{aligned}{} & {} \textbf{r}_j(\mu (\textbf{a})) = \{ f_j \in U(B) \mid \\{} & {} \quad (\forall f_{i \ne j}, h \in U(B))\, [\mathop { \& }\limits _{i \ne j} a_i \in f_i ~ \& ~ R^\textbf{B}(f_1, \ldots , f_k, h)] \Longrightarrow a_j \in h \}. \end{aligned}$$

First, assume $f_j \in \mu (\textbf{r}_j^\textbf{B}(\textbf{a}))$, i.e., $\textbf{r}_j^\textbf{B}(\textbf{a}) \in f_j$. Suppose $a_i \in f_i$, for all $i \ne j$, and $R^\textbf{B}(f_1, \dots , f_k, h)$. Then, $a_j \in h$, by definition of $R^\textbf{B}$, hence $f_j \in \textbf{r}_j(\mu (\textbf{a}))$.

Conversely, assume $f_j \notin \mu (\textbf{r}_j^\textbf{B}(\textbf{a}))$, i.e., $\textbf{r}_j^\textbf{B}(\textbf{a}) \notin f_j$. To prove that $f_j \notin \textbf{r}_j(\mu (\textbf{a}))$, we show that there exist $f_i \in U(B)$, where $i \in \{1, \ldots , k\} - \{j\}$, and $h \in U(B)$ such that $a_i \in f_i$, for every $i \ne j$, as well as $R^\textbf{B}(f_1, \dots , f_k, h)$ and $a_j \notin h$. Let $f_i := [a_i)$, for all $i \in \{1, \ldots , k\} - \{j\}$, and let $h := \{ b \in B \mid b \not \leqslant ^\textbf{B}a_j \}$; these sets are clearly in U(B). It should also be clear that $a_i \in f_i$, for all $i \ne j$, and that $a_j \notin h$. We next show that $R^\textbf{B}(f_1, \dots , f_k, h)$.

Suppose that $\textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{t}^\textbf{B})$ and $c_i \in f_i$, for every $i \in \{1, \ldots , k\}$. Then, $a_i \leqslant ^\textbf{B}c_i$, for every $i \ne j$. Since, by assumption, $\textbf{r}_j^\textbf{B}(\textbf{a}) \notin f_j$ and $f_j \in U(B)$, it follows that $c_j \not \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{a})$. Then, by (iv’), $\textbf{t}^\textbf{B}(\textbf{c}) \not \leqslant ^\textbf{B}a_j$. Thus, $\textbf{t}^\textbf{B}(\textbf{c}) \in h$, as required.

We show, next, that the second clause of the definition of $R^\textbf{B}$ holds for the j we fixed. Suppose $\textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^\textbf{B})$, as well as $c_i \in f_i$, for all $i \ne j$, and $\textbf{r}_j^\textbf{B}(\textbf{c}) \in f_j$. Then $a_i \leqslant ^\textbf{B}c_i$, for all $i \ne j$. Since $\textbf{r}_j^\textbf{B}(\textbf{a}) \notin f_j$, we also obtain $\textbf{r}_j^\textbf{B}(\textbf{c}) \not \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{a})$; hence, by (v’), $c_j \not \leqslant ^\textbf{B}a_j$. Thus, $c_j \in h$, as required.

We show, last, that the same clause holds for every $\ell \in \{1, \ldots , k\} - \{j\}$. Fix such an $\ell$ and suppose that $\textbf{c} \in {{\,\textrm{dom}\,}}(\textbf{r}_\ell ^\textbf{B})$, as well as $c_i \in f_i$, for all $i \ne \ell$, and $\textbf{r}_\ell ^\textbf{B}(\textbf{c}) \in f_\ell$. Then, $a_i \leqslant ^\textbf{B}c_i$ for every i distinct from $\ell$ and j, and $a_\ell \leqslant \textbf{r}_\ell ^\textbf{B}(\textbf{c})$. Since $\textbf{r}_j^\textbf{B}(\textbf{a}) \notin f_j$, we also obtain $c_j \not \leqslant ^\textbf{B}\textbf{r}_j^\textbf{B}(\textbf{a})$, hence, by (vi’), $c_\ell \not \leqslant ^\textbf{B}a_j$. Thus, $c_\ell \in h$, as required.

Thus, $R^\textbf{B}(f_1, \dots , f_k, h)$, which implies that $f_j \notin \textbf{r}_j(\mu (\textbf{a}))$ and, hence, that $\textbf{r}_j(\mu (\textbf{a})) \subseteq \mu (\textbf{r}_j^\textbf{B}(\textbf{a}))$.

Thus, $\mu$ is an embedding of $\textbf{B}$ into $\textbf{A}$. It follows that $\textbf{B}$ is a partial $\textit{ra}_k$, which completes the proof. $\square$

In the case $k = 2$, the conditions (i’–vi’) of Theorem 10 are equivalent to conditions (i–x) of Theorem 1. In the case $k = 1$, the conditions (i’–vi’) may be presented in a simpler form, as given in the following corollary.

Corollary 1

A partial $\sigma _1$-structure $\textbf{B}= \langle B, \textbf{t}^{\textbf{B}}, \textbf{r}^\textbf{B}, \leqslant ^\textbf{B}\rangle$ is a partial $\textit{ra}_1$ if, and only if, it satisfies the following conditions:

• $(i\prime \prime )$ $\langle B, \leqslant ^\textbf{B}\rangle$ is a partially ordered set;

• $(ii\prime \prime )$ $(\forall a, c \in \textit{dom} (\textbf{t}^{\textbf{B}}))\, [ a \leqslant ^\textbf{B}c \Longrightarrow \textbf{t}^{\textbf{B}} (a) \leqslant \textbf{t}^{\textbf{B}} (c)]$;

• $(iii\prime \prime )$ $(\forall a, c \in \textit{dom} (\textbf{r}^{\textbf{B}}))\, [ a \leqslant ^\textbf{B}c \Longrightarrow \textbf{r}^{\textbf{B}} (a) \leqslant ^\textbf{B}\textbf{r}^{\textbf{B}} (c)]$;

• $(vi\prime \prime )$ $(\forall a \in \textit{dom} (\textbf{t}^{\textbf{B}})) (\forall c \in \textit{dom} (\textbf{r}^{\textbf{B}}))\, [ \textbf{t}^{\textbf{B}} (a) \leqslant ^\textbf{B}c \Longleftrightarrow a \leqslant ^\textbf{B}\textbf{r}^{\textbf{B}} (c)]$.

8 Complexity of the Universal Theory of Residuated Algebras

In this section we consider classes of residuated algebras over fixed signatures that may contain finitely many fusion operations and their residuals. We prove that the universal theory of each such class is co$\textsf {NP}$-complete.

Let k be an integer with $k \geqslant 1$. By a k -residuation tuple, we mean a tuple $\langle \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k \rangle$ of $k+1$ operation symbols, each of arity k. By a residuation signature we mean a signature consisting of a binary relation symbol $\leqslant$ and a finite set of residuation tuples.

Let $\rho$ be a residuation signature. A residuated $\rho$ -algebra, or $ra_\rho$, is a $\rho$-structure $\textbf{A}$, with universe A and binary relation $\leqslant ^\textbf{A}$ such that $\langle A, \leqslant ^\textbf{A}\rangle$ is a partially ordered set and, for each $k \geqslant 1$ and each k-residuation tuple $\langle \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k \rangle$ in $\rho$, $\textbf{A}$ has k-ary operations $\textbf{t}^{\textbf{A}}, \textbf{r}_1^{\textbf{A}}, \dots , \textbf{r}_k^{\textbf{A}}$ such that the structure $\langle A, \textbf{t}^{\textbf{A}}, \textbf{r}_1^{\textbf{A}}, \dots , \textbf{r}_k^{\textbf{A}}, \leqslant ^\textbf{A}\rangle$ is a $\textit{ra}_k$, that is, it satisfies (11). The class of all residuated $\rho$-algebras in denoted by $\mathcal{R}\mathcal{A}_\rho$.

Let $\rho$ be a residuation signature. A partial $\rho$ -structure is a structure $\textbf{B}$ that has universe B, a binary relation $\leqslant ^\textbf{B}$ on B and, for each $k \geqslant 1$ and each k-residuation tuple $\langle \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k \rangle$ in $\rho$, $\textbf{B}$ has corresponding partial k-ary operations $\textbf{t}^{\textbf{B}}, \textbf{r}_1^{\textbf{B}}, \ldots , \textbf{r}_k^{\textbf{B}}$. The domain of each operation $\textbf{f}^\textbf{B}$ in $\textbf{B}$ is denoted by ${{\,\textrm{dom}\,}}(\textbf{f}^{\textbf{B}})$. A partial $\textit{ra}_\rho$ is a partial $\rho$-structure $\textbf{B}$ that is a partial substructure of a $\textit{ra}_\rho$, that is, there exists a $\textit{ra}_\rho$ $\textbf{A}$ with $B \subseteq A$, $\leqslant ^{\textbf{B}} = {\leqslant ^\textbf{A}}\!\restriction _B$ and, for each $k \geqslant 1$ and each k-residuation tuple $\langle \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k \rangle$ in $\rho$,

• $\textbf{t}^{\textbf{B}} (\textbf{a}) = \textbf{t}^\textbf{A}(\textbf{a})$ for all $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{t}^{\textbf{B}})$;

• $\textbf{r}_j^{\textbf{B}} (\textbf{a}) = \textbf{r}_j^\textbf{A}(\textbf{a})$ for every $j \in \{1, \ldots , k\}$ and all $\textbf{a} \in {{\,\textrm{dom}\,}}(\textbf{r}_j^{\textbf{B}})$.

We next give an intrinsic characterization of partial $\textit{ra}_\rho$’s.

Theorem 11

Let $\rho$ be a residuation signature. A partial $\rho$-structure $\textbf{B}$ is a partial $\textit{ra}_\rho$ if, and only if, condition (i’) of Theorem 10 holds and, for each $k \geqslant 1$ and each k-residuation tuple $\langle \textbf{t}, \textbf{r}_1, \ldots , \textbf{r}_k \rangle$ in $\rho$, conditions (ii’–vi’) of Theorem 10 hold.

Proof

The proof is an adaptation of the proof of Theorem 10. If $\textbf{B}$ is a partial $\textit{ra}_\rho$, then the required conditions hold. Conversely, suppose that $\textbf{B}$ is a partial $\rho$-structure satisfying the conditions of the theorem. For each residuation tuple in $\rho$, we define a corresponding relation $R^\textbf{B}$ on U(B) as in the proof of Theorem 10. Next, construct $\textit{ra}_\rho$ $\textbf{A}$ with universe U(U(B)) and operations, corresponding to each relation $R^\textbf{B}$, defined as in Sect. 6. Then the map $\mu : B \rightarrow U(U(B))$ defined by $\mu (a) = \{ f \in U(B) \mid a \in f \}$ can be shown to be an embedding of $\textbf{B}$ into $\textbf{A}$, completing the proof. $\square$

For each residuation signature $\rho$, quantifier-free $\rho$-formulas and universal $\rho$-sentences are defined as in Sect. 4 for the signature $\sigma$. The definition of satisfaction of quantifier-free $\rho$-formulas in $\textit{ra}_\rho$s and partial $\textit{ra}_\rho$s is analogous to that given in Sect. 4 for $\textit{rog}$s. The size of a quantifier-free $\rho$-formula $\varphi$, denoted $size(\varphi )$, is defined as the number of variables in $\varphi$ plus the total number of occurrences of operation symbols in $\varphi$.

The following result is an analogue of Theorem 2.

Theorem 12

Let $\rho$ be a residuation signature. A quantifier-free $\rho$-formula $\varphi$ is satisfiable in $\mathcal{R}\mathcal{A}_\rho$ if, and only if, it is satisfiable in a partial $\textit{ra}_\rho$ whose cardinality does not exceed $size(\varphi )$.

By the above results, following the methods used for $\textit{rog}$s, we obtain the following result.

Theorem 13

Let $\rho$ be a residuation signature. Satisfiability of quantifier-free $\rho$-formulas in $\mathcal{R}\mathcal{A}_\rho$ is $\textsf {NP}$-complete. The universal theory of $\mathcal{R}\mathcal{A}_\rho$ is co$\textsf {NP}$-complete.

9 Conclusion

We conclude by offering some future research directions related to the results presented here. Firstly, it is common in the study of substructural logics—such as NL—that various structural rules are considered alongside the existing set of rules. Structural rules typically correspond to familiar algebraic properties of the related classes of algebras. For example, the exchange rule corresponds to commutativity of the $\circ$ operation in $\textit{rog}$s, while the weakening rule corresponds to the integrality property of $\textit{irog}$s. The computational complexity of the universal theory for such extensions of $\textit{rog}$s may be an interesting research direction. For residuated k-algebras, with $k \geqslant 3$, there may be scope for investigation of structural rules in general, as well as related complexity questions. Classes of residuated 1-algebras have been investigated in the context of ordered sets with a pair of residuated unary operations, or Galois operators, where the ordered set is usually a poset, as in the case here, or a lattice. There seems to be scope for investigating computational complexity questions for various classes of such algebras.