--- abstract: | An algebra $\mathbf A = \langle A, \to, 0 \rangle$, where $\to$ is binary and $0$ is a constant, is called an <span>*implication zroupoid*</span> ($\mathcal I$-zroupoid, for short) if $\mathbf A$ satisfies the identities: (I): $(x \to y) \to z \approx ((z' \to x) \to (y \to z)')'$, and (I$_{0}$): $ 0'' \approx 0$, where $x' : = x \to 0$. An implication zroupoid is <span>*symmetric*</span> if it satisfies the identities: $x'' \approx x$ and $(x \to y')' \approx (y \to x')'$. An identity is of <span>*Bol-Moufang type*</span> if it contains only one binary operation symbol, one of its three variables occurs twice on each side, each of the other two variables occurs once on each side, and the variables occur in the same (alphabetical) order on both sides of the identity. In this paper we make a systematic analysis of all $ 60$ identities of Bol-Moufang type in the variety $\mathcal S$ of symmetric $\mathcal I$-zroupoids. We show that $47$ of the subvarieties of $\mathcal S$, defined by the identities of Bol-Moufang type are equal to the variety $\mathcal{SL}$ of $\lor$-semilattices with the least element $0$ and, one of them is equal to $\mathcal S$. Of the remaining 12, there are only $3$ distinct ones. We also give an explicit description of the poset of the (distinct) subvarieties of $\mathcal S$ of Bol-Moufang type. author: - 'Juan M. Cornejo and Hanamantagouda P. Sankappanavar' title: 'Symmetric implication zroupoids and identities of Bol-Moufang type' --- \[section\] \[Lemma\]<span>**THEOREM**</span> \[Lemma\]<span>**CLAIM**</span> \[Lemma\]<span>**COROLLARY**</span> \[Lemma\]<span>**PROPOSITION**</span> \[Lemma\]<span>**EXAMPLE**</span> \[Lemma\]<span>**FACT**</span> \[Lemma\]<span>**DEFINITION**</span> \[Lemma\]<span>**NOTATION**</span> \[Lemma\]<span>**REMARK**</span> <span> This paper has been pubished by Soft Comput onlline on 25 October 2017. DOI 10.1007/s00500-017-2869-z</span> Introduction ============ In 1934, Bernstein gave a system of axioms for Boolean algebras in @bernstein1934postulates using implication alone. Even though his system was not equational, it is not hard to see that one could easily convert it into an equational one by using an additional constant. In 2012, the second author extended this "modified Bernstein's theorem" to De Morgan algebras in @sankappanavarMorgan2012. Indeed, he shows in @sankappanavarMorgan2012 that the varieties of De Morgan algebras, Kleene algebras, and Boolean algebras are term-equivalent, respectively, to the varieties, $\mathcal{DM}$, $\mathcal{KL}$, and $\mathcal{BA}$ (defined below) whose defining axioms use only an implication $\to$ and a constant $0$. The primary role played by the identity (I): $(x \to y) \to z \approx [(z' \to x) \to (y \to z)']'$, where $x' : = x \to 0$, in the axiomatization of each of those new varieties motivated the second author to introduce a new equational class of algebras called "Implication zroupoids" in @sankappanavarMorgan2012. It also turns out that this new variety contains the variety $\mathcal{SL}$ (defined below) which is shown (see @cornejo2015implication) to be term-equivalent to the variety of $\lor$-semilattices with the least element $0$. An algebra $\mathbf A = \langle A, \to, 0 \rangle$, where $\to$ is binary and $0$ is a constant, is called a <span>zroupoid</span>. A zroupoid $\mathbf A = \langle A, \to, 0 \rangle$ is an <span>Implication zroupoid</span> ($\mathcal I$-zroupoid, for short) if $\mathbf A$ satisfies: - \[<span>(I)</span>\] $(x \to y) \to z \approx ((z' \to x) \to (y \to z)')'$, where $x' : = x \to 0$, - $ 0'' \approx 0$. $\mathcal{I}$ denotes the variety of implication zroupoids. The varieties $\mathcal{DM}$, $\mathcal I_{1,0}$, $\mathcal C$ and $\mathcal{SL}$ are defined relative to $\mathcal{I}$, respectively, by the following identities: $$\begin{array}{ll} {\rm (DM)} & (x \to y) \to x \approx x \mbox{ (De Morgan Algebras)}; \\ {\rm (I_{1,0})} & x' \approx x; \\ {\rm (C)} & x \to y \approx y \to x; \\ {\rm (SL)} & x' \approx x \mbox{ and } x \to y \approx y \to x. \end{array}$$ The varieties $\mathcal{KL}$ and $\mathcal{BA}$ are defined relative to $\mathcal{DM}$, respectively, by the following identities: $$\begin{array}{ll} {\rm (KL)} & (x \to x) \to (y \to y) \approx y \to y \mbox{ (Kleene algebras)} ; \\ {\rm (BA)} & x \to x \approx 0' \mbox{ (Boolean algebras)}.\\ \end{array}$$ As proved in @sankappanavarMorgan2012, the variety $\mathcal{I}$ generalizes the variety of De Morgan algebras and exhibits several interesting properties; for example, the identity $x''' \to y \approx x' \to y$ holds in $\mathcal{I}$. Several new subvarieties of $\mathcal{I}$ are also introduced and investigated in @sankappanavarMorgan2012. The (still largely unexplored) lattice of subvarieties of $\mathcal{I}$ seems to be fairly complex. In fact, Problem 6 of @sankappanavarMorgan2012 calls for an investigation of the structure of the lattice of subvarieties of $\mathcal{I}$. The papers @cornejo2015implication, @cornejo2016order and @cornejo2016semisimple have addressed further, but still partially, the above-mentioned problem by introducing new subvarieties of $\mathcal{I}$ and investigating relationships among them. The (currently known) size of the poset of subvarieties of $\mathcal{I}$ is at least 24; but it is still unknown whether the lattice of subvarieties is finite or infinite. Two of the subvarieties of $\mathcal{I}$ are: $\mathcal{I}_{2,0}$ and $\mathcal{MC}$ which are defined relative to $\mathcal{I}$, respectively, by the following identities, where $x \land y := (x \to y')' $ :\ $$\label{eq_I20} \tag{{\rm I}$_{2,0}$} x'' \approx x;$$ $$\label{eq_MC} \tag{MC} x \wedge y \approx y \wedge x.$$ For a somewhat more detailed summary of the results contained in the above-mentioned papers, we refer the reader to the introduction of @cornejo2016derived. Let $\mathbf{A} \in \mathcal{I}$. $\mathbf{A}$ is <span>involutive</span> if $A \in \mathcal{I}_{2,0}$. $\mathbf{A}$ is <span>meet-commutative</span> if $A \in \mathcal{MC}$. $\mathbf{A}$ is <span>symmetric</span> if $\mathbf{A}$ is both involutive and meet-commutative. Let $\mathcal{S}$ denote the variety of symmetric $\mathcal{I}$-zroupoids. In other words, $\mathcal{S} = \mathcal{I}_{2,0} \cap \mathcal{MC}$. In the present paper we are interested in the subvarieties of $\mathcal{S}$ defined by certain <span>*weak associative laws*</span>, called "Bol-Moufang" laws. A precise definition of a <span>*weak associative law*</span> appears in @Ku96, which is essentially restated below. Let $n \in \mathbb{N}$ and let $\mathcal{L} := \langle \times \rangle$, where $\times$ is a binary operation symbol. A (groupoid) term in $\mathcal{L}$ is of length $n$ if the number of occurrences of variables (not necessarily distinct) is $n$. A weak associative law of length $n$ in $\mathcal{L}$ is an identity of the form $p \approx q$, where $p$ and $q$ are of length $n$ and contain the same variables that occur in the same order in both $p$ and $q$ (only the bracketing is possibly different). We note that the identities of <span>*Bol-Moufang type*</span> investigated in @Fe69 are weak associative laws of length 4 in three distinct variables, with one of them repeated (see below for a more precise definition). The following (general) problem presents itself naturally.\ PROBLEM: Let $\mathcal V$ be a given variety of algebras (whose language includes a binary operation symbol, say, $\times$). Investigate the subvarieties of $\mathcal V$ defined by weak associative laws <span>(</span>with respect to $\times$<span>)</span> and their mutual relationships.\ Special cases of the above problem have already been considered in the literature, wherein the weak associative laws are the identities of Bol-Moufang type, and the variety ${\mathcal V}$ is the variety of quasigroups or the variety of loops (see @Fe69, @Ku96, @PV05a, @PV05b). @Fe69 has noted that there are $60$ weak associative laws of length 4 in three distinct variables (with one variable repeated). Since the Moufang laws and the Bol identities were among those $60$ laws, the author of that paper called such identities as those of Bol-Moufang type. For more information about these identities in the context of quasigroups and loops, see @Ku96 [@PV05a; @PV05b]. In this paper and in @cornejo2016weak [@associative], we carry out a complete analysis of weak associative identities of lenth $\leq 4$, in the context of the variety ${\mathcal S}$ of symmetric implication zroupoids. We focus, in this paper, exclusively on the systematic study of the identities of Bol-Moufang type in the context of symmetric implication zroupoids, while @cornejo2016weak [@associative] will focus on the rest of the weak associative identities. Without loss of generality, we will assume that the variables in $p$ and $q$ occur alphabetically. So, we can say (more explicitly) that an identity $p \approx q$, in the language $\langle \to \rangle$, is of *Bol-Moufang type* if: 1. $p$ and $q$ contain the same three variables (chosen alphabetically), 2. the length of $p$ = $4$ = the length of $q$, 3. the order in which the variables appear in $p$ is exactly the same as the order in which they appear in $q$. Let $B$ denote the set of identities of Bol-Moufang type. The systematic notation for the identities in $B$, presented below, was developed in @PV05a. Let $x, y, z$ be all the variables appearing in the identities of $B$. Without loss of generality, we can assume that they appear in the terms in the alphabetical order. Then, the 6 ways in which the 3 variables can form a word of length 4 are shown below:\ $$\begin{aligned} &\rm A: \quad xxyz; \qquad \quad &\rm B: \quad xyxz; \\ &\rm C: \quad xyyz; \qquad \quad &\rm D: \quad xyzx; \\ &\rm E: \quad xyzy; \qquad \quad &\rm F: \quad xyzz.\\\end{aligned}$$ It is clear that there are exactly 5 ways in which a word of size 4 can be bracketed, as given below:\ 1: $o \to (o \to (o \to o))$;\ 2: $o \to ((o \to o) \to o)$;\ 3: $(o \to o) \to (o \to o)$;\ 4: $(o \to (o \to o)) \to o$;\ 5: $((o \to o) \to o) \to o$.\ Let ($X_{ij}$) with $X \in \{\rm A, \dots, \rm F\}$, $1 \leq i < j \leq 5$, denote the identity from $B$ whose left-hand side is bracketed according to $i$, and whose right-hand side is bracketed according to $j$. For instance, ($A_{12}$) is the identity $x \to (x \to (y \to z)) \approx x \to ((x \to y) \to z)$. We note that B$_{15}$ is a Moufang identity, while E$_{25}$ is a Bol identity. It is noted in @Fe69 that there are ($6 \times (4 + 3 + 2 + 1) =) \ 60$ nontrivial identities in B. We will denote by $\mathcal{X}_{ij}$ the subvariety of $\mathcal S$ defined by the identity ($X_{ij}$). We will show in Section 3 that $47$ of these $60$ varieties coincide with $\mathcal{SL}$ (and hence with each other). In Section 4, we prove our main result that there are 4 nontrivial varieties of Bol-Moufang type that are distinct from each other. Furthermore, we describe explicitly the poset formed by them, together with the variety $\mathcal{BA}$ (which is contained in some of them). We would like to acknowledge that the software "Prover 9/Mace 4" developed by McCune @Mc has been useful to us in some of our findings presented in this paper. We have used it to find examples and to check some conjectures. Preliminaries ============= We refer the reader to the standard references @balbesDistributive1974, @burrisCourse1981 and @Ra74 for concepts and results used, but not explained, in this paper. Recall from @sankappanavarMorgan2012 that $\mathcal{SL}$ is the variety of semilattices with a least element $0$. It was shown in @cornejo2015implication that $\mathcal{SL} = \mathcal{C} \cap \mathcal{I}_{1,0} $. The two-element algebras $\mathbf{2_s}$, $\mathbf{2_b}$ were introduced in @sankappanavarMorgan2012. Their operations $\to$ are respectively as follows:\ <span>0.3 </span> $\to$: 0 1 -------- --- --- 0 0 1 1 1 1 <span>0.3 </span> $\to$: 0 1 -------- --- --- 0 1 1 1 0 1 \ \ Notice that $\mathcal{V}(\mathbf{2_b}) = \mathcal{BA}$. Recall also from @cornejo2015implication [Corollary 11.4] \[CorSL\] that $\mathcal{V}(\mathbf{2_s}) = \mathcal{SL}$. The following lemma easily follows from the definition of $\land$ given earlier in the Introduction. \[lemma\_SL\_I10\_C\] $\mathcal{MC} \cap \mathcal{I}_{1,0} \subseteq \mathcal{C} \cap \mathcal{I}_{1,0} = \mathcal{SL}$. <span>**@sankappanavarMorgan2012 [Theorem 8.15]**</span> \[general\_properties\_equiv\] Let $\mathbf A$ be an $\mathcal{I}$-zroupoid. Then the following are equivalent: 1. $0' \to x \approx x$, \[TXX\] 2. $x'' \approx x$, 3. $(x \to x')' \approx x$, \[reflexivity\] 4. $x' \to x \approx x$. \[LeftImplicationwithtilde\] <span>**@sankappanavarMorgan2012**</span> \[general\_properties\] Let $\mathbf A \in \mathcal{I}_{2,0}$. Then 1. $x' \to 0' \approx 0 \to x$, \[cuasiConmutativeOfImplic2\] 2. $0 \to x' \approx x \to 0'$. \[cuasiConmutativeOfImplic\] \[general\_properties3\] \[general\_properties2\] Let $\mathbf A \in \mathcal{I}_{2,0}$. Then $\mathbf A$ satisfies: 1. $(x \to 0') \to y \approx (x \to y') \to y$, \[281014\_05\] 2. $x \to (0 \to x)' \approx x'$, \[291014\_02\] 3. $(y \to x) \to y \approx (0 \to x) \to y$, \[291014\_10\] 4. $(0 \to x) \to (0 \to y) \approx x \to (0 \to y)$, \[311014\_06\] 5. $x \to y \approx x \to (x \to y)$, \[031114\_04\] 6. $0 \to (0 \to x)' \approx 0 \to x'$, \[031114\_07\] 7. $0 \to (x' \to y)' \approx x \to (0 \to y')$, \[071114\_01\] 8. $0 \to (x \to y) \approx x \to (0 \to y)$, \[071114\_04\] 9. $0 \to (x \to y')' \approx 0 \to (x' \to y)$, \[191114\_05\] 10. $x \to (y \to x') \approx y \to x'$, \[281114\_01\] 11. $(x \to y')' \to z \approx x \to (y \to z)$. \[140715\_20\] For the proofs of items (\[281014\_05\]), (\[291014\_02\]), (\[291014\_10\]), (\[031114\_07\]), (\[071114\_01\]), (\[071114\_04\]), (\[191114\_05\]) and (\[281114\_01\]) we refer the reader to @cornejo2015implication [Lemma 2.7]. The proofs of items (\[311014\_06\]) and (\[031114\_04\]) are given in @cornejo2016order [Lemma 2.6], while the proof of the item (\[140715\_20\]) can be found in @cornejo2016derived [Lemma 3.3]. \[lemma\_070616\_01\] Let $\mathbf A \in \mathcal{I}_{2,0}$ such that $\mathbf A \models 0 \to x \approx x$, then $\mathbf A \models (x \to y)' \approx x' \to y'$. Let $a,b \in A$. Hence, we have that $$\begin{array}{lcll} a' \to b' & = & 0 \to (a' \to b') & \mbox{by hyphotesis} \\ &=& a' \to (0 \to b') & \mbox{by Lemma \ref{general_properties2} (\ref{071114_04})}\\ & = & 0 \to (a'' \to b)' & \mbox{by Lemma \ref{general_properties3} (\ref{071114_01})}\\ & = & 0 \to (a \to b)' & \mbox{by (\ref{eq_I20})} \\ & = & (a \to b)' & \mbox{by hyphotesis}. \end{array}$$ This completes the proof. Symmetric $\mathcal{I}$-zroupoids of Bol-Moufang type ===================================================== Recall that the variety $\mathcal{S} = \mathcal{I}_{2,0} \cap \mathcal{MC}$, which was investigated in @cornejo2015implication. Throughout this section, $\mathbf{A} \in \mathcal{S}$. In this section our goal is to prove that 47 of the subvarieties of $\mathcal{S}$ of Bol-Moufang type are equal to $\mathcal{SL}$ and hence are equal to each other. First, we present some new properties of $\mathcal{S}$ which will be useful later in this paper. \[properties\_of\_I20\_MC\] $\mathbf A$ satisfies: 1. $x \to (y \to z) \approx y \to (x \to z)$, \[310516\_01\] 2. $x' \to y \approx y' \to x$, \[310516\_02\] 3. $x \to y \approx y' \to x'$, \[021017\_01\] 4. $x \to y' \approx y \to x'$. \[021017\_02\] Let $a,b,c \in A$. Then 1. $$\begin{array}{lcll} a \to (b \to c) & = & (a \to b')' \to c & \mbox{by Lemma \ref{general_properties3} (\ref{140715_20})} \\ & = & (b \to a')' \to c & \mbox{by (\ref{eq_MC})} \\ & = & b \to (a \to c) & \mbox{by Lemma \ref{general_properties3} (\ref{140715_20})}. \end{array}$$ 2. $$\begin{array}{lcll} a' \to b & = & (a' \to b'')'' & \mbox{by (\ref{eq_I20})} \\ & = & (b' \to a'')'' & \mbox{by (\ref{eq_MC})} \\ & = & b' \to a & \mbox{by (\ref{eq_I20}).} \end{array}$$ 3. $$\begin{array}{lcll} a \to b & = & a'' \to b & \mbox{by (\ref{eq_I20})} \\ & = & b' \to a' & \mbox{by item (\ref{310516_02})} \end{array}$$ 4. $$\begin{array}{lcll} a \to b' & = & a'' \to b' & \mbox{by (\ref{eq_I20})} \\ & = & b'' \to a' & \mbox{by item (\ref{310516_02})} \\ & = & b \to a' & \mbox{by (\ref{eq_I20})} \end{array}$$ \[310516\_09\] Let $\mathbf A \models x \to x \approx x$. Then $\mathbf A \models x' \approx x$. Let $a \in A$. Then $$\begin{array}{lcll} a' & = & (a \to a)' & \mbox{by hypothesis} \\ & = & (a \to a'')' & \mbox{by (\ref{eq_I20})} \\ & = & (a' \to a')' & \mbox{by (\ref{eq_MC})} \\ & = & a'' & \mbox{by hypothesis} \\ & = & a & \mbox{by (\ref{eq_I20})}. \end{array}$$ \[010616\_01\] Let $\mathbf A \models x' \approx x \to x$ and $\mathbf A \models 0' \approx 0$. Then $\mathbf A \models x' \approx x$. Let $a \in A$. Then $$\begin{array}{lcll} a & = & a'' & \mbox{} \\ & = & (a \to a)' & \mbox{by hypothesis} \\ & = & (a \to a) \to 0 & \mbox{} \\ & = & (a \to a) \to 0' & \mbox{by hypothesis} \\ & = & \{(0'' \to a) \to (a \to 0')'\}' & \mbox{by (I)} \\ & = & \{(0 \to a) \to (a \to 0')'\}' & \mbox{by (\ref{eq_I20})} \\ & = & \{(0 \to a) \to (a \to 0)'\}' & \mbox{by hypothesis} \\ & = & \{(0 \to a) \to a''\}' & \mbox{} \\ & = & \{(0 \to a) \to a\}' & \mbox{by (\ref{eq_I20})} \\ & = & \{(a \to a) \to a\}' & \mbox{by Lemma \ref{general_properties3} (\ref{291014_10})} \\ & = & (a' \to a)' & \mbox{by hypothesis} \\ & = & a' & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})}, \end{array}$$ completing the proof. \[040716\_03\] Let $\mathbf A \models 0 \to (x \to x) \approx x \to x.$ Then\ $\mathbf A \models (x \to x) \to (y \to z) \approx ((x \to x) \to y) \to z.$ Let $a,b,c \in A$. Now, $$\begin{array}{lcll} (a \to a) \to b' & = & (0 \to (a \to a)) \to b' & \mbox{by hypothesis} \\ & = & (b' \to (a \to a)) \to b' & \mbox{by Lemma \ref{general_properties2} (\ref{291014_10})} \\ & = & \{(b'' \to b') \to ((a \to a) \to b')' \}' & \mbox{by (I)} \\ & = & \{b' \to ((a \to a) \to b')' \}' & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & \{((a \to a) \to b')'' \to b \}' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & \{((a \to a) \to b') \to b \}' & \mbox{by (\ref{eq_I20})} \\ & = & \{((a \to a) \to 0') \to b \}' & \mbox{by Lemma \ref{general_properties2} (\ref{281014_05})} \\ & = & \{(0 \to (a \to a)') \to b \}' & \mbox{by Lemma \ref{general_properties} (\ref{cuasiConmutativeOfImplic})} \\ & = & \{(0 \to (a \to a'')') \to b \}' & \mbox{by (\ref{eq_I20})} \\ & = & \{(0 \to (a' \to a')) \to b \}' & \mbox{by Lemma \ref{general_properties2} (\ref{191114_05})} \\ & = & \{(a' \to a') \to b \}' & \mbox{by hypothesis} \\ & = & \{(a \to a) \to b \}' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})}. \end{array}$$ Therefore, $$\rm\label{040716_02} \mathbf A \models (x \to x) \to y' \approx ((x \to x) \to y)'.$$ Hence, $$\begin{array}{llll} ((a \to a) \to b) \to c & = c' \to [(a \to a) \to b]' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = c' \to [(a \to a) \to b'] & \mbox{by (\ref{040716_02})} \\ & = (a \to a) \to (c' \to b') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = (a \to a) \to (b \to c) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})}. \end{array}$$ This completes the proof. \[including\_relations\_of\_BA\] $\mathcal{BA} \subseteq \mathcal A_{12}$. It is routine to check that $\mathbf{2_b} \in \mathcal A_{12}$. The proof is complete since we know $\mathcal{V}(\mathbf{2_b}) = \mathcal{BA}$. \[including\_relations\_of\_SL\] $\mathcal{SL} \subseteq \mathcal X_{ij}$, for $\mathcal X \in \{\mathcal A,\mathcal B,\mathcal C,\mathcal D,\mathcal E,\mathcal F\}$ and for all $1 \leq i < j \leq 5$. By a routine computation, it is easy to check that $\mathbf{2_s} \in \mathcal X_{ij}$ for all $1 \leq i < j \leq 5$. Then the proof is complete, in view of $\mathcal{V}(\mathbf{2_s}) = \mathcal{SL}$. Let $\mathbf{M}$ denote the set that contains the subvarieties $\mathcal{A}_{13}$, $\mathcal{A}_{14}$, $\mathcal{A}_{15}$, $\mathcal{A}_{24}$, $\mathcal{A}_{34}$, $\mathcal{A}_{45}$, $\mathcal{B}_{12}$, $\mathcal{B}_{14}$, $\mathcal{B}_{15}$, $\mathcal{B}_{23}$, $\mathcal{B}_{24}$, $\mathcal{B}_{34}$, $\mathcal{B}_{35}$, $\mathcal{B}_{45}$, $\mathcal{C}_{12}$, $\mathcal{C}_{13}$, $\mathcal{C}_{14}$, $\mathcal{C}_{15}$, $\mathcal{C}_{23}$, $\mathcal{C}_{24}$, $\mathcal{C}_{34}$, $\mathcal{C}_{35}$, $\mathcal{C}_{45}$, $\mathcal{D}_{13}$, $\mathcal{D}_{14}$, $\mathcal{D}_{15}$, $\mathcal{D}_{23}$, $\mathcal{D}_{24}$, $\mathcal{D}_{34}$, $\mathcal{D}_{45}$, $\mathcal{E}_{12}$, $\mathcal{E}_{13}$, $\mathcal{E}_{14}$, $\mathcal{E}_{15}$, $\mathcal{E}_{23}$, $\mathcal{E}_{24}$, $\mathcal{E}_{34}$, $\mathcal{E}_{35}$, $\mathcal{E}_{45}$, $\mathcal{F}_{12}$, $\mathcal{F}_{14}$, $\mathcal{F}_{15}$, $\mathcal{F}_{23}$, $\mathcal{F}_{24}$, $\mathcal{F}_{34}$, $\mathcal{F}_{35}$, $\mathcal{F}_{45}$. Observe that $\mathbf{M}$ has $47$ elements. \[theo\_47\_SL\] If $\mathcal X \in \mathbf{M}$ then $\mathcal X = \mathcal{SL} $. In the proof below the following list of statements will be useful. <span>0.1 </span> ($\ast$) <span>0.9 </span> The identity (\[eq\_I20\]), Lemma \[general\_properties\_equiv\] (\[TXX\]), Lemma \[general\_properties\_equiv\] (\[LeftImplicationwithtilde\]), Lemma \[general\_properties2\] (\[281014\_05\]), Lemma \[general\_properties3\] (\[291014\_02\]), Lemma \[general\_properties3\] (\[031114\_04\]) and Lemma \[properties\_of\_I20\_MC\] (\[310516\_01\]). Let $\mathcal X \in M$. In view of Lemma \[including\_relations\_of\_SL\], it suffices to prove that $\mathcal X \subseteq \mathcal{SL}$. In fact, by Lemma \[lemma\_SL\_I10\_C\], it suffices to prove that $\mathcal X \models x' \approx x$. Let $\mathbf A \in \mathcal X$ and let $a \in \mathbf A$. To facilitate a uniform presentation (and to make the proof shorter), we introduce the following notation, where $x_0, y_0, z_0 \in \mathbf A$:\ The notation $$\mathcal X/ x_0, y_0, z_0$$ denotes the following statement: "Given an algebra $\mathbf A \in \mathcal X$, with $\mathcal X$ being defined by the identity $(X)$, consider $x_0, y_0, z_0 \in \mathbf A$. By substituting $x:= x_0, y:= y_0$ and $z:=z_0$ in $(X)$ and simplifying using the list ($\ast$), we obtain a proof of $\mathbf A \models x \to x \approx x$."\ For example, suppose we want to prove that the statement "$\mathcal A_{24}/ a, a', a$" is true. We start with $\mathbf A \in \mathcal A_{24}$ and observe that $$\begin{array}{lcll} a & = & a' \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & (a'' \to a') \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & (a \to a') \to a & \mbox{by (\ref{eq_I20})} \\ & = & (a \to (a \to a')) \to a & \mbox{by Lemma \ref{general_properties3} (\ref{031114_04})} \\ & = & a \to ((a \to a') \to a) & \mbox{by ($A_{2 4}$)} \\ & = & a \to ((a'' \to a') \to a) & \mbox{by (\ref{eq_I20})} \\ & = & a \to (a' \to a) & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & a \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde}).} \end{array}$$ Consequently, $$\mathbf A \models x \approx x \to x.$$ By Lemma \[310516\_09\], $$\mathbf A \models x \approx x'.$$ We divide the 47 varieties under consideration into several groups (again, with a view to making this proof shorter) as follows: Firstly, we consider the varieties associated with the following statements: <span>3</span> 1. $\mathcal A_{24}/ a, a', a$, 2. $\mathcal A_{45}/ a, 0, 0$, 3. $\mathcal B_{12}/ a',a,0$, 4. $\mathcal B_{14}/ a,a,0$, 5. $\mathcal B_{23}/ a',0,0$, 6. $\mathcal B_{24}/ a, 0', 0$, 7. $\mathcal B_{34}/ 0', a, a$, 8. $\mathcal B_{35}/ 0', a, a$, 9. $\mathcal B_{45}/ a, 0', 0$, 10. $\mathcal C_{15}/ 0', a, 0$, 11. $\mathcal C_{23}/ 0', a, 0$, 12. $\mathcal C_{24}/ a, 0, a$, 13. $\mathcal C_{35}/ 0', a, 0$, 14. $\mathcal C_{45}/ a, 0, a$, 15. $\mathcal D_{13}/ a, a', a'$, 16. $\mathcal D_{14}/ a, a, a'$, 17. $\mathcal D_{23}/ a, 0', 0'$, 18. $\mathcal D_{24}/ a, 0', 0'$, 19. $\mathcal D_{45}/ a, 0, 0$, 20. $\mathcal E_{15}/ 0', a, 0'$, 21. $\mathcal E_{23}/ 0', a, 0'$, 22. $\mathcal E_{34}/ 0', a, 0'$, 23. $\mathcal E_{35}/ 0', a, 0'$, 24. $\mathcal F_{24}/ a, a, 0$. It is routine to verify that each of the above statements is true, from which it follows that, in each case, $\mathcal X \models x \to x \approx x$. Then, applying Lemma \[310516\_09\], we get that $\mathcal X \models x' \approx x$.\ The notation $$\mathcal X / x_0, y_0, z_0 / x_1, y_1, z_1\ /p \approx q$$ is an abbreviation for the following statement:\ "Given an algebra $\mathbf A \in \mathcal X$, with $\mathcal X$ being defined by the identity $(X)$, consider $x_0, y_0, z_0 \in \mathbf A$. By substituting $x:= x_0, y:= y_0, z:= z_0$, and simplifying (X) using (the appropriate lemmas from) the list ($\ast$), we obtain a proof of $\mathbf A \models 0' \approx 0$. Then, by substituting $x:= x_1, y:= y_1, z:= z_1$ in the identity (X) and simplifying it, using $0'=0$ and the list ($\ast$), we obtain a proof of $\mathbf A \models p \approx q$."\ Secondly, consider the varieties associated with the following statements: <span>2</span> 1. $\mathcal D_{15} / 0, 0, 0' / 0, a, a\ / x \to x \approx x$, 2. $\mathcal D_{34} / 0, 0, 0 / 0', a, a\ / x \to x \approx x $, 3. $\mathcal E_{13} / 0, 0, 0' / a', 0, a' / x \to x \approx x$, 4. $\mathcal E_{14} / 0, 0, 0 / a, a', 0\ / x \to x \approx x$, 5. $\mathcal E_{24} / 0, 0, 0 / a, 0, a\ / x \to x \approx x$, 6. $\mathcal E_{45} / 0, 0, 0 / a, 0, a\ / x \to x \approx x$. It is straightforward to verify that each of the above statements is true. Hence, it follows that in each case $\mathcal{X} \models x \to x \approx x$. Then, applying Lemma \[310516\_09\], we get that $\mathcal X \models x' \approx x$. Thirdly, consider the varieties associated with the following statements: <span>2</span> 1. $\mathcal A_{14} / 0,0,0 / a, 0', 0\ / x' \approx x, $ 2. $\mathcal F_{14} / 0,0,0 / a, 0, 0\ / x' \approx x, $ 3. $\mathcal F_{23} / 0',0,0 / a, 0, 0\ / x' \approx x, $ 4. $\mathcal F_{34} / 0',0,0 / a, a, 0\ / x' \approx x, $ 5. $\mathcal F_{35} / 0',0,0 / 0', a, 0\ / x' \approx x, $ 6. $\mathcal F_{45} / 0,0,0 / a, 0, 0\ / x' \approx x. $ It is easy to verify that the above statements are true. Hence, it follows in each of the above cases that $\mathcal X \models x' \approx x.$ Lastly, consider the varieties associated with the following statements: 1. $\mathcal A_{15} / 0, 0', 0 / a, 0, 0\ / x' \approx x \to x,$ 2. $\mathcal A_{34} / 0, 0, 0 / a, 0, 0\ / x' \approx x \to x,$ 3. $\mathcal F_{15} / 0', 0, 0 / a, a', 0\ / x' \approx x \to x.$ It is clear that each of the above statements is true. Hence in each case $\mathcal{X} \models x' \approx x \to x $. Then, applying Lemma \[010616\_01\], we get that $\mathcal X \models x' \approx x$. Thus, the varieties still left to consider are $\mathcal A_{13}$, $\mathcal B_{15}$, $\mathcal C_{12}$, $\mathcal C_{13}$, $\mathcal C_{14}$, $\mathcal C_{34}$, $\mathcal E_{12}$ and $\mathcal F_{12}$. From Lemma \[properties\_of\_I20\_MC\] (\[310516\_01\]) we can easily verify that $\mathcal C_{13} = \mathcal B_{12}$, $\mathcal C_{14} = \mathcal B_{14}$, $\mathcal C_{34} = \mathcal B_{24}$, $\mathcal E_{12} = \mathcal D_{13}$, and $\mathcal F_{12} = \mathcal E_{13}$, from which we have, in view of earlier conclusions that $\mathcal C_{13} = \mathcal C_{14} = \mathcal C_{34} = \mathcal E_{12} = \mathcal E_{14} = \mathcal F_{12} = \mathcal{SL}.$ Now, we are left with $\mathcal A_{13}$, $\mathcal B_{15}$, and $\mathcal C_{12}$ to consider. But, it can be easily seen, using Lemma \[properties\_of\_I20\_MC\], that $\mathcal C_{12} =\mathcal A_{13}$. Thus, it only remains to verify that $\mathcal A_{13} = \mathcal{SL}$ and $\mathcal B_{15} = \mathcal{SL}$. First, we show that $\mathcal A_{13} = \mathcal{SL}$. Let $\mathbf A \in \mathcal A_{13}$ and let $a \in A$. Then $$\begin{array}{lcll} a & = & 0' \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & (0 \to 0) \to a & \mbox{} \\ & = & (0 \to 0) \to (a' \to a) & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & 0 \to (0 \to (a' \to a)) & \mbox{by ($A_{1 3}$)} \\ & = & 0 \to (0 \to a) & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & 0 \to a & \mbox{by Lemma \ref{general_properties3} (\ref{031114_04})}. \end{array}$$ Hence $$\label{300516_01} \mathbf A \models x \approx 0 \to x.$$ Therefore $$\begin{array}{lcll} a & = & a' \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & a' \to (a' \to a) & \mbox{by Lemma \ref{general_properties3} (\ref{031114_04})} \\ & = & a' \to (a' \to a'') & \mbox{by (\ref{eq_I20})} \\ & = & a' \to (a' \to (a' \to 0)) & \mbox{} \\ & = & (a' \to a') \to (a' \to 0) & \mbox{by ($A_{1 3}$)} \\ & = & (a' \to a') \to a'' & \mbox{} \\ & = & (a' \to 0') \to a'' & \mbox{by Lemma \ref{general_properties3} (\ref{281014_05})} \\ & = & (0 \to a'') \to a'' & \mbox{by Lemma \ref{general_properties} (\ref{cuasiConmutativeOfImplic})} \\ & = & (0 \to a) \to a & \mbox{by (\ref{eq_I20})} \\ & = & a \to a & \mbox{by (\ref{300516_01})}. \end{array}$$ Using Lemma \[310516\_09\] we have that $\mathbf A \in \mathcal{SL}$, hence $\mathcal A_{13} \subseteq \mathcal{SL}$, implying $\mathcal A_{13} = \mathcal{SL}$. Next, we prove that $\mathcal B_{15} = \mathcal{SL}$. Let $\mathbf A \in \mathcal B_{15}$ and let $a \in A$. Then $$\begin{array}{lcll} a & = & a'' & \mbox{by (\ref{eq_I20})} \\ & = & (a'' \to a')' & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & ((a' \to 0) \to a')' & \mbox{} \\ & = & ((a' \to 0) \to a') \to 0 & \mbox{} \\ & = & a' \to (0 \to (a' \to 0)) & \mbox{by ($B_{1 5}$)} \\ & = & a' \to (0 \to a'') & \mbox{} \\ & = & a' \to (0 \to a) & \mbox{by (\ref{eq_I20})} \\ & = & 0 \to (a' \to a) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & 0 \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})}. \end{array}$$ Hence $$\begin{array}{lcll} a & = & a'' & \mbox{by (\ref{eq_I20})} \\ & = & (a'' \to a')' & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & (a \to a')' & \mbox{by (\ref{eq_I20})} \\ & = & (a \to (a \to 0))' & \mbox{} \\ & = & (a \to (a \to (a \to 0)))' & \mbox{by Lemma \ref{general_properties3} (\ref{031114_04})} \\ & = & ((a \to a) \to a)'' & \mbox{by ($B_{1 5}$)} \\ & = & (a \to a) \to a & \mbox{by (\ref{eq_I20})} \\ & = & (0 \to a) \to a & \mbox{by Lemma \ref{general_properties2} (\ref{291014_10})} \\ & = & a \to a & \mbox{by previous calculus.} \end{array}$$ Thus, $$\mathbf A \models x \approx x \to x.$$ By Lemma \[310516\_09\] we have that $\mathbf A \models x' \approx x$, implying that $\mathcal B_{15} \subseteq \mathcal{SL}$. So, $\mathcal B_{15} = \mathcal{SL}$, completing the proof. The following corollary is immediate from the above theorem. $\mathbf M = \{\mathcal{SL}\}$. Thus, there are 47 Bol-Moufang subvarieties each of which is equal to $\mathcal{SL}$; and hence they are equal to each other. In order to be able to compare the remaining (possibly distinct) subvarieties with each other, the following lemmas will be useful. \[properties\_A23\] Let $\mathbf A \in \mathcal A_{23}$. Then $\mathbf A $ satisfies the identities: 1. $0 \to x \approx x$, \[310516\_03\] 2. $(x \to x) \to y \approx x \to ((x \to 0') \to y)$, \[310516\_05\] 3. $(x \to x) \to y \approx x \to (x \to y')'$. \[310516\_08\] <!-- --> (a) Let $a \in A$. Then $$\begin{array}{lcll} a & = & 0' \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & (0 \to 0) \to a & \mbox{} \\ & = & (0 \to 0) \to a'' & \mbox{by (\ref{eq_I20})} \\ & = & (0 \to 0) \to (a' \to 0) & \mbox{} \\ & = & 0 \to (0 \to a')' & \mbox{by ($A_{2 3}$)} \\ & = & 0 \to a'' & \mbox{by Lemma \ref{general_properties3} (\ref{031114_07})} \\ & = & 0 \to a & \mbox{by (\ref{eq_I20})}. \end{array}$$ (b) Let $a,b \in A$. Then, using ($A_{2 3}$) and Lemma \[general\_properties\_equiv\] (\[TXX\]), we have that $a \to ((a \to 0') \to b) = (a \to a) \to (0' \to b) = (a \to a) \to b$. (c) Let $a,b \in A$. By ($A_{2 3}$) we have that $(a \to a) \to b = (a \to a) \to b'' = (a \to a) \to (b' \to 0) = a \to (a \to b')'$. \[properties\_A25\] \[properties\_C25\] \[properties\_D25\] \[properties\_E25\] We have 1. Let $\mathbf A \in \mathcal A_{25} \cup \mathcal C_{25} \cup \mathcal D_{25} \cup \mathcal E_{25}$. Then $\mathbf A $ satisfies the identities 1. $0 \to x \approx x$, \[060616\_01\] \[070616\_03\] \[070616\_05\] \[070616\_07\] 2. $(x \to y)' \approx x' \to y'$. \[060616\_02\] \[070616\_04\] \[070616\_06\] \[070616\_08\] 2. Let $\mathbf A \in \mathcal A_{25}$. Then $\mathbf A \models x \to (y \to (y' \to z)) \approx y \to ((y \to x) \to z)$. \[060616\_03\] <!-- --> 1. (a) Let $\mathbf A \in \mathcal A_{25}$ and $a \in A$. Then $$\begin{array}{lcll} a & = & a'' & \mbox{by (\ref{eq_I20})} \\ & = & a' \to 0 & \mbox{} \\ & = & (0' \to a') \to 0 & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & ((0 \to 0) \to a') \to 0 & \mbox{} \\ & = & 0 \to ((0 \to a') \to 0) & \mbox{by ($A_{2 5}$)} \\ & = & 0 \to a'' & \mbox{by Lemma \ref{general_properties3} (\ref{031114_07})} \\ & = & 0 \to a & \mbox{by (\ref{eq_I20})}. \end{array}$$ Let $\mathbf A \in \mathcal C_{25}$ and $a \in A$. Then $$\begin{array}{lcll} 0 \to a & = & 0 \to (0' \to a) & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & 0 \to ((0' \to 0') \to a) & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & ((0 \to 0') \to 0') \to a & \mbox{by ($C_{2 5}$)} \\ & = & ((0'' \to 0') \to 0') \to a & \mbox{by $0 \approx 0''$} \\ & = & (0' \to 0') \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})} \\ & = & 0' \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX}).} \end{array}$$ Let $\mathbf A \in \mathcal D_{25}$ and $a \in A$. Then $$\begin{array}{lcll} 0 \to a & = & 0 \to a'' & \mbox{by (\ref{eq_I20})} \\ & = & 0 \to (0 \to a')' & \mbox{by Lemma \ref{general_properties3} (\ref{031114_07})} \\ & = & 0 \to ((0 \to a') \to 0) & \mbox{} \\ & = & ((0 \to 0) \to a') \to 0 & \mbox{by ($D_{2 5}$)} \\ & = & (0' \to a') \to 0 & \mbox{} \\ & = & a' \to 0 & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & a & \mbox{by (\ref{eq_I20})}. \end{array}$$ If $\mathbf A \in \mathcal E_{25}$, then the proof is analogous to that of the preceding case. Just replace ($D_{2 5}$) with ($E_{2 5}$). (b) By (\[060616\_01\]), $\mathbf A \models x \approx 0 \to x$. Then by Lemma \[lemma\_070616\_01\], we have $$\mathbf A \models (x \to y)' \approx x' \to y'.$$ 2. Let $a,b,c \in A$. Then $$\begin{array}{lcll} a \to (b \to (b' \to c)) & = & a \to ((b \to b)' \to c) & \mbox{by ($A_{2 5}$)} \\ & = & a \to (c' \to (b \to b)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & a \to (b \to (c' \to b)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & b \to (a \to (c' \to b)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & b \to (c' \to (a \to b)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & b \to ((a \to b)' \to c) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & b \to ((a' \to b') \to c) & \mbox{by (\ref{060616_02})} \\ & = & b \to ((b \to a) \to c) & \mbox{ by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}. \end{array}$$ This completes the proof. \[properties\_A12\] Let $\mathbf A \in \mathcal A_{12} \cup \mathcal D_{12} \cup \mathcal D_{35}$ then $\mathbf A $ satisfies the identities 1. $0 \to x' \approx x \to x \approx 0 \to x$, \[140616\_01\] \[140616\_02\] \[140616\_03\] 2. $0 \to (x \to y) \approx 0 \to (y \to x)$, \[140616\_04\] 3. $0 \to (x \to (y \to z)) \approx 0 \to ((x \to y) \to z)$. \[230616\_03\] Let $a, b, c \in A$. (a) Suppose $\mathbf A \in \mathcal A_{12}$. Then $$\begin{array}{lcll} 0 \to a' & = & a \to 0' & \mbox{by Lemma \ref{general_properties} (\ref{cuasiConmutativeOfImplic})} \\ & = & a \to (a \to 0') & \mbox{by Lemma \ref{general_properties2} (\ref{031114_04})} \\ & = & a \to (a \to (0 \to 0)) & \mbox{} \\ & = & a \to ((a \to 0) \to 0) & \mbox{by ($A_{1 2}$)} \\ & = & a \to a'' & \mbox{} \\ & = & a \to a & \mbox{by (\ref{eq_I20})}. \end{array}$$ Thus, we have $$\label{230616_01} \mathbf A \models 0 \to x' \approx x \to x.$$ Hence, $$\begin{array}{lcll} 0 \to a & = & 0 \to a'' & \mbox{by (\ref{eq_I20})} \\ & = & a' \to a' & \mbox{by (\ref{230616_01})} \\ & = & a \to a & \mbox{ by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}. \end{array}$$ Consequently, $$\mathbf A \models 0 \to x \approx x \to x.$$ Next, assume that $\mathbf A \in \mathcal D_{12}$. Then $$\begin{array}{lcll} a \to a & = & a \to (0' \to a) & \mbox{by Lemma \ref{general_properties_equiv} (\ref{TXX})} \\ & = & a \to ((0 \to 0) \to a) & \mbox{} \\ & = & a \to (0 \to (0 \to a)) & \mbox{by ($D_{1 2}$)} \\ & = & 0 \to (0 \to (a \to a)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01}) twice} \\ & = & 0 \to (a \to a) & \mbox{by Lemma \ref{general_properties2} (\ref{031114_04})} \\ & = & 0 \to (a'' \to a'') & \mbox{by (\ref{eq_I20})} \\ & = & 0 \to (a' \to a')' & \mbox{by Lemma \ref{general_properties2} (\ref{191114_05})} \\ & = & 0 \to ((a' \to a') \to 0) & \mbox{} \\ & = & 0 \to (a' \to (a' \to 0)) & \mbox{by ($D_{1 2}$)} \\ & = & 0 \to (a' \to a) & \mbox{by (\ref{eq_I20})} \\ & = & 0 \to a & \mbox{by Lemma \ref{general_properties_equiv} (\ref{LeftImplicationwithtilde})}. \end{array}$$ Hence $$\label{230616_02} \mathbf A \models 0 \to x \approx x \to x.$$ Now, $$\begin{array}{lcll} 0 \to a' & = & a' \to a' & \mbox{by (\ref{230616_02})} \\ & = & a \to a & \mbox{ by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}. \end{array}$$ Consequently, $$\mathbf A \models 0 \to x' \approx x \to x.$$ Finally, assume that $\mathbf A \in \mathcal D_{35}$. Then $$\begin{array}{lcll} 0 \to a & = & a' \to (0 \to a) & \mbox{by Lemma \ref{general_properties2} (\ref{281114_01})} \\ & = & (a \to 0) \to (0 \to a) & \mbox{} \\ & = & ((a \to 0) \to 0) \to a & \mbox{by ($D_{3 5}$)} \\ & = & a'' \to a & \mbox{} \\ & = & a \to a & \mbox{by (\ref{eq_I20})}. \end{array}$$ Hence $$\label{230616_05} \mathbf A \models 0 \to x \approx x \to x.$$ $$\begin{array}{lcll} 0 \to a' & = & a' \to a' & \mbox{by (\ref{230616_05})} \\ & = & a \to a & \mbox{ by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}. \end{array}$$ Consequently, $$\mathbf A \models 0 \to x' \approx x \to x.$$ (b) Observe that $$\begin{array}{lcll} 0 \to (a \to b) & = & 0 \to (b' \to a') & \mbox{ by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & (0 \to b') \to (0 \to a') & \mbox{by Lemma \ref{general_properties2} (\ref{071114_04}) and (\ref{311014_06})} \\ & = & (0 \to b) \to (0 \to a) & \mbox{by (\ref{140616_03})} \\ & = & 0 \to (b \to a) & \mbox{by Lemma \ref{general_properties2} (\ref{071114_04}) and (\ref{311014_06})}. \end{array}$$ (c) $$\begin{array}{lcll} 0 \to (b \to (c \to a)) & = & (0 \to b) \to (0 \to (c \to a)) & \\ & & \mbox{by Lemma \ref{general_properties2} (\ref{071114_04}) and (\ref{311014_06})} & \\ & = & (0 \to b) \to (0 \to (a \to c)) & \mbox{by (\ref{140616_04})} \\ & = & 0 \to (b \to (a \to c)) & \\ & & \mbox{by Lemma \ref{general_properties2} (\ref{071114_04}) and (\ref{311014_06})} & \\ & = & 0 \to (a \to (b \to c)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & 0 \to ((b \to c) \to a) & \mbox{by (\ref{140616_04})}. \end{array}$$ This completes the proof. Distinct Varieties of Symmetric $\mathcal{I}$-zroupoids of Bol-Moufang type =========================================================================== Recall that 47 of the 60 subvarieties of $\mathcal{S}$ were shown to be equal to the variety $\mathcal{SL}$. In this section we will investigate the relationships among the remaining 13 varieties: $\mathcal A_{12}, \mathcal A_{23}, \mathcal A_{25}, \mathcal A_{35}, \mathcal B_{13}, \mathcal B_{25}, \mathcal C_{25}, \mathcal D_{12},$ $ \mathcal D_{25}, \mathcal D_{35}, \mathcal E_{25}, \mathcal F_{13}$ and $\mathcal F_{25} $. We still need to determine which of these are distinct from each other. The following theorem throws more light on this issue. \[theorem\_040716\_05\] We have 1. $\mathcal A_{23} = \mathcal A_{25} = \mathcal C_{25} = \mathcal D_{25} = \mathcal E_{25}$, 2. $\mathcal A_{12} = \mathcal B_{13} = \mathcal D_{12} = \mathcal D_{35} = \mathcal F_{13}$, 3. $\mathcal A_{35} = \mathcal F_{25}$, \[040716\_06\] 4. $\mathcal B_{25} \ = \ \mathcal{S}$. <!-- --> (a) Let $\mathbf A \in \mathcal{A}_{23}$ and $a,b,c \in A$. We have that $$\begin{array}{lcll} c' \to (a \to (b \to a)) & = & a \to (c' \to (b \to a)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & a \to (b \to (c' \to a)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & a \to (b \to (a' \to c)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & a \to (a' \to (b \to c)). & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})}. \end{array}$$ Hence $\mathbf A$ satisfies the identity $$\label{310516_04} z' \to (x \to (y \to x)) \approx x \to (x' \to (y \to z)).$$ Observe $$\begin{array}{lcll} (a \to (a \to b')')' & = & ((a \to b') \to a')' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_02})} \\ & = & ((a'' \to a) \to (b' \to a')')'' & \mbox{by (I)} \\ & = & (a \to a) \to (b' \to a')' & \mbox{by (\ref{eq_I20})} \\ & = & (a \to a) \to ((b \to 0) \to a')' & \mbox{} \\ & = & (a \to a) \to ((a'' \to b) \to (0 \to a')')'' & \mbox{by (I)} \\ & = & (a \to a) \to ((a \to b) \to (0 \to a')') & \mbox{by (\ref{eq_I20})} \\ & = & (a \to a) \to ((a \to b) \to a'') & \mbox{by Lemma \ref{properties_A23} (\ref{310516_03})} \\ & = & (a \to a) \to ((a \to b) \to a) & \mbox{by (\ref{eq_I20})} \\ & = & (a \to a) \to ((0 \to b) \to a) & \mbox{by Lemma \ref{general_properties2} (\ref{291014_10})} \\ & = & (a \to a) \to (b \to a) & \mbox{by Lemma \ref{properties_A23} (\ref{310516_03})} \\ & = & a \to ((a \to b) \to a) & \mbox{by ($A_{2 3}$)} \\ & = & a \to ((0 \to b) \to a) & \mbox{by Lemma \ref{general_properties2} (\ref{291014_10})} \\ & = & a \to (b \to a) & \mbox{by Lemma \ref{properties_A23} (\ref{310516_03})}. \end{array}$$ Hence, using (\[310516\_04\]), we have that $\mathbf A$ satisfies $$z' \to (x \to (x \to y')')' \approx x \to (x' \to (y \to z)).$$ Therefore, by Lemma \[properties\_A23\] (\[310516\_03\]), $$\label{310516_06} \mathbf A \models z' \to (x \to (x \to y')')' \approx x \to ((0 \to x') \to (y \to z)).$$ From $$\begin{array}{lcll} a \to ((0 \to a') \to (b \to c)) & = & a \to ((a \to 0') \to (b \to c)) & \mbox{by Lemma \ref{general_properties} (\ref{cuasiConmutativeOfImplic})} \\ & = & (a \to a) \to (b \to c) & \mbox{by Lemma \ref{properties_A23} (\ref{310516_05})} \\ & = & a \to ((a \to b) \to c) & \mbox{by ($A_{2 3}$)}, \\ \end{array}$$ and the equation (\[310516\_06\]), we obtain $$\label{310516_07} \mathbf A \models z' \to (x \to (x \to y')')' \approx x \to ((x \to y) \to z).$$ Finally, $$\begin{array}{lcll} a \to ((a \to b) \to c)& = & c' \to (a \to (a \to b')')' & \mbox{by (\ref{310516_07})} \\ & = & c' \to ((a \to a) \to b)' & \mbox{by Lemma \ref{properties_A23} (\ref{310516_08})} \\ & = & ((a \to a) \to b) \to c & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}, \end{array}$$ proving that the identity ($A_{2 5}$) holds in $\mathbf A$. Therefore, we have that $$\label{070616_09} \mathcal{A}_{23} \subseteq \mathcal{A}_{25}.$$ Let $\mathbf A \in \mathcal{A}_{25}$ and $a,b,c \in A$. Then $$\begin{array}{llll} ((a \to b) \to b) \to c & = (((a \to b) \to b) \to c)'' & \mbox{by (\ref{eq_I20})} \\ & = (c' \to ((a \to b) \to b)')'' & \mbox{ by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = (c' \to (b' \to (a \to b)')')'' & \mbox{{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}} \\ & = (c' \to (b \to (a \to b)))'' & \mbox{by Lemma \ref{properties_A25} (\ref{060616_02})} \\ & = (c'' \to (b \to (a \to b))')' & \mbox{by Lemma \ref{properties_A25} (\ref{060616_02})} \\ & = (c \to (b \to (a \to b))')' & \mbox{by (\ref{eq_I20})} \\ & = (c \to (b \to (b' \to a'))')' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = (c \to (b' \to (b' \to a')'))' & \mbox{by Lemma \ref{properties_A25} (\ref{060616_02})} \\ & = (c \to (b' \to (b \to a)))' & \mbox{by Lemma \ref{properties_A25} (\ref{060616_02})} \\ & = (c \to (b \to (b' \to a)))' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = (b \to ((b \to c) \to a))' & \mbox{by Lemma \ref{properties_A25} (\ref{060616_03})} \\ & = (((b \to b) \to c) \to a)' & \mbox{by ($A_{2 5}$)} \\ & = (a' \to ((b \to b) \to c)')' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = a \to ((b \to b) \to c) & \mbox{by Lemma \ref{properties_A25} (\ref{060616_02})}. \end{array}$$ Therefore, we have that $$\label{070616_10} \mathcal{A}_{25} \subseteq \mathcal{C}_{25}.$$ Let $\mathbf A \in \mathcal{C}_{25}$ and $a,b,c \in A$. We have that $$\begin{array}{lcll} ((a \to b) \to c) \to a & = & ((a \to b) \to c)'' \to a & \mbox{by (\ref{eq_I20})} \\ & = & ((a \to b)' \to c')' \to a & \mbox{by Lemma \ref{properties_C25} (\ref{070616_04})} \\ & = & ((a' \to b') \to c')' \to a & \mbox{by Lemma \ref{properties_C25} (\ref{070616_04})} \\ & = & a' \to ((a' \to b') \to c') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & a' \to (c \to (a' \to b')') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_02})} \\ & = & c \to (a' \to (a' \to b')') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & c \to (a' \to (a \to b)) & \mbox{by Lemma \ref{properties_C25} (\ref{070616_04})}. \\ & = & c \to (a' \to (a'' \to b)) & \mbox{by (\ref{eq_I20}) }\\ & = & c \to (a' \to (b' \to a')) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})}\\ & = & c \to (b' \to (a' \to a')) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & c \to ((a' \to a')' \to b) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & c \to ((a \to a) \to b) & \mbox{by Lemma \ref{properties_C25} (\ref{070616_04})} \\ & = & ((c \to a) \to a) \to b & \mbox{by ($C_{2 5}$)} \\ & = & b' \to ((c \to a) \to a)' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & b' \to ((c \to a)' \to a') & \mbox{by Lemma \ref{properties_C25} (\ref{070616_04})} \\ & = & b' \to (a \to (c \to a)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & b' \to (c \to (a \to a)) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & b' \to ((a \to a)' \to c') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & (a \to a)' \to (b' \to c') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & (b' \to c')' \to (a \to a) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & (b \to c) \to (a \to a) & \mbox{by Lemma \ref{properties_C25} (\ref{070616_04})} \\ & = & a \to ((b \to c) \to a) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})}. \end{array}$$ Thus, $$\label{070616_11} \mathcal{C}_{25} \subseteq \mathcal{D}_{25}.$$ Let $\mathbf A \in \mathcal{D}_{25}$ and $a,b,c \in A$. Then $$\begin{array}{lcll} ((a \to b) \to c) \to b & = & b' \to ((a \to b) \to c)' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & b' \to (c' \to (a \to b)')' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & b' \to (c' \to (a' \to b'))' & \mbox{by Lemma \ref{properties_D25} (\ref{070616_06})} \\ & = & b' \to (c \to (a' \to b')') & \mbox{by Lemma \ref{properties_D25} (\ref{070616_06})} \\ & = & b' \to (c \to (a \to b)) & \mbox{by Lemma \ref{properties_D25} (\ref{070616_06})} \\ & = & b' \to (c \to (a'' \to b)) & \mbox{by (\ref{eq_I20}) }\\ & = & b' \to (c \to (b' \to a')) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & b' \to (b' \to (c \to a')) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & b' \to (c \to a') & \mbox{by Lemma \ref{general_properties2} (\ref{031114_04})} \\ & = & b' \to (a \to c') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_02})} \\ & = & a \to (b' \to c') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & a \to (b \to c)' & \mbox{by Lemma \ref{properties_D25} (\ref{070616_06})} \\ & = & (b \to c) \to a' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_02})} \\ & = & (b \to (b \to c)) \to a' & \mbox{by Lemma \ref{general_properties2} (\ref{031114_04})} \\ & = & ((b \to c)' \to b') \to a' & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & ((b \to c) \to b)' \to a' & \mbox{by Lemma \ref{properties_D25} (\ref{070616_06})} \\ & = & a \to ((b \to c) \to b) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})}. \end{array}$$ Consequently, $$\label{070616_12} \mathcal{D}_{25} \subseteq \mathcal{E}_{25}.$$ Let $\mathbf A \in \mathcal{E}_{25}$ and $a,b,c \in A$. Then $$\begin{array}{lcll} (a \to a) \to (b \to c) & = & b \to ((a \to a) \to c) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})} \\ & = & b \to (c' \to (a \to a)') & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{021017_01})} \\ & = & b \to (c' \to (a' \to a')) & \mbox{by Lemma \ref{properties_E25} (\ref{070616_08})} \\ & = & b \to (a' \to (c' \to a')) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_01})}. \\ & = & b \to ((c' \to a')' \to a) & \mbox{by Lemma \ref{properties_of_I20_MC} (\ref{310516_02})} \\ & = & b \to ((c \to a) \to a) & \mbox{by Lemma \ref{properties_E25} (\ref{070616_08})} \\ & =
{'source': 'arXiv_out/1710'}