On prevarieties of logic

TL;DR

This paper demonstrates that every prevariety of algebras can be represented as a prevariety of logic, revealing insights into the algebraic semantics of deductive systems and properties of congruence lattices.

Contribution

It establishes the categorical equivalence between prevarieties of algebras and prevarieties of logic, and analyzes properties of congruence lattices in logical varieties.

Findings

Every prevariety of algebras is categorically equivalent to a prevariety of logic.

No nontrivial equation in meet, join, and relational product holds universally in congruence lattices of logical varieties.

Being a (pre)variety of logic is not a categorical property.

Abstract

It is proved that every prevariety of algebras is categorically equivalent to a "prevariety of logic", i.e., to the equivalent algebraic semantics of some sentential deductive system. This allows us to show that no nontrivial equation in the language "meet, join, and relational product" holds in the congruence lattices of all members of every variety of logic, and that being a (pre)variety of logic is not a categorical property.

Equations

$$\big{(}\text{\large\&}_{i\in I,\,j\in J}\,\,\delta_{i}(\rho_{j}(x,y))\approx\varepsilon_{i}(\rho_{j}(x,y))\big{)}\,\Longleftrightarrow\,x\approx y,$$

$$\left(x\to y\approx 1\&y\to x\approx 1\right)⟺x\approx y.$$

$$\mathbf{\tau }(\phi )\text{mbox}:=\text{nolinebreak}\{⟨{\delta }_i(\phi ),{\epsilon }_i(\phi )⟩:i\in I\}$$

$$\mathbf{\tau }[\Gamma ]{\models }_{\mathsf{K}}\mathbf{\tau }(\phi ).)$$

$$\Gamma {⊢}_{\mathsf{K},\mathbf{\tau }}\phi$$

$$⊢$$

$${\mathbf{A}}^{[n]}\text{mbox}:=\text{nolinebreak}⟨A^n,\{m_t:t\in T_{kn}(\mathbf{A}{)}^n\text{ for some positive }k\in \omega \},$$

$$m_t(a_1,\dots ,a_k)=⟨t_i^{\mathbf{A}}(a_{11},\dots ,a_{1n},\dots ,a_{k1},\dots ,a_{kn}):1\le i\le n⟩.$$

$$⟨a,b⟩{\to }^{{\mathbf{A}}^{[2]}}⟨c,d⟩$$

$$⟨a,b⟩{\leftarrow }^{{\mathbf{A}}^{[2]}}⟨c,d⟩$$

$${\square }^{{\mathbf{A}}^{[2]}}⟨a,b⟩$$

$$⟨a,b⟩=⟨c,d⟩$$

$$\big{(}x\to y\approx\Box(x\to y)\;\;\&\;\;x\leftarrow y\approx\Box(x\leftarrow y)\big{)}\Longleftrightarrow x\approx y.$$

$$\mathbf{\tau }(x)=\{⟨x,\square x⟩\}\text{ and }\mathbf{\rho }(x,y)=\{x\to y,x\leftarrow y\}.\text{qed}$$

$$\mathbf{\tau }=\{⟨{\delta }_i,{\epsilon }_i⟩:i=1,\dots ,n\}$$

$$x\approx t_1(x,y,\overline{\delta \rho }(x,y),\overline{\epsilon \rho }(x,y))$$

$$t_i(x,y,\overline{\epsilon \rho }(x,y),\overline{\delta \rho }(x,y))\approx t_{i+1}(x,y,\overline{\delta \rho }(x,y),\overline{\epsilon \rho }(x,y))(1\le i<k)$$

$$t_k(x,y,\overline{\epsilon \rho }(x,y),\overline{\delta \rho }(x,y))\approx y$$

$${\delta }_1({\rho }_1(x,y)),\dots ,{\delta }_n({\rho }_1(x,y)),\dots ,{\delta }_1({\rho }_m(x,y)),\dots ,{\delta }_n({\rho }_m(x,y))$$

$${\epsilon }_1({\rho }_1(x,y)),\dots ,{\epsilon }_n({\rho }_1(x,y)),\dots ,{\epsilon }_1({\rho }_m(x,y)),\dots ,{\epsilon }_n({\rho }_m(x,y))$$

$$\alpha \vee \beta \text{mbox}:=\text{nolinebreak}{\Theta }^{\mathbf{A}}(\alpha \cup \beta )$$

$$\alpha \otimes \beta =\{⟨⟨a,b⟩,⟨c,d⟩⟩:⟨a,c⟩\in \alpha \text{ and }⟨b,d⟩\in \beta \}\in Rel(A^2).$$

$$⟨e_1,g_1⟩,\dots ,⟨e_m,g_m⟩\in \alpha \text{ and }⟨e_{m+1},g_{m+1}⟩,\dots ,⟨e_{2m},g_{2m}⟩\in \beta$$

$$a$$

$$p_i(g_1,\dots ,g_{2m},e_1,\dots ,e_{2m})$$

$$p_k(g_1,\dots ,g_{2m},e_1,\dots ,e_{2m})$$

$$b$$

$$q_i(g_1,\dots ,g_{2m},e_1,\dots ,e_{2m})$$

$$q_k(g_1,\dots ,g_{2m},e_1,\dots ,e_{2m})$$

$${\hat{p}}_i(x_1,\dots ,x_{4m})\text{mbox}:=\text{nolinebreak}$$

$$x_{2m+1},x_{2m+3},\dots ,x_{4m-1},x_{2m+2},x_{2m+4},\dots ,x_{4m});$$

$${\hat{q}}_i(x_1,\dots ,x_{4m})\text{mbox}:=\text{nolinebreak}$$

$$x_{2m+1},x_{2m+3},\dots ,x_{4m-1},x_{2m+2},x_{2m+4},\dots ,x_{4m});$$

$$t_i(z_1,\dots ,z_{2m})\text{mbox}:=\text{nolinebreak}⟨$$

$${\hat{q}}_i({\pi }_1(z_1),{\pi }_2(z_1),\dots ,{\pi }_1(z_{2m}),{\pi }_2(z_{2m}))⟩$$

$$p_i(s_1,s_2,\dots ,s_m,u_1,\dots ,u_m,s_{m+1},\dots ,s_{2m},u_{m+1},\dots ,u_{2m})$$

$$\text{and }{q}_i(s_1,s_2,\dots ,s_m,u_1,\dots ,u_m,s_{m+1},\dots ,s_{2m},u_{m+1},\dots ,u_{2m}).$$

$$⟨a,b⟩=$$

Full text

This work received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 689176 (project “Syntax Meets Semantics: Methods, Interactions, and Connections in Substructural logics”). The first author was supported by project CZ.02.2.69/0.0/0.0/17_050/0008361, OPVVV MŠMT, MSCA-IF Lidské zdroje v teoretické informatice. The second author was supported in part by the National Research Foundation (NRF) of South Africa (UID 85407). Both authors thank the University of Pretoria and the DST-NRF Centre of Excellence in Mathematical and Statistical Sciences (CoE-MaSS) for partially funding the first author’s travel to Pretoria in 2017 and 2018

1. Prevarieties of Logic

Recall that the class operator symbols $\mathbb{I}$, $\mathbb{H}$, $\mathbb{S}$, $\mathbb{P}$ and $\mathbb{P}_{\!\textsc{u}}$ stand for the formation of isomorphic and homomorphic images, subalgebras, direct products and ultraproducts, respectively. A class of similar algebras is called a prevariety, a quasivariety or a variety if it is closed, respectively, under $\mathbb{I}$, $\mathbb{S}$ and $\mathbb{P}$, under $\mathbb{I}$, $\mathbb{S}$, $\mathbb{P}$ and $\mathbb{P}_{\!\textsc{u}}$, or under $\mathbb{H}$, $\mathbb{S}$ and $\mathbb{P}$.

The informal notion of a ‘variety of logic’ has acquired a precise meaning in abstract algebraic logic (see [4, 10, 13]), where it extends naturally to prevarieties. In the standard terminology, a prevariety of logic is the equivalent algebraic semantics of an algebraizable (sentential) logic, but the following purely algebraic characterization can serve here as a definition.

Definition 1**.**

A prevariety $\mathsf{K}$ is called a prevariety of logic if some fixed formula of infinitary logic, having the form

[TABLE]

is valid in (every member of) $\mathsf{K}$. It is understood here that $I$ and $J$ are sets, and that $\bm{\tau}=\{\langle\delta_{i},\varepsilon_{i}\rangle:i\in I\}$ is a family of pairs of unary terms and $\bm{\rho}=\{\rho_{j}:j\in J\}$ a family of binary terms in the signature of $\mathsf{K}$. In this context, $\bm{\tau}$ and $\bm{\rho}$ are called transformers. If, moreover, $\mathsf{K}$ is a [quasi]variety, then we refer to it as a [quasi]variety of logic.∎

Example 2**.**

In the variety of Boolean [resp. Heyting] algebras, which algebraizes classical [resp. intuitionistic] propositional logic, (1) takes the form

[TABLE]

In the variety of commutative residuated lattices [14], which algebraizes a rich fragment of linear logic, (1) is most naturally instantiated as**

$\left((x\rightarrow y)\wedge 1\approx 1\;\;\&\;\;(y\rightarrow x)\wedge 1\approx 1\right)\Longleftrightarrow\,x\approx y$. ∎

Given $\mathsf{K},\bm{\tau}$ and $\bm{\rho}$ as in Definition 1, we can construct a logic $\,\vdash_{\mathsf{K},\bm{\tau}}$ for which $\mathsf{K}$ is the equivalent algebraic semantics, as follows. It is convenient here to fix a proper class $\mathit{Var}$ of variables for the entire discussion.

For each set $X\subseteq\mathit{Var}$, a term $\varphi$ over $X$ in the signature of $\mathsf{K}$ is declared a $\,\vdash^{X}_{\mathsf{K},\bm{\tau}}$-consequence of a set $\Gamma$ of such terms (written as $\Gamma\vdash^{X}_{\mathsf{K},\bm{\tau}}\varphi$) provided that the following is true: for any homomorphism $h$ from the absolutely free algebra ${\bm{T}}(X)$ over $X$ to any member of $\mathsf{K}$, the kernel of $h$ contains

[TABLE]

whenever it contains $\bm{\tau}[\Gamma]\mathrel{\mbox{\,{:}\!}=\nolinebreak}\,\bigcup_{\gamma\in\Gamma}\bm{\tau}(\gamma)$. (This criterion is abbreviated as

[TABLE]

Thus, $\,\vdash^{X}_{\mathsf{K},\bm{\tau}}$ is a binary relation from the power set of $T(X)$ to $T(X)$.

For any two sets $X,Y\subseteq\mathit{Var}$, with $\Gamma\cup\{\varphi\}\subseteq T(X)\cap T(Y)$, it can be verified that $\Gamma\vdash^{X}_{\mathsf{K},\bm{\tau}}\varphi$ iff $\Gamma\vdash^{Y}_{\mathsf{K},\bm{\tau}}\varphi$. It therefore makes sense to write

[TABLE]

Technically, $\,\vdash_{\mathsf{K},\bm{\tau}}$ is the family of relations $\,\vdash^{X}_{\mathsf{K},\bm{\tau}}$ indexed by the subsets $X$ of $\mathit{Var}$. It has the following properties for any sets $X,Y\subseteq\mathit{Var}$, any $\Gamma\cup\Psi\cup\{\varphi\}\subseteq T(X)$ and any homomorphism $h\colon{\bm{T}}(X)\mathrel{-\!\!\!\!\!\rightarrow}{\bm{T}}(Y)$, where we abbreviate $\,\vdash_{\mathsf{K},\bm{\tau}}$ as $\,\vdash$ :

1. (i)

if $\varphi\in\Gamma$, then $\Gamma\vdash\varphi$; 2. (ii)

if $\Gamma\vdash\psi$ for all $\psi\in\Psi$, and $\Psi\vdash\varphi$, then $\Gamma\vdash\varphi$; 3. (iii)

if $\Gamma\vdash\varphi$, then $h[\Gamma]\vdash h(\varphi)$.

For present purposes, (i)–(iii) are the defining properties of logics (over $\mathit{Var}$) in general. Notice that $\,\vdash_{\mathsf{K},\bm{\tau}}$ is defined and is a logic for any class $\mathsf{K}$ of similar algebras and any set $\bm{\tau}$ of pairs of unary terms in its signature (regardless of $\bm{\rho}$ and (1)).

We say that a logic $\,\vdash$ is finitary if it has the following additional property:

1. (iv)

whenever $\Gamma\vdash\varphi$, then $\Gamma^{\prime}\vdash\varphi$ for some finite $\Gamma^{\prime}\subseteq\Gamma$.

In this case, for any infinite set $X\subseteq\mathit{Var}$, the logic $\,\vdash$ is determined by its restriction to terms over $X$, and (iii) need only be stipulated for the endomorphisms $h$ of ${\bm{T}}(X)$. A finitary logic is usually (and can always be) specified by a formal system $\mathbf{F}$ of axioms and finite inference rules, where the natural deducibility relation of $\mathbf{F}$ satisfies (i)–(iv).

Definition 3**.**

If a logic $\,\vdash$ has the form $\,\vdash_{\mathsf{K},\bm{\tau}}$ for some prevariety $\mathsf{K}$ and transformers $\bm{\tau}$ and $\bm{\rho}$, where $\mathsf{K}$ satisfies (1), then $\mathsf{K}$ is said to algebraize $\,\vdash$, and $\,\vdash$ is said to be algebraizable. 111 This implies that $\,\vdash$ and the full equational consequence relation $\models_{\,\mathsf{K}}$ of $\mathsf{K}$ are essentially interchangeable (i.e., the interpretation given by (2) is invertible), but we shall not dwell further on the interpretations here. See [13] for additional motivation.∎

Under these conditions, $\mathsf{K}$ is called the equivalent algebraic semantics of $\,\vdash$, because it is the only prevariety that algebraizes $\,\vdash$; the transformers are essentially unique as well, cf. [4, Thm. 2.15]. A quasivariety that algebraizes two different logics (via different transformers $\bm{\tau}$ and a common $\bm{\rho}$) is exhibited in [4, Sec. 5.2], along with several non-algebraizable finitary logics.

An algebraizable logic is said to be finitely algebraizable if, in its algebraization, the transformer $\bm{\rho}$ can be chosen finite, i.e., the index set $J$ in (1) can be kept finite. That happens, for instance, whenever the equivalent algebraic semantics $\mathsf{K}$ is a quasivariety. Dually, if an algebraizable logic $\,\vdash$ is finitary, then a finite choice of $\bm{\tau}$ (i.e., of $I$) is possible in (1). These facts and the next lemma are proved, for instance, in [13, Lem. 3.37].

Lemma 4**.**

Let $\mathsf{K}$ be a quasivariety of logic, with transformers $\bm{\tau}$ and $\bm{\rho}$ as in (1). Then $\bm{\tau}$ can be chosen finite iff $\,\vdash_{\mathsf{K},\bm{\tau}}$ is finitary.

(The finitely algebraizable finitary logics coincide with the original ‘algebraizable logics’ of Blok and Pigozzi [4]. For cases excluded by their definition, see [17, 27].)

Notice that (1) is valid in a class $\mathsf{K}$ of similar algebras iff it is valid in the prevariety $\mathbb{ISP}(\mathsf{K})$ generated by $\mathsf{K}$. Our focus on prevarieties is therefore not restrictive. In contrast with the case of quasivarieties, it is not provable in the class theory NBG (with choice) that every prevariety has an axiomatization involving only a set of variables [1]. Papers dealing with the algebraization of logics over proper classes of variables include [2, 11, 23].

Remark 5**.**

A variety $\mathsf{K}$ that satisfies $f(x,x,\dots,x)\approx x$ for each of its basic operation symbols $f$ is said to be idempotent. In this case, if (1) is valid in $\mathsf{K}$, then $\mathsf{K}$ satisfies ${\delta_{i}(x)\approx x\approx\varepsilon_{i}(x)}$ for all $i\in I$, making the left hand side of (1) true on any interpretation of $x,y$ in any member of $\mathsf{K}$. In view of the right hand side of (1), this forces $\mathsf{K}$ to be trivial. Thus, no nontrivial idempotent variety is a variety of logic. In particular, a nontrivial variety of lattices cannot be a variety of logic, as it is idempotent. More strikingly, although De Morgan lattices are a modest generalization of Boolean algebras, in essentially the same signature, the variety of De Morgan lattices (which is not idempotent) also fails to be a variety of logic [12]. ∎

2. Category Equivalences

A class $\mathsf{K}$ of similar algebras can be treated as a concrete category, the morphisms being the algebraic homomorphisms between members of $\mathsf{K}$. Termwise equivalent classes are then categorically equivalent, but not conversely.

When a prevariety $\mathsf{K}$ algebraizes a logic $\,\vdash$, we sometimes discover significant features of $\,\vdash$ via ‘bridge theorems’ of the form

[TABLE]

Examples include connections between metalogical interpolation properties and algebraic amalgamation properties [11], between definability theorems and the surjectivity of suitable epimorphisms [2, 23], and between deduction-like theorems and congruence extensibility properties [3, 5, 10].

As it happens, the algebraic properties $Q$ alluded to here are categorical, i.e., they persist under category equivalences between classes $\mathsf{K}$ of the kind to which (3) applies. In such cases, if we wish to establish $P$ for $\,\vdash$, we are not forced to prove $Q$ in $\mathsf{K}$ directly; it suffices to prove $Q$ in an equally suitable class $\mathsf{M}$ that is categorically equivalent to $\mathsf{K}$. 222 The value of this observation lies not only in the hope that $\mathsf{M}$ can be chosen simpler or better-understood than $\mathsf{K}$, but also in the possibility that $\mathsf{M}$ algebraizes a logic $\,\vdash^{\prime}$, different from $\,\vdash$ (perhaps in a different signature). In that situation, a category equivalence $F$ between $\mathsf{M}$ and $\mathsf{K}$ carries positive and negative results from one whole family of logics to another. This is because, in the case of varieties for instance, $F$ induces an isomorphism between the respective sub(quasi)variety lattices of $\mathsf{M}$ and $\mathsf{K}$, along which categorical properties can still be transferred. And the subquasivarieties of $\mathsf{K}$ [resp. $\mathsf{M}$] algebraize the extensions of $\,\vdash$ [resp. $\,\vdash^{\prime}$], with subvarieties corresponding to axiomatic extensions.

That being so, and in view of Remark 5, it is natural to ask which prevarieties are categorically equivalent to prevarieties of logic. We proceed to prove that this is true of every prevariety.

Definition 6**.**

Given an algebra ${\bm{A}}$ and $n\in\omega=\{0,1,2,\dots\}$, we denote by $T_{n}(\bm{A})$ the set of all $n$-ary terms in the signature of $\bm{A}$. For $n>0$, the $n$-th matrix power of $\bm{A}$ is the algebra

[TABLE]

where for each $t=\langle t_{1},\dots,t_{n}\rangle\in T_{kn}(\bm{A})^{n}$, we define $m_{t}\colon(A^{n})^{k}\mathrel{-\!\!\!\!\!\rightarrow}A^{n}$ as follows: if $a_{j}=\langle a_{j1},\dots,a_{jn}\rangle\in A^{n}$ for $j=1,\dots,k$, then

[TABLE]

(Roughly speaking, therefore, the basic operations of $\bm{A}^{[n]}$ are all conceivable operations on $n$-tuples that can be defined using the terms of ${\bm{A}}$.)**

For $0<n\in\omega$, the $n$-th matrix power of a class $\mathsf{K}$ of similar algebras is the class $\mathsf{K}^{[n]}\mathrel{\mbox{\,{:}\!}=\nolinebreak}\,\mathbb{I}\{\bm{A}^{[n]}:\bm{A}\in\mathsf{K}\}$.∎

Applications of the matrix power construction in universal algebra range from the algebraic description of category equivalences and adjunctions [21, 22] to the study of clones [24], Maltsev conditions [29, 15], and finite algebras [18]. Matrix powers are also the basis for ‘twist-product’ constructions and product representations; see for instance [9].

Theorem 7**.**

(cf. [21, Thm. 2.3])* Let $\mathsf{K}$ be a class of similar algebras and $n$ a positive integer. Then $\mathsf{K}^{[n]}$ is a class of similar algebras, which is categorically equivalent to $\mathsf{K}$. Moreover, if $\mathsf{K}$ is a prevariety [resp. a quasivariety; a variety], then so is $\mathsf{K}^{[n]}$*.**

Proof.

It is not difficult to see that the functor $(\cdot)^{[n]}\colon\mathsf{K}\to\mathsf{K}^{[n]}$ sending algebras $\bm{A}\in\mathsf{K}$ to $\bm{A}^{[n]}\in\mathsf{K}^{[n]}$ and replicating homomorphisms componentwise is a category equivalence. And for each class operator $\mathbb{O}$ among $\mathbb{S},\mathbb{P},\mathbb{P}_{\!\textsc{u}},\mathbb{H}$, it is easily verified that $\mathsf{K}$ is closed under $\mathbb{O}$ iff the same is true of $\mathsf{K}^{[n]}$. ∎

We can now prove the main result of this section.

Theorem 8**.**

Let $\mathsf{K}$ be any prevariety. Then $\mathsf{K}$ is categorically equivalent to a prevariety of logic, i.e., to the equivalent algebraic semantics $\mathsf{M}$ of some algebraizable logic $\,\vdash$.**

*Moreover, we can choose $\mathsf{M}$ in such a way that the transformers $\bm{\tau}$ and $\bm{\rho}$ in (1) are finite, and we can arrange that $\mathsf{M}$ is a *[quasi]variety if $\mathsf{K}$ is.

If $\mathsf{K}$ is a quasivariety, then $\,\vdash$ can be chosen finitary.

Proof.

Let $\mathsf{M}$ be the matrix power $\mathsf{K}^{[2]}$. By Theorem 7 and Lemma 4, we need only prove that $\mathsf{M}$ satisfies (1) for some finite transformers $\bm{\tau},\bm{\rho}$ (in which case $\,\vdash_{\mathsf{M},\bm{\tau}}$ can serve as $\,\vdash$).

Now each member of $\mathsf{M}$ has basic binary operations $\to$ and $\leftarrow$, and a basic unary operation $\Box$ such that, for all ${\bm{A}}\in\mathsf{K}$ and $a,b,c,d\in A$,

[TABLE]

where $\pi_{k}(z_{1},\dots,z_{n})\mathrel{\mbox{\,{:}\!}=\nolinebreak}\,z_{k}$ whenever $1\leq k\leq n\in\omega$. These are indeed basic operations for $\mathsf{M}$, because projections are term functions of ${\bm{A}}$.

For every $\bm{A}\in\mathsf{K}$ and $a,b,c,d\in A$, we have

[TABLE]

This implies that the following formula is valid in $\mathsf{M}$:

[TABLE]

In other words, (1) becomes valid in $\mathsf{M}$ when we set

[TABLE]

Corollary 9**.**

The property of being the equivalent algebraic semantics of an algebraizable logic is not preserved by category equivalences between prevarieties, quasivarieties or varieties.

Proof.

This follows from Theorem 8 and Remark 5. ∎

3. Congruence Equations

We have noted that the transformer $\bm{\rho}$ in the definition of a quasivariety of logic can be chosen finite. By a finitary variety of logic, we mean a variety of logic for which the transformer $\bm{\tau}$ can also be chosen finite (i.e., $\,\vdash_{\mathsf{K},\bm{\tau}}$ is finitary—see Lemma 4).

Remark 10**.**

The finitary varieties of logic constitute a Maltsev class in the sense of [28]. Indeed, suppose

[TABLE]

Applying Maltsev’s Lemma (cf. [8, Lem. V.3.1]) to the free $2$-generated algebra in a variety $\mathsf{K}$, we see that (1) is equivalent, over $\mathsf{K}$, to the conjunction of the identities $\delta_{i}(\rho_{j}(x,x))\approx\varepsilon_{i}(\rho_{j}(x,x))$ and a suitable scheme of identities

[TABLE]

involving terms $t_{1},\dots,t_{k}$, where $\overline{\delta\rho}(x,y)$ [resp. $\overline{\varepsilon\rho}(x,y)$] abbreviates

[TABLE]

If we leave the term symbols $\delta_{i},\varepsilon_{i},\rho_{j},t_{r}$ unspecified, then the finite conjunction above defines a strong Maltsev class, which need not be idempotent (e.g., the variety $\mathsf{M}$ in the proof of Theorem 8 does not satisfy $\Box x\approx x$ when $\mathsf{K}$ is a variety). There are only denumerably many such formal conjunctions, and any two of them have a common weakening of the same form, got by maximizing, for each of the letters $\delta,\varepsilon,\rho,t$, the number of subscripted occurrences of that letter. The finitary varieties of logic are therefore directed by the interpretability relation, whence they form a Maltsev class. 444 Alternatively, it can be verified that the non-indexed product of two finitary varieties of logic is a finitary variety of logic; see [19, 25, 28] for the pertinent characterizations.**∎

Despite this observation, Theorem 8 allows us to show, by an elementary argument, that finitary varieties of logic are not forced to satisfy any interesting ‘congruence equation’ in the sense of the next definition. This contrasts with the fact that the most familiar varieties of logic—the ‘point-regular’ varieties—are congruence modular and congruence $n$-permutable for a suitable finite $n$ [16]. (They include the varieties in Example 2.)

Definition 11**.**

A congruence equation is a formal equation in the binary symbols $\land$, $\lor$ and $\circ$. It is satisfied by an algebra $\bm{A}$ if it becomes true whenever we interpret the variables of the equation as congruence relations of $\bm{A}$, and for arbitrary binary relations $\alpha$ and $\beta$ on $A$, we interpret $\alpha\land\beta$, $\alpha\lor\beta$ and $\alpha\circ\beta$ as $\alpha\cap\beta$,  $\Theta^{\bm{A}}(\alpha\cup\beta)$ and the relational product, respectively. (Here, $\Theta^{\bm{A}}$ stands for congruence generation in ${\bm{A}}$.) A congruence equation is satisfied by a class of algebras if it is satisfied by every member of the class. It is nontrivial if some algebra fails to satisfy it.∎

Because $\circ$ is not generally a binary operation on congruences, we associate with each algebra $\bm{A}$ another algebra ${\bm{\mathit{Rel}}}(\bm{A})=\langle\mathit{Rel}(A);\cap,\lor,\circ\rangle$, where $\mathit{Rel}(A)$ is the set of all binary relations on $A$, and

[TABLE]

The congruence lattice of ${\bm{A}}$ is therefore a subalgebra of the $\cap,\lor$ reduct of ${\bm{\mathit{Rel}}}(\bm{A})$. Given $\alpha,\beta\in\mathit{Rel}({\bm{A}})$, we also define

[TABLE]

For congruences $\alpha,\beta$ of ${\bm{A}}$, it is well known that $\alpha\otimes\beta$ is a congruence of the algebra ${\bm{A}}^{2}$, but in fact it is also a congruence of ${\bm{A}}^{[2]}$. This follows straightforwardly from the definitions of ${\bm{A}}^{[2]}$ and $\alpha\otimes\beta$.

Recall that a polynomial of an algebra $\langle A;F\rangle$ is a term function of the algebra $\langle A;F\cup F_{0}\rangle$, where $F_{0}$ consists of the elements of $A$, considered as nullary basic operations. (Of course, we arrange first that $A\cap F=\emptyset$.)

Lemma 12**.**

Let $\bm{A}$ be an algebra. Then $\lambda\colon\alpha\mapsto\alpha\otimes\alpha$ defines an embedding of ${\bm{\mathit{Rel}}}(\bm{A})$ into ${\bm{\mathit{Rel}}}(\bm{A}^{[2]})$,* which maps congruences to congruences. *

Proof.

It is easily verified that, as a function from ${\bm{\mathit{Rel}}}(\bm{A})$ to ${\bm{\mathit{Rel}}}(\bm{A}^{[2]})$, $\lambda$ is injective, $\cap$-preserving and $\circ$-preserving. Let $\alpha,\beta\in\textup{Rel}(A)$. We have already mentioned that $\lambda$ preserves congruencehood, from which it follows that $\lambda(\alpha)\lor\lambda(\beta)\subseteq\lambda(\alpha\lor\beta)$. It remains to prove the reverse inclusion.

Accordingly, let $\langle\langle a,b\rangle,\langle c,d\rangle\rangle\in\lambda(\alpha\lor\beta)$, so $\langle a,c\rangle,\langle b,d\rangle\in\alpha\lor\beta$. The closure operator $\Theta^{\bm{A}}$ (on the power set of $A^{2}$) is algebraic, so there exist

[TABLE]

with $\langle a,c\rangle,\langle b,d\rangle\in\Theta^{\bm{A}}\{\langle e_{1},g_{1}\rangle,\dots,\langle e_{m},g_{m}\rangle,\langle e_{m+1},g_{m+1}\rangle,\dots,\langle e_{2m},g_{2m}\rangle\}$ (where $m$ is finite). By Maltsev’s Lemma, therefore, there are finitely many $4m$-ary polynomials $p_{1},\dots,p_{k}$ and $q_{1},\dots,q_{k}$ of ${\bm{A}}$ such that

[TABLE]

for $i=1,\dots,k-1$. For each $i\in\{1,\dots,k-1\}$, the rules

[TABLE]

define two new $4m$-ary polynomials of ${\bm{A}}$ and a $2m$-ary polynomial $t_{i}$ of $\bm{A}^{[2]}$, such that for any $\langle s_{1},u_{1}\rangle,\dots,\langle s_{2m},u_{2m}\rangle\in A^{2}$, the respective first and second co-ordinates of $t_{i}(\langle s_{1},u_{1}\rangle,\dots,\langle s_{2m},u_{2m}\rangle)$ are

[TABLE]

It follows that

[TABLE]

[TABLE]

[TABLE]

for $i=1,\dots,k-1$, whence

[TABLE]

Now let $j\in\{1,\dots,m\}$. By (5),

[TABLE]

For the basic operation $\to^{{\bm{A}}^{[2]}}$ in the proof of Theorem 8, we have

[TABLE]

so $\langle\langle e_{j},e_{m+j}\rangle,\langle g_{j},g_{m+j}\rangle\rangle\in\lambda(\alpha)\lor\lambda(\beta)$, by (7). Then, since $j\in\{1,\dots,m\}$ was arbitrary, (6) yields $\langle\langle a,b\rangle,\langle c,d\rangle\rangle\in\lambda(\alpha)\lor\lambda(\beta)$, as required. ∎

Corollary 13**.**

If a congruence equation fails in an algebra $\bm{A}$,* then it fails in $\bm{A}^{[2]}$*.**

This allows us to prove the main result of this section:

Theorem 14**.**

*Every nontrivial congruence equation fails in some finitary variety of logic, i.e., in a variety that is the equivalent algebraic semantics of some finitely algebraizable finitary logic. *

Proof.

Each nontrivial congruence equation fails in some variety $\mathsf{K}$, hence also in $\mathsf{K}^{[2]}$ (by Corollary 13), which is itself a variety (by Theorem 7). And $\mathsf{K}^{[2]}$ is a finitary variety of logic, by the proof of Theorem 8. ∎

A finitary variety of logic satisfying no nontrivial congruence equation in the signature $\land,\lor$ (excluding $\circ$) was exhibited in [6]. The stronger fact that this variety satisfies no nontrivial idempotent Maltsev condition was pointed out in [7, Sec. 10.1], using [20, Thm. 4.23]. Theorem 14 does not follow from these observations and general results of universal algebra, however, because it is not evident that every nontrivial congruence equation (in the full signature $\land,\lor,\circ$) entails a nontrivial idempotent Maltsev condition, as opposed to a weak Maltsev condition. (This corrects an impression left in the last lines of [7, p. 647], and in [26].) For more on the general connections between these notions, see [20].