# An Algebra of Properties of Binary Relations

Jochen Burghardt

► To cite this version:

Jochen Burghardt. An Algebra of Properties of Binary Relations. [Technical Report] FIRST - Forschungsinstitut für Rechnerarchitektur und Softwaretechnik. 2020. [hal-03138023]

HAL Id: hal-03138023

https://hal.science/hal-03138023

Submitted on 10 Feb 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An Algebra of Properties of Binary Relations

Jochen Burghardt

jochen.burghardt@alumni.tu-berlin.de

Feb 2021

## Abstract

We consider all 16 unary operations that, given a homogeneous binary relation $R$, define a new one by a boolean combination of $xRy$ and $yRx$. Operations can be composed, and connected by pointwise-defined logical junctors. We consider the usual properties of relations, and allow them to be lifted by prepending an operation.

We investigate extensional equality between lifted properties (e.g. *a relation is connex iff its complement is asymmetric*), and give a table to decide this equality. Supported by a counter-example generator and a resolution theorem prover, we investigate all 3-atom implications between lifted properties, and give a sound and complete axiom set for them (containing e.g. “if $R$'s complement is left Euclidean and $R$ is right serial, then $R$'s symmetric kernel is left serial”).

*Keywords: Binary relation; Boolean algebra; Hypotheses generation*

## Contents

<table><tr><td>1</td><td>Introduction</td><td>3</td></tr><tr><td>2</td><td>Definitions</td><td>5</td></tr><tr><td>3</td><td>An algebra of unary operations on relations</td><td>9</td></tr><tr><td>4</td><td>Equivalent lifted properties</td><td>17</td></tr><tr><td>4.1</td><td>Proof of equivalence classes</td><td>21</td></tr><tr><td>5</td><td>Implications between lifted properties</td><td>28</td></tr><tr><td>5.1</td><td>Referencing an implication</td><td>28</td></tr><tr><td>5.2</td><td>Trivial inferences</td><td>29</td></tr><tr><td>5.3</td><td>Finding implications</td><td>30</td></tr><tr><td>5.4</td><td>Finite counter-examples</td><td>31</td></tr><tr><td>5.5</td><td>Infinite counter-examples</td><td>36</td></tr><tr><td>5.6</td><td>Reported laws</td><td>40</td></tr><tr><td>5.7</td><td>Axiom set</td><td>49</td></tr><tr><td>5.8</td><td>Some proofs of axioms</td><td>51</td></tr><tr><td>6</td><td>References</td><td>60</td></tr></table>
List of Figures

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>Encoding of unary operations</td>
      <td>9</td>
    </tr>
    <tr>
      <td>2</td>
      <td>Semantics of unary operations</td>
      <td>10</td>
    </tr>
    <tr>
      <td>3</td>
      <td>Composition computation example for q = 5</td>
      <td>11</td>
    </tr>
    <tr>
      <td>4</td>
      <td>Composition of unary operations (p ◦ q =?)</td>
      <td>11</td>
    </tr>
    <tr>
      <td>5</td>
      <td>Left inverses w.r.t. composition (? ◦ q = p)</td>
      <td>12</td>
    </tr>
    <tr>
      <td>6</td>
      <td>Right inverses w.r.t. composition (p ◦? = q)</td>
      <td>13</td>
    </tr>
    <tr>
      <td>7</td>
      <td>Partition split algorithm</td>
      <td>17</td>
    </tr>
    <tr>
      <td>8</td>
      <td>Redundant properties.</td>
      <td>18</td>
    </tr>
    <tr>
      <td>9</td>
      <td>Computed partitions of lifted properties</td>
      <td>19</td>
    </tr>
    <tr>
      <td>10</td>
      <td>Default representations of lifted properties</td>
      <td>20</td>
    </tr>
    <tr>
      <td>11</td>
      <td>Approach to find implications</td>
      <td>30</td>
    </tr>
    <tr>
      <td>12</td>
      <td>Counter-example relation for aiir and qij0</td>
      <td>33</td>
    </tr>
    <tr>
      <td>13</td>
      <td>Counter-example relation for eiit</td>
      <td>33</td>
    </tr>
    <tr>
      <td>14</td>
      <td>Counter-example relation for g0ih</td>
      <td>34</td>
    </tr>
    <tr>
      <td>15</td>
      <td>Counter-example relation for qbvk</td>
      <td>34</td>
    </tr>
    <tr>
      <td>16</td>
      <td>Counter-example relation for qiiu, r0jq, and reuu</td>
      <td>34</td>
    </tr>
    <tr>
      <td>17</td>
      <td>Counter-example relation for qism</td>
      <td>34</td>
    </tr>
    <tr>
      <td>18</td>
      <td>Counter-example relation for qisr</td>
      <td>35</td>
    </tr>
    <tr>
      <td>19</td>
      <td>Counter-example relation for rg0u and rgak</td>
      <td>35</td>
    </tr>
    <tr>
      <td>20</td>
      <td>Counter-example relation for rylq and rymo</td>
      <td>35</td>
    </tr>
    <tr>
      <td>21</td>
      <td>Counter-example relation for xrkv</td>
      <td>35</td>
    </tr>
    <tr>
      <td>22</td>
      <td>Relation in Exm. 34</td>
      <td>37</td>
    </tr>
    <tr>
      <td>23</td>
      <td>Relation in Exm. 35</td>
      <td>38</td>
    </tr>
    <tr>
      <td>24</td>
      <td>Relation in Exm. 36</td>
      <td>38</td>
    </tr>
    <tr>
      <td>25</td>
      <td>Relation in Exm. 37</td>
      <td>39</td>
    </tr>
    <tr>
      <td>26</td>
      <td>Relation in Exm. 39</td>
      <td>39</td>
    </tr>
    <tr>
      <td>27</td>
      <td>Relation in Exm. 40</td>
      <td>40</td>
    </tr>
    <tr>
      <td>28</td>
      <td>Implications about anti-symmetry (an)</td>
      <td>41</td>
    </tr>
    <tr>
      <td>29</td>
      <td>Implications about anti-transitivity (at)</td>
      <td>42</td>
    </tr>
    <tr>
      <td>30</td>
      <td>Implications about density (de)</td>
      <td>42</td>
    </tr>
    <tr>
      <td>31</td>
      <td>Implications about left Euclideanness (le)</td>
      <td>43</td>
    </tr>
    <tr>
      <td>32</td>
      <td>Implications about left quasi-reflexivity (lq)</td>
      <td>43</td>
    </tr>
    <tr>
      <td>33</td>
      <td>Implications about left seriality (ls)</td>
      <td>44</td>
    </tr>
    <tr>
      <td>34</td>
      <td>Implications about left uniqueness (lu)</td>
      <td>44</td>
    </tr>
    <tr>
      <td>35</td>
      <td>Implications about semi-order property 1 (s1)</td>
      <td>45</td>
    </tr>
    <tr>
      <td>36</td>
      <td>Implications about semi-order property 2 (s2)</td>
      <td>45</td>
    </tr>
    <tr>
      <td>37</td>
      <td>Implications about transitivity (tr)</td>
      <td>46</td>
    </tr>
    <tr>
      <td>38</td>
      <td>Implications about symmetry (sy), asymmetry (as), and reflexivity (rf)</td>
      <td>46</td>
    </tr>
    <tr>
      <td>39</td>
      <td>Implications about basic properties</td>
      <td>47</td>
    </tr>
    <tr>
      <td>40</td>
      <td>Inconsistencies between lifted properties</td>
      <td>48</td>
    </tr>
    <tr>
      <td>41</td>
      <td>Proof sketch in Lem. 42 (lf) Order-based axiom set computation (rg)</td>
      <td>49</td>
    </tr>
    <tr>
      <td>42</td>
      <td>Minimal axiom set</td>
      <td>52</td>
    </tr>
    <tr>
      <td>43</td>
      <td>Proof tree of "Trans ∧ Irref → ASym"</td>
      <td>53</td>
    </tr>
    <tr>
      <td>44</td>
      <td>Disproof tree of "ASym ∧ Trans ≠ Refl"</td>
      <td>53</td>
    </tr>
  </tbody>
</table>
# 1. Introduction

We strive to compute new laws about homogeneous binary relations. In [1], we considered the 24 “best-known” basic properties of relations, and used a counter-example search combined with the Quine-McCluskey algorithm and followed by a manual confirmation / disconfirmation process, to obtain a complete list of laws of the form

$$ \forall R. \text{prop}_1(R) \lor \dots \lor \text{prop}_n(R), $$

where $prop_i$ are negated or unnegated properties, and $R$ ranges over all relations. A classical example of such a law is “each irreflexive and transitive relation is asymmetric”; a lesser known example is “a left unique and right serial relation (on a domain of $\ge 5$ elements) cannot be incomparability-transitive”. Once such a law has been stated it is usually easy to prove.

We also briefly sketched in [1, p.6-7] a more general approach based on regular tree grammars which could obtain laws involving arbitrary operators on relations (union, closures, ...); however, this approach would require infeasible large computation time and memory.

In the current report, we investigate an intermediate approach which allows one to detect laws involving certain unary operations on relations. The considered set of operations can be motivated by the definition of quasi-transitivity: a relation $R$ is quasi-transitive iff $op_2(R)$ is transitive, where the relation $op_2(R)$ is defined as

$$ x \text{ op}_2(R) y \quad \text{iff} \quad x R y \text{ and not } y R x. $$

Slightly more general, we will allow all unary operations that can be defined by a boolean combination of $xRy$ and $yRx$. Since there are only 16 such operations, generating law suggestions will be still feasible. This allows one to search for laws of the form

$$ \forall R. \text{prop}_1(\text{op}_{11} \circ \dots \circ \text{op}_{1m_1}(R)) \lor \dots \lor \text{prop}_n(\text{op}_{n1} \circ \dots \circ \text{op}_{nm_n}(R)), $$

An example law is “the symmetric closure of a left-serial and transitive relation is always dense”; once it is stated, it is straight forward to prove (Lem. 49.6).

Our set of unary operations is closed w.r.t. composition (“$\circ$”, Def. 8), therefore it is sufficient to look for laws of the form

$$ \forall R. \text{prop}_1(\text{op}_1(R)) \lor \dots \lor \text{prop}_n(\text{op}_n(R)). $$

We define a “lifted property” to be the composition of a basic property and a unary operation, that is, an expression of the form $\lambda R. \text{prop}(\text{op}(R))$ in Lambda-calculus notation. Considering all $24 \cdot 16 = 384$ possible combinations of basic properties (Def. 1) and unary operations (Def. 6), it turns out that many combinations are extensionally equal, and there are only 81 different ones (Thm. 22).

Found laws may now involve e.g. the converse, the complement, the symmetric closure, and the symmetric kernel of a relation.<fnref n="1" /> Moreover, some basic properties are rendered

<footnote n="1">¹ Note that we can’t express e.g. reflexive closure, since our unary operations aren’t concerned with information about $xRx$. To achieve this, our approach could be extended to all 65536 boolean combinations of $xRy$, $yRx$, $xRx$, and $yRy$; however, this is likely to be beyond feasibility again.</footnote>
redundant, as they can be expressed by lifting other properties (Lem. 14). For example, a relation is empty and co-reflexive iff its symmetric closure is asymmetric and anti-symmetric, respectively.

While the basic properties were obtained from mathematical applications (order, equivalence, ...; cf. Def. 2) developed over the years, and therefore pretty much ad hoc, considering all 81 lifted properties is slightly more systematic; the latter are closed w.r.t. our unary operations, while the former are not. A completely systematic approach would consider each property definable by a predicate logic formula with a given number of quantifiers, rather than just the 24 of them shown in Def. 1; however, such an approach is, again, computationally infeasible. So, the unary-operations approach presented here is a good compromise; we will demonstrate in this report that it is in fact feasible.

In Sect. 2, we give some basic definitions prior to the formal introduction of our unary-operation approach in Sect. 3. In Sect. 4, we compute the 81 equivalence classes (w.r.t. extensional equality) of lifted properties. We also define a default representative of each class. While the Quine-McCluskey approach from [1] is still infeasible for 81 different lifted properties, we investigate, in Sect. 5, all laws of the form

$$ \forall R. lprop_1(R) \wedge lprop_2(R) \rightarrow lprop_3(R), $$

where $lprop_i$ are (unnegated) lifted properties. Using an approach different from Quine-McCluskey to eliminate redundant laws, we isolate in Sect. 5.7 a total of 124 “axioms” which imply all found laws (Thm. 56). Our C source code is provided in the ancillary files.
## 2. Definitions

In this section, we give some preparatory definitions. Definition 1 defines the “basic” properties we consider throughout this report. Definition 2 indicates their historical origins, and at the same time names some applications for them. Definition 3 introduces some operators on relations; each of them will later be identified with an admitted unary operation (Lem. 12). Definition 4 defines the notion of monotonic and antitonic properties; Lem. 5 classifies our basic properties by these categories.

**Definition 1.** (*Binary relation properties*) Let $X$ be a set. A (homogeneous) binary relation $R$ on $X$ is a subset of $X \times X$. The relation $R$ is called

1. reflexive (“Refl”, “rf”) if $\forall x \in X. xRx$;

2. irreflexive (“Irrefl”, “ir”) if $\forall x \in X. \neg xRx$;

3. co-reflexive (“CoRefl”, “cr”) if $\forall x, y \in X. xRy \to x = y$;

4. left quasi-reflexive (“lq”) if $\forall x, y \in X. xRy \to xRx$;

5. right quasi-reflexive (“rq”) if $\forall x, y \in X. xRy \to yRy$;

6. quasi-reflexive (“QuasiRefl”) if it is both left and right quasi-reflexive;

7. symmetric (“Sym”, “sy”) if $\forall x, y \in X. xRy \to yRx$;

8. asymmetric (“ASym”, “as”) if $\forall x, y \in X. xRy \to \neg yRx$;

9. anti-symmetric (“AntiSym”, “an”) if $\forall x, y \in X. xRy \land x \neq y \to \neg yRx$;

10. semi-connex (“SemiConnex”, “sc”) if $\forall x, y \in X. xRy \lor yRx \lor x = y$;

11. connex (“Connex”, “co”) if $\forall x, y \in X. xRy \lor yRx$;

12. transitive (“Trans”, “tr”) if $\forall x, y, z \in X. xRy \land yRz \to xRz$;

13. anti-transitive (“AntiTrans”, “at”) if $\forall x, y, z \in X. xRy \land yRz \to \neg xRz$;

14. quasi-transitive (“QuasiTrans”, “qt”) if
   $\forall x, y, z \in X. xRy \land \neg yRx \land yRz \land \neg zRy \to xRz \land \neg zRx$;

15. right Euclidean (“RgEucl”, “re”) if $\forall x, y, z \in X. xRy \land xRz \to yRz$;

16. left Euclidean (“LfEucl”, “le”) if $\forall x, y, z \in X. yRx \land zRx \to yRz$;

17. semi-order property 1 (“SemiOrd1”, “s1”) if
   $\forall w, x, y, z \in X. wRx \land \neg xRy \land \neg yRx \land yRz \to wRz$;

18. semi-order property 2 (“SemiOrd2”, “s2”) if
   $\forall w, x, y, z \in X. xRy \land yRz \to wRx \lor xRw \lor wRy \lor yRw \lor wRz \lor zRw$.

19. right serial (“RgSerial”, “rs”) if $\forall x \in X \exists y \in X. xRy$

20. left serial (“LfSerial”, “ls”) if $\forall y \in X \exists x \in X. xRy$

21. dense (“Dense”, “de”) if $\forall x, z \in X \exists y \in X. xRz \to xRy \land yRz$.

22. incomparability-transitive (“IncTrans”, “it”) if
   $\forall x, y, z \in X. \neg xRy \land \neg yRx \land \neg yRz \land \neg zRy \to \neg xRz \land \neg zRx$.

23. left unique (“LfUnique”, “lu”) if $\forall x_1, x_2, y \in X. x_1Ry \land x_2Ry \to x_1 = x_2$.

24. right unique (“RgUnique”, “ru”) if $\forall x, y_1, y_2 \in X. xRy_1 \land xRy_2 \to y_1 = y_2$.

The capitalized abbreviations in parentheses are used by our software; the two-letter codes are used in tables and pictures when space is scarce.

We say that $x, y$ are incomparable w.r.t. $R$, if $\neg xRy \land \neg yRx$ holds. $\square$

<figure><img src="image_2.png" /></figure>

**Definition 2.** (*Kinds of binary relations*) A binary relation $R$ on a set $X$ is called
1. an equivalence if it is reflexive, symmetric, and transitive;

2. a partial equivalence if it is symmetric and transitive;

3. a tolerance relation if it is reflexive and symmetric;

4. idempotent if it is dense and transitive;

5. trichotomous if it is irreflexive, asymmetric, and semi-connex;

6. a non-strict partial order if it is reflexive, anti-symmetric, and transitive;

7. a strict partial order if it is irreflexive, asymmetric, and transitive;

8. a semi-order if it is asymmetric and satisfies semi-order properties 1 and 2;

9. a preorder if it is reflexive and transitive;

10. a weak ordering if
it is irreflexive, asymmetric, transitive, and incomparability-transitive;

11. a partial function if it is right unique;

12. a total function if it is right unique and right serial;

13. an injective function if it is left unique, right unique, and right serial;

14. a surjective function if it is right unique and left and right serial;

15. a bijective function if it is left and right unique and left and right serial. ☐

**Definition 3. (Operation names)**

1. The symmetric kernel of a relation $R$ is defined as the largest subset of $R$ that is a symmetric relation.

2. The symmetric closure of a relation $R$ is defined as the smallest superset of $R$ that is a symmetric relation.

3. We define the asymmetric kernel of a relation $R$ as the intersection of all maximal subsets of $R$ that are asymmetric relations.
Note that for an arbitrary relation $R$, a largest subset that is an asymmetric relation need not exist. For example, on the set $X = \{0, 1\}$, the relation $R = \{\langle0, 1\rangle, \langle1, 0\rangle\}$ has three asymmetric subsets, viz. $R_1 = \{\langle0, 1\rangle\}$, $R_2 = \{\langle1, 0\rangle\}$, and $R_3 = \{\}$.
While $R_1$ and $R_2$ are maximal w.r.t. $\subseteq$, none of them is largest.
☐

**Definition 4. (Monotonicity)** A property *prop* of binary relations is called monotonic if ∀*R*₁, *R*₂. *R*₁ ⊆ *R*₂ ∧ *prop*(*R*₁) ⇒ *prop*(*R*₂). It is called antitonic if ∀*R*₁, *R*₂. *R*₁ ⊇ *R*₂ ∧ *prop*(*R*₁) ⇒ *prop*(*R*₂). ☐

**Lemma 5. (Monotonic properties)** We use first-order formulas without constants and function symbols and with equality and one binary relation symbol $R$ to define properties of binary relations, as in Def. 1. Such a formula is called an $\wedge$-$\vee$-formula if it is in prenex normal form, contains no other binary junctors than $(\wedge)$ and $(\vee)$, and contains $(\neg)$ only applied to atoms.

1. A property is monotonic if its definition can be written as a closed $\wedge$-$\vee$-formula without any negated occurrence of $R$.

2. A property is antitonic if its definition can be written as a closed $\wedge$-$\vee$-formula without any unnegated occurrence of $R$.
3. The following basic properties from Def. 1 are monotonic:
   Refl, SemiConnex, Connex, RgSerial, LfSerial.

4. The following basic properties are antitonic:
   Irrefl, Corefl, ASym, AntiSym, AntiTrans, LfUnique, RgUnique.

5. The following basic properties are neither monotonic nor antitonic:
   LfQuasiRefl, RgQuasiRefl, QuasiRefl, Sym, Trans, QuasiTrans, RgEucl, LfEucl, SemiOrd1, SemiOrd2, Dense, IncTrans.

PROOF. 1. Given an $\wedge$-$\vee$-formula $\psi$ in $n$ free variables $x_1, \dots, x_n$ and a relation $R$ on a domain $X$, define $M(R, \psi)$ to be the set of all $n$-tuples in $X^n$ satisfying $\psi$, w.r.t. $R$. For an $\wedge$-$\vee$-formula $\psi$ without quantifiers or negated occurrences of $R$, show by induction on the structure of $\psi$ that $R_1 \subseteq R_2$ implies $M(R_1, \psi) \subseteq M(R_2, \psi)$:

* If $\psi$ has the form $\psi_1 \wedge \psi_2$, then
  $M(R_1, \psi) = M(R_1, \psi_1) \cap M(R_1, \psi_2) \subseteq M(R_2, \psi_1) \cap M(R_2, \psi_2) = M(R_2, \psi)$.

* The case $\psi_1 \vee \psi_2$ is similar, relying on the monotonicity of $\cup$, rather than of $\cap$.

* If $\psi$ has the form $x_i R x_j$, then $M(R_1, \psi) = \{\langle x_1, \dots, x_i, \dots, x_j, \dots, x_n \rangle \mid x_i R_1 x_j\} \subseteq \{\langle x_1, \dots, x_i, \dots, x_j, \dots, x_n \rangle \mid x_i R_2 x_j\} = M(R_2, \psi)$.

* If $\psi$ does not contain $R$, then $M(R_1, \psi) = M(R_2, \psi)$. Note that $\psi$ needn't be an atom in this case.

Finally, show that $M(R_1, \psi) \subseteq M(R_2, \psi)$ implies both $M(R_1, \forall x_n. \psi) \subseteq M(R_2, \forall x_n. \psi)$ and $M(R_1, \exists x_n. \psi) \subseteq M(R_2, \exists x_n. \psi)$. By induction on $n$, this extends to arbitrarily long quantifier prefixes.

2. The proof is similar to 1.

3. For each of the listed properties, its definition in Def. 1 is in the form required by 1.

4. The definition of irreflexivity in Def. 1 is in the form required by 2. For the remaining properties, resolving $(\rightarrow)$ brings it into that form:

* Corefl: $\forall x, y \in X. \neg xRy \lor x = y$

* ASym: $\forall x, y \in X. \neg xRy \lor \neg yRx$

* AntiSym: $\forall x, y \in X. \neg xRy \lor \neg yRx \lor x = y$

* AntiTrans: $\forall x, y, z \in X. \neg xRy \lor \neg yRz \lor \neg xRz$.

* LfUnique: $\forall x_1, x_2, y \in X. \neg x_1Ry \lor \neg x_2Ry \lor x_1 = x_2$.

* RgUnique: $\forall x, y_1, y_2 \in X. \neg xRy_1 \lor \neg xRy_2 \lor x_1 = x_2$.

5. For each property, we give relations $R_1 \subset R_2 \subset R_3$ on the domain $X = \{0, 1, 2, 3\}$ such that $R_2$, but neither $R_1$ nor $R_3$, has the property. $R_1$ consists of all black pairs, $R_2$ consists of all black or green pairs, and $R_3$ consists of all pairs. Intuitively, adding the green pair establishes the property, and adding the red destroys it again. We use semi-colons to indicate the sub-relation separations in grey-scale renderings.

* LfQuasiRefl: $\{\langle 0, 1 \rangle; \langle 0, 0 \rangle; \langle 1, 2 \rangle\}$

* RgQuasiRefl, QuasiRefl: $\{\langle 0, 0 \rangle, \langle 0, 1 \rangle; \langle 1, 1 \rangle; \langle 1, 2 \rangle\}$

* Sym: $\{\langle 0, 1 \rangle; \langle 1, 0 \rangle; \langle 0, 2 \rangle\}$

* Trans, QuasiTrans: $\{\langle 0, 1 \rangle, \langle 1, 2 \rangle; \langle 0, 2 \rangle; \langle 2, 3 \rangle\}$
• RgEucl: {⟨0, 1⟩; ⟨1, 1⟩; ⟨0, 0⟩}

• LfEucl: {⟨0, 1⟩; ⟨0, 0⟩; ⟨1, 0⟩}

• SemiOrd1: {⟨0, 0⟩, ⟨1, 1⟩; ⟨0, 1⟩; ⟨2, 2⟩}

• SemiOrd2: {⟨0, 1⟩, ⟨1, 2⟩; ⟨0, 3⟩; ⟨0, 0⟩}

• Dense: {⟨0, 1⟩; ⟨0, 0⟩; ⟨1, 2⟩}

• IncTrans: {⟨0, 1⟩, ⟨1, 2⟩; ⟨1, 3⟩; ⟨0, 0⟩}

☐
<table><caption>Figure 1: Encoding of unary operations</caption><tr><td>xRy :</td><td>false false true true</td></tr><tr><td>yRx :</td><td>false true false true</td></tr><tr><td>xR<sup>q</sup>y :</td><td>q<sub>8</sub> q<sub>4</sub> q<sub>2</sub> q<sub>1</sub></td></tr></table>

### 3. An algebra of unary operations on relations

In this section, we introduce and investigate our admitted unary operations on relations.

**Definition 6. (Unary operations)** We represent a unary operation on relations as a 4-bit number $p \in \{0, \dots, 9, A, \dots, F\}$, and denote its bits as $p_8, p_4, p_2, p_1$, that is,

$$p = 8 \cdot p_8 + 4 \cdot p_4 + 2 \cdot p_2 + 1 \cdot p_1.$$

Given a binary relation $R$ on a domain set $X$, and $x, y \in X$, we write $R^p$ to denote the application of $p$ to $R$, which we define as

$$\begin{align*}
&R^p \\
\Leftrightarrow & (\neg xRy \land \neg yRx \land p_8) \\
\lor & (\neg xRy \land yRx \land p_4) \\
\lor & (xRy \land \neg yRx \land p_2) \\
\lor & (xRy \land yRx \land p_1)
\end{align*}$$

tacitly identifying 0 with false and 1 with true, see Fig. 1. For example, $xR^1y$ is true iff both $xRy$ and $yRx$ is; moreover, $op_2(R)$ from Sect. 1 can now be written as $R^2$. Figure 2 shows the semantics of each of the 16 possible unary operations.<fnref n="2" /> They allow us to express e.g. the converse, the complement, the symmetric kernel, and the symmetric closure of a relation. For unary operations $p$ and $q$, we define $p \subseteq q$ bitwise as

$$p_8 \leq q_8 \land p_4 \leq q_4 \land p_2 \leq q_2 \land p_1 \leq q_1.$$

Moreover, we extend boolean connectives to unary operations in a bitwise manner, e.g. $\neg p$ is defined as bitwise complement:

$$\begin{align*}
(\neg p) &= 8 \cdot (\neg p_8) + 4 \cdot (\neg p_4) + 2 \cdot (\neg p_2) + 1 \cdot (\neg p_1) \\
&= 8 \cdot (1 - p_8) + 4 \cdot (1 - p_4) + 2 \cdot (1 - p_2) + 1 \cdot (1 - p_1),
\end{align*}$$

similar for the other connectives.

<figure><img src="image_3.png" /></figure>

It may be helpful to think of a unary operation as a set of graph rewriting rules. This view is supported in column “Rewriting” of Fig. 2. Representing a binary relation as a directed graph, two given vertices $x$ and $y$ can be connected by

<footnote n="2">² We use $\oplus$ to denote exclusive or.</footnote>
<table><caption>Figure 2: Semantics of unary operations</caption><thead><tr><th colspan="2">Optn</th><th rowspan="2">Formal</th><th rowspan="2">Rewriting</th><th rowspan="2">Intuitively</th></tr><tr><th>hx</th><th>bin</th></tr></thead><tbody><tr><td>0</td><td>0000</td><td>false</td><td>||| &larr; &rarr;</td><td>empty relation</td></tr><tr><td>1</td><td>0001</td><td>xRy &and; yRx</td><td>|||| &larr; &rarr;</td><td>symmetric kernel</td></tr><tr><td>2</td><td>0010</td><td>xRy &and; &not;yRx</td><td>|||| &larr; &rarr;</td><td>asymmetric kernel</td></tr><tr><td>3</td><td>0011</td><td>xRy</td><td>|||| &larr; &rarr;</td><td>identity</td></tr><tr><td>4</td><td>0100</td><td>&not;xRy &and; yRx</td><td>|||| &rarr; &larr;</td><td>converse asymmetric kernel</td></tr><tr><td>5</td><td>0101</td><td>yRx</td><td>|||| &rarr; &larr;</td><td>converse</td></tr><tr><td>6</td><td>0110</td><td>xRy &oplus; yRx</td><td>|||| &rarr; &rarr;</td><td></td></tr><tr><td>7</td><td>0111</td><td>xRy &or; yRx</td><td>|||| &rarr; &rarr;</td><td>symmetric closure</td></tr><tr><td>8</td><td>1000</td><td>&not;xRy &and; &not;yRx</td><td>&rarr; ||| ||| |||</td><td>incomparable</td></tr><tr><td>9</td><td>1001</td><td>xRy &oplus; &not;yRx</td><td>&rarr; ||| ||| |||</td><td></td></tr><tr><td>A</td><td>1010</td><td>&not;yRx</td><td>&rarr; &larr; &rarr;</td><td>complement of converse</td></tr><tr><td>B</td><td>1011</td><td>xRy &or; &not;yRx</td><td>&rarr; &larr; &rarr;</td><td>complement of converse asymmetric kernel</td></tr><tr><td>C</td><td>1100</td><td>&not;xRy</td><td>&rarr; &rarr; &larr;</td><td>complement</td></tr><tr><td>D</td><td>1101</td><td>&not;xRy &or; yRx</td><td>&rarr; &rarr; &larr;</td><td>complement of asymmetric kernel</td></tr><tr><td>E</td><td>1110</td><td>&not;xRy &or; &not;yRx</td><td>&rarr; &rarr; &rarr;</td><td>complement of symmetric kernel</td></tr><tr><td>F</td><td>1111</td><td>true</td><td>&rarr; &rarr; &rarr;</td><td>universal relation</td></tr></tbody></table>

1. no edge at all (depicted |||),

2. just an edge from $y$ to $x$ (depicted $\leftarrow$),

3. just an edge from $x$ to $y$ (depicted $\rightarrow$), or

4. both an edge from $x$ to $y$ and a reverse edge (depicted $\leftrightarrow$).

For each of the four situations, column “Rewriting” gives the appropriate replacement performed by an operation. For example, operation 7 replaces all $\leftarrow$ and all $\rightarrow$ situations by $\leftrightarrow$, and thus obtains the symmetric closure. Since the column “$\leftarrow$” is just a mirror of “$\rightarrow$”, it is grayed out. Observe that 0 and 1 in the most significant bit in column “bin” corresponds to $||||$ and $\leftrightarrow$, respectively; similar for the least significant bit; for the two middle bits, 00, 01, 10, and 11 correspond to $||||||||$, $\leftarrow \rightarrow$, $\rightarrow \leftarrow$, and $\leftrightarrow \leftrightarrow$, respectively.

**Lemma 7.** (Boolean connectives on operations)

1. $xR^{\neg p}y$ iff $\neg xR^{p}y$

2. $xR^{p}y \land xR^{q}y$ iff $xR^{p \land q}y$

3. Any other boolean connective distributes over operation application in a similar way.

4. If $p \subseteq q$, then $R^p \subseteq R^q$.

**PROOF.** 1,2 We distinguish four cases:

* $xRy \land yRx$:

Then $xR^{\neg p}y$ iff $(\neg p_1) = 1$ iff $p_1 = 0$ iff $\neg xR^{p}y$.

And $xR^{p}y \land xR^{q}y$ iff $(p_1 = 1) \land (q_1 = 1)$ iff $(p_1 \land q_1) = 1$ iff $xR^{p \land q}y$.
<table><caption>Figure 3: Composition computation example for $q = 5$</caption><thead><tr><th>xRy</th><th>yRx</th><th></th><th>xR<sup>q</sup>y</th><th>yR<sup>q</sup>x</th><th></th><th>x(R<sup>q</sup>)<sup>p</sup>y</th></tr></thead><tbody><tr><td>0</td><td>0</td><td>→</td><td>q<sub>8</sub>=0</td><td>q<sub>8</sub>=0</td><td>→</td><td>p<sub>8</sub></td></tr><tr><td>0</td><td>1</td><td>→</td><td>q<sub>4</sub>=1</td><td>q<sub>2</sub>=0</td><td>→</td><td>p<sub>2</sub></td></tr><tr><td>1</td><td>0</td><td>→</td><td>q<sub>2</sub>=0</td><td>q<sub>4</sub>=1</td><td>→</td><td>p<sub>4</sub></td></tr><tr><td>1</td><td>1</td><td>→</td><td>q<sub>1</sub>=1</td><td>q<sub>1</sub>=1</td><td>→</td><td>p<sub>1</sub></td></tr></tbody></table>

<table><caption>Figure 4: Composition of unary operations ($p \circ q = ?$)</caption><thead><tr><th>p\<sup>q</sup></th><th>0</th><th>1</th><th>2</th><th>3</th><th>4</th><th>5</th><th>6</th><th>7</th><th>8</th><th>9</th><th>A</th><th>B</th><th>C</th><th>D</th><th>E</th><th>F</th></tr></thead><tbody><tr><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td></tr><tr><td>1</td><td>0</td><td>1</td><td>0</td><td>1</td><td>0</td><td>1</td><td>6</td><td>7</td><td>8</td><td>9</td><td>8</td><td>9</td><td>8</td><td>9</td><td>E</td><td>F</td></tr><tr><td>2</td><td>0</td><td>0</td><td>2</td><td>2</td><td>4</td><td>4</td><td>0</td><td>0</td><td>0</td><td>0</td><td>2</td><td>2</td><td>4</td><td>4</td><td>0</td><td>0</td></tr><tr><td>3</td><td>0</td><td>1</td><td>2</td><td>3</td><td>4</td><td>5</td><td>6</td><td>7</td><td>8</td><td>9</td><td>A</td><td>B</td><td>C</td><td>D</td><td>E</td><td>F</td></tr><tr><td>4</td><td>0</td><td>0</td><td>4</td><td>4</td><td>2</td><td>2</td><td>0</td><td>0</td><td>0</td><td>0</td><td>4</td><td>4</td><td>2</td><td>2</td><td>0</td><td>0</td></tr><tr><td>5</td><td>0</td><td>1</td><td>4</td><td>5</td><td>2</td><td>3</td><td>6</td><td>7</td><td>8</td><td>9</td><td>C</td><td>D</td><td>A</td><td>B</td><td>E</td><td>F</td></tr><tr><td>6</td><td>0</td><td>0</td><td>6</td><td>6</td><td>6</td><td>6</td><td>0</td><td>0</td><td>0</td><td>0</td><td>6</td><td>6</td><td>6</td><td>6</td><td>0</td><td>0</td></tr><tr><td>7</td><td>0</td><td>1</td><td>6</td><td>7</td><td>6</td><td>7</td><td>6</td><td>7</td><td>8</td><td>9</td><td>E</td><td>F</td><td>E</td><td>F</td><td>E</td><td>F</td></tr><tr><td>8</td><td>F</td><td>E</td><td>9</td><td>8</td><td>9</td><td>8</td><td>9</td><td>8</td><td>7</td><td>6</td><td>1</td><td>0</td><td>1</td><td>0</td><td>1</td><td>0</td></tr><tr><td>9</td><td>F</td><td>F</td><td>9</td><td>9</td><td>9</td><td>9</td><td>F</td><td>F</td><td>F</td><td>F</td><td>9</td><td>9</td><td>9</td><td>9</td><td>F</td><td>F</td></tr><tr><td>A</td><td>F</td><td>E</td><td>B</td><td>A</td><td>D</td><td>C</td><td>9</td><td>8</td><td>7</td><td>6</td><td>3</td><td>2</td><td>5</td><td>4</td><td>1</td><td>0</td></tr><tr><td>B</td><td>F</td><td>F</td><td>B</td><td>B</td><td>D</td><td>D</td><td>F</td><td>F</td><td>F</td><td>F</td><td>B</td><td>B</td><td>D</td><td>D</td><td>D</td><td>F</td></tr><tr><td>C</td><td>F</td><td>E</td><td>D</td><td>C</td><td>B</td><td>A</td><td>9</td><td>8</td><td>7</td><td>6</td><td>5</td><td>4</td><td>3</td><td>2</td><td>1</td><td>0</td></tr><tr><td>D</td><td>F</td><td>F</td><td>D</td><td>D</td><td>B</td><td>B</td><td>F</td><td>F</td><td>F</td><td>F</td><td>D</td><td>D</td><td>B</td><td>B</td><td>F</td><td>F</td></tr><tr><td>E</td><td>F</td><td>E</td><td>F</td><td>E</td><td>F</td><td>E</td><td>9</td><td>8</td><td>7</td><td>6</td><td>7</td><td>6</td><td>7</td><td>6</td><td>1</td><td>0</td></tr><tr><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td></tr></tbody></table>

* $xRy \wedge \neg yRx$:

* $\neg xRy \wedge yRx$:

* $\neg xRy \wedge \neg yRx$: These cases are similar, using $p_2$, $p_4$, and $p_8$ instead of $p_1$.

3. Any other boolean connective $c$ distributes over operation application, since $\neg$ and $\wedge$ do, and $c$ can be obtained as an expression over $\neg$ and $\wedge$; e.g. $xR^{p \vee q}y$ iff $xR^{-(\neg p \wedge \neg q)}y$ iff $\neg(\neg xR^p y \wedge \neg xR^q y)$ iff $xR^p y \vee xR^q y$.

4. Follows from 3: $p \subseteq q$ iff $(p \wedge q) = p$, iff $(R^p \cap R^q) = R^p$ iff $R^p \subseteq R^q$. $\square$

As an example, Sen's construction [2, p.381] of a transitive relation $I$ and a symmetric relation $P$ from a given quasi-transitive relation $R$, such that $R = I \cup P$, cf. [1, Lem.17.3, p.26], can now be paraphrased as $I := R^2$ and $P := R^1$. Using Lem. 7, the proof of disjoint union boils down to two simple computations: $I \cup P = R^2 \cup R^1 = R^3 = R$, and $I \cap P = R^2 \cap R^1 = R^0 = \{\}$. See Lem. 52.1 for another proof using Lem. 7.

**Definition 8. (Operation composition)** We define operation composition in the usual way by $R^{p \circ q} = (R^q)^p$. The set of operations is closed w.r.t. composition; Fig. 3 shows, by way of an example ($q = 5$) how to compute the bit representation of $p \circ q$, given that of $p$ and $q$. $\square$
<table><caption>Figure 5: Left inverses w.r.t. composition $(? \circ q = p)$</caption><thead><tr><th>p</th><th>0</th><th>1</th><th>2</th><th>3</th><th>4</th><th>5</th><th>6</th><th>7</th><th>8</th><th>9</th><th>A</th><th>B</th><th>C</th><th>D</th><th>E</th><th>F</th></tr></thead><tbody><tr><td>0</td><td>0123<br>4567</td><td>0246</td><td>01</td><td>0</td><td>01</td><td>0</td><td>0246</td><td>0246</td><td>0246</td><td>0246</td><td>0</td><td>08</td><td>0</td><td>08</td><td>0246</td><td>0246<br>8ACE</td></tr><tr><td>1</td><td></td><td>1357</td><td></td><td>1</td><td>1</td><td></td><td></td><td></td><td></td><td></td><td>8</td><td>8</td><td></td><td></td><td>8ACE</td><td></td></tr><tr><td>2</td><td></td><td></td><td>23</td><td>2</td><td>45</td><td>4</td><td></td><td></td><td></td><td></td><td>2</td><td>2A</td><td>4</td><td>4C</td><td></td><td></td></tr><tr><td>3</td><td></td><td></td><td></td><td>3</td><td>5</td><td></td><td></td><td></td><td></td><td></td><td>A</td><td>C</td><td></td><td></td><td></td><td></td></tr><tr><td>4</td><td></td><td></td><td>45</td><td>4</td><td>23</td><td>2</td><td></td><td></td><td></td><td></td><td>4</td><td>4C</td><td>2</td><td>2A</td><td></td><td></td></tr><tr><td>5</td><td></td><td></td><td></td><td>5</td><td>3</td><td></td><td></td><td></td><td></td><td></td><td>C</td><td>A</td><td></td><td></td><td></td><td></td></tr><tr><td>6</td><td></td><td></td><td>67</td><td>6</td><td>67</td><td>6</td><td>1357</td><td></td><td></td><td>8ACE</td><td>6</td><td>6E</td><td>6</td><td>6E</td><td></td><td></td></tr><tr><td>7</td><td></td><td></td><td></td><td>7</td><td>7</td><td></td><td>1357</td><td>8ACE</td><td></td><td></td><td>E</td><td>E</td><td></td><td></td><td></td><td></td></tr><tr><td>8</td><td></td><td></td><td></td><td>8</td><td>8</td><td></td><td>8ACE</td><td>1357</td><td></td><td></td><td>1</td><td>1</td><td></td><td></td><td></td><td></td></tr><tr><td>9</td><td></td><td></td><td>89</td><td>9</td><td>89</td><td>9</td><td>8ACE</td><td></td><td></td><td></td><td>1357</td><td>9</td><td>19</td><td>9</td><td>19</td><td></td></tr><tr><td>A</td><td></td><td></td><td></td><td>A</td><td>C</td><td></td><td></td><td></td><td></td><td></td><td></td><td>3</td><td>5</td><td></td><td></td><td></td></tr><tr><td>B</td><td></td><td></td><td>AB</td><td>B</td><td>CD</td><td>D</td><td></td><td></td><td></td><td></td><td></td><td>B</td><td>3B</td><td>D</td><td>5D</td><td></td></tr><tr><td>C</td><td></td><td></td><td></td><td>C</td><td>A</td><td></td><td></td><td></td><td></td><td></td><td></td><td>5</td><td>3</td><td></td><td></td><td></td></tr><tr><td>D</td><td></td><td></td><td>CD</td><td>D</td><td>AB</td><td>B</td><td></td><td></td><td></td><td></td><td></td><td>D</td><td>5D</td><td>B</td><td>3B</td><td></td></tr><tr><td>E</td><td></td><td>8ACE</td><td></td><td>E</td><td>E</td><td></td><td></td><td></td><td></td><td></td><td></td><td>7</td><td>7</td><td></td><td>1357</td><td></td></tr><tr><td>F</td><td>89AB<br>CDEF</td><td>9BDF</td><td>EF</td><td>F</td><td>EF</td><td>F</td><td>9BDF</td><td>9BDF</td><td>9BDF</td><td>9BDF</td><td>F</td><td>7F</td><td>F</td><td>7F</td><td>9BDF</td><td>1357<br>9BDF</td></tr></tbody></table>

Figure 4 shows a computer-generated composition table. Observe that operation 3 is a neutral element, and the operations $3, 5, A, C$ have inverses; in fact, this set is a group w.r.t. composition. Figure 5 shows the sets of left inverses w.r.t composition; in line $p$, column $q$, all operations $x$ are listed that satisfy $x \circ q = p$. To save space, we omitted braces and commas. Similarly, Fig. 6 shows the right inverses; line $p$, column $q$ contains all $x$ such that $p \circ x = q$.

A machine-supported investigation of the algebraic structure w.r.t. composition showed nothing interesting. Of the 65536 possible operation sets, 461 are closed w.r.t. composition; besides $\{3, 5, A, C\}$ the subsets $\{0\}, \{F\}, \{1, E\}, \{2, 4\}, \{7, 8\},$ and $\{B, D\}$ are maximal groups, each with a different neutral element. Each of the 296 closed subset containing 3 is, of course, a monoid; besides them, the subsets $\{0, 1, E, F\}, \{0, 2, 4\}, \{0, 7, 8, F\},$ and $\{B, D, F\}$ are maximal monoids, again each with a different neutral element. The ancillary file `optnComposition_GroupsMonoids.txt` lists each operation set that is closed w.r.t. composition, and indicates whether it is a monoid, or even a group.

**Definition 9. (Lifted property)** If $prop$ is a property of binary relations, and $q$ is a unary operation, then we call $q-prop$ a *lifted property*. We define that a relation $R$ has the property $q-prop$ if $R^q$ has the property $prop$. $\square$

In this way, unary operations can be lifted from relations to relation properties. For example, 8-transitivity is a synonym for incomparability-transitivity, and irreflexivity coincides with $C$-reflexivity.
<table><caption>Figure 6: Right inverses w.r.t. composition ($p \circ? = q$)</caption><thead><tr><th>p\q</th><th>0</th><th>1</th><th>2</th><th>3</th><th>4</th><th>5</th><th>6</th><th>7</th><th>8</th><th>9</th><th>A</th><th>B</th><th>C</th><th>D</th><th>E</th><th>F</th></tr></thead><tbody><tr><td>0</td><td>*</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>1</td><td>024</td><td>135</td><td></td><td></td><td></td><td></td><td>6</td><td>7</td><td>8AC</td><td>9BD</td><td></td><td></td><td></td><td></td><td>E</td><td>F</td></tr><tr><td>2</td><td>0167<br>89EF</td><td></td><td>23AB</td><td>45CD</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>3</td><td>0</td><td>1</td><td>2</td><td>3</td><td>4</td><td>5</td><td>6</td><td>7</td><td>8</td><td>9</td><td>A</td><td>B</td><td>C</td><td>D</td><td>E</td><td>F</td></tr><tr><td>4</td><td>0167<br>89EF</td><td></td><td>45CD</td><td>23AB</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>5</td><td>0</td><td>1</td><td>4</td><td>5</td><td>2</td><td>3</td><td>6</td><td>7</td><td>8</td><td>9</td><td>C</td><td>D</td><td>A</td><td>B</td><td>E</td><td>F</td></tr><tr><td>6</td><td>0167<br>89EF</td><td></td><td></td><td></td><td></td><td></td><td>2345<br>ABCD</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>7</td><td>0</td><td>1</td><td></td><td></td><td></td><td></td><td>246</td><td>357</td><td>8</td><td>9</td><td></td><td></td><td></td><td></td><td>ACE</td><td>BDF</td></tr><tr><td>8</td><td>BDF</td><td>ACE</td><td></td><td></td><td></td><td></td><td>9</td><td>8</td><td>357</td><td>246</td><td></td><td></td><td></td><td></td><td>1</td><td>0</td></tr><tr><td>9</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>2345<br>ABCD</td><td></td><td></td><td></td><td></td><td></td><td>0167<br>89EF</td></tr><tr><td>A</td><td>F</td><td>E</td><td>B</td><td>A</td><td>D</td><td>C</td><td>9</td><td>8</td><td>7</td><td>6</td><td>3</td><td>2</td><td>5</td><td>4</td><td>1</td><td>0</td></tr><tr><td>B</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>23AB</td><td>45CD</td><td></td><td></td><td>0167<br>89EF</td></tr><tr><td>C</td><td>F</td><td>E</td><td>D</td><td>C</td><td>B</td><td>A</td><td>9</td><td>8</td><td>7</td><td>6</td><td>5</td><td>4</td><td>3</td><td>2</td><td>1</td><td>0</td></tr><tr><td>D</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>45CD</td><td>23AB</td><td></td><td></td><td>0167<br>89EF</td></tr><tr><td>E</td><td>F</td><td>E</td><td></td><td></td><td></td><td></td><td>9BD</td><td>8AC</td><td>7</td><td>6</td><td></td><td></td><td></td><td></td><td>135</td><td>024</td></tr><tr><td>F</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>*</td></tr></tbody></table>
Starting from the 24 basic properties from Def. 1,<fnref n="3" /> we obtain 24 · 16 = 384 lifted properties, some of which coincide. We call two lifted properties equivalent if they agree on every relation on a sufficiently large,<fnref n="4" /> finite or infinite, domain set. For example, 3-transitivity is equivalent to 5-transitivity, due to the self-duality of the definition. We first show a few simple laws about lifted properties that are needed later on. In the next section, we compute equivalence classes of lifted properties.

**Lemma 10. (Operations and properties)**

1. Operation 0 always yields the empty relation.

2. Operation F always yields the universal relation.

3. Operations B, D, F always yield a connex relation.

4. Operations 0, 2, 4, 6 always yield an irreflexive relation.

5. Operations 1, 3, 5, 7 preserve reflexivity and irreflexivity.

6. Operations 8, A, C, E invert reflexivity and irreflexivity.

7. Operations 0, 2, 4 always yield an asymmetric relation.

8. Operations 9, B, D, F always yield a reflexive relation.

9. Operations 0, 9, B, D, F always yield a dense relation.

10. Operations 9, B, D, F always yield a left serial relation.

11. Operations 0, 9, B, D, F always yield a left quasi-reflexive relation.

12. Operations 0, B, D, F always yield a relation that satisfies semi-order property 1.

13. Operations 0, B, D, F always yield a relation that satisfies semi-order property 2.

14. Operations 0, 1, 6, 7, 8, 9, E, F always yield a symmetric relation.

**PROOF.** 1. Obvious from Def. 6. See [1, Exm.74, p.48] for the properties satisfied by the empty relation,

2. Obvious from Def. 6. See [1, Exm.75, p.48] for the properties satisfied by the universal relation,

3. Each listed operation $q$ satisfies $7 \circ q = F$, hence the symmetric closure of its result relation is the universal one.

4. $xR^q x$ boils down to *false* for $q \in \{0, 2, 4, 6\}$.

5. For $q \in \{1, 3, 5, 7\}$, the formula $xR^q x$ boils down to $xRx$; hence $R^q$ is (ir)reflexive iff $R$ is.

6. For $q \in \{8, A, C, E\}$, the formula $xR^q x$ boils down to $\neg xRx$; hence $R^q$ is reflexive iff $R$ is irreflexive, and $R^q$ is irreflexive iff $R$ is reflexive.

7. Each listed operation $q$ satisfies $q \cap (5 \circ q) = 0$, hence its result relation is disjoint from its own converse.

8. $xR^9 x$ iff $xRx \oplus \neg xRx$ iff true. Similarly, $xR^q x$ boils down to true for $q \in \{B, D, F\}$.

9. The empty relation $R^0$ is dense by [1, Exm.74.11, p.48]. Operations 9, B, D, F always yield a reflexive relation by 8, which is dense by [1, Lem.48.1, p.38].

<footnote n="3">³ Unlike in [1], we this time included left-, right-, and two-sided quasi-reflexivity, to obtain machine-generated evidence for the laws about them; cf. Fig. 8. We didn't include co-transitivity (which we only recently became aware of) since it obviously can be expressed as C-Trans.</footnote>

<footnote n="4">⁴ It will turn out that two properties agree on every relation on a 7-element domain iff they agree on every relation of a larger domain, see Thm. 22.</footnote>
10. Operations 9, B, D, F always yield a reflexive relation by 8, which is left-serial by
   [1, Lem.54, p.40].

11. The empty relation $R^0$ is quasi-reflexive by [1, Exm.74.1, p.48], hence left quasi-reflexive in particular. Operations 9, B, D, F always yield a reflexive relation by 8, which is quasi-reflexive by [1, Lem.9, p.23], and hence left quasi-reflexive.

12. The empty relation $R^0$ satisfies semi-order property 1 by [1, Exm.74.9, p.48]. Operations B, D, F always yield a connex relation by Lem. 10.3, which satisfies semi-order property 1 by [1, Lem.66, p.45].

13. The empty relation $R^0$ satisfies semi-order property 2 by [1, Exm.74.9, p.48]. Operations B, D, F always yield a connex relation by Lem. 10.3, which satisfies semi-order property 2 by [1, Lem.66, p.45].

14. Each listed operation $q$ satisfies $q = 5 \circ q$, hence its result relation agrees with its own converse. $\square$

**Lemma 11.** (Unsatisfiable lifted properties) On a domain set $X$ with $\ge 1$ elements, no relation has any of the following properties:

1. 9-, B-, D-, F-ASym

2. 9-, B-, D-, F-AntiTrans

3. 0-LfSerial

4. 0-, 2-, 4-, 6-Refl

On a domain set with $\ge 2$ elements, no relation has one of the following properties:

5. F-AntiSym

On a domain set with $\ge 4$ elements, no relation has one of the following properties:

6. B-, D-, F-LfUnique

**PROOF.** On a nonempty domain set:

1. By Lem. 10.8, operations 9, B, D, F yield a reflexive relation, which cannot be asymmetric by [1, Lem.10, p.23].

2. By Lem. 10.8, operations 9, B, D, F yield a reflexive relation, which cannot be anti-transitive by [1, Lem.10, p.23].

3. Operation 0 always yields the empty relation which isn't left-serial on a non-empty domain.

4. By Lem. 10.4, operations 0, 2, 4, 6 yield an irreflexive relation, which cannot be reflexive on a nonempty domain.

On a domain set with $\ge 2$ elements:

5. For $x \neq y$, we have $xR^Fy \wedge yR^Fx$, contradicting anti-symmetry.

On a domain set with $\ge 4$ elements:

6. By Lem. 10.3, operations B, D, F yield a connex relation, which cannot be left-unique on a set of 4 or more elements by [1, Lem.51, p.39]. $\square$
**Lemma 12. (Operation names)**

1. The symmetric kernel of a relation $R$ is obtained as $R^1$.

2. The symmetric closure of a relation $R$ is obtained as $R^7$.

3. The asymmetric kernel of a relation $R$ is obtained as $R^2$. As discussed in Def. 3.3, it is an asymmetric subset of $R$, but need not be a maximal one.

**PROOF.** 1. We show that $R^1$ is the largest symmetric sub-relation of $R$. First, $R^1$ is symmetric by Lem. 10.14, and a subset of $R$ by Lem. 7.4. If $R' \subseteq R$ is a symmetric relation, then $xR'y$ implies $yR'x$ by symmetry, hence $xRy \wedge yRx$ by the subset property, hence $xR^1y$ by definition.

2. We show that $R^7$ is the smallest symmetric super-relation of $R$. First, $R^7$ is symmetric by Lem. 10.14, and a superset of $R$ by Lem. 7.4. Let $R' \supseteq R$ be a symmetric relation. If $xR^7y$, then by definition $xRy$ or $yRx$. In the former case, we have $xR'y$ per superset, in the latter, we additionally use the symmetry of $R'$.

3. We show that $R^2$ equals the intersection of all maximal asymmetric sub-relations of $R$.

"$\subseteq$": Let $R'$ be a maximal asymmetric subset of $R$, we show $R^2 \subseteq R'$: Let $xR^2y$, then $xRy \wedge \neg yRx$, hence $\neg yR'x$. If $xR'y$ did not hold, then $R' \cup \{\langle x, y \rangle\}$ was a larger, but still asymmetric subset of $R$.

"$\supseteq$": First, $\{\}$ is an asymmetric subset of $R$, hence<fnref n="5" /> a maximal one can also be found; we call it $R_0$. Now let $xR'y$ for every maximal asymmetric subset $R'$ of $R$, we show $xR^2y$. We have in particular $xR_0y$, hence $xRy$, Assume for contradiction $yRx$ does also hold. Then $R_1 = (R_0 \setminus \{\langle x, y \rangle\}) \cup \{\langle y, x \rangle\}$ is another maximal asymmetric subset of $R$, which, however, does not satisfy $xR_1y$, contrary to our assumption.

Note that $R^2$ is asymmetric by Lem. 10.7, and a subset of $R$ by Lem. 7.4. In contrast, $R^4$ is different from the asymmetric kernel since it is not a subset of $R$. $\square$

<footnote n="5">⁵ We use Zorn's lemma here.</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 7: Partition split algorithm</figcaption></figure>

4. Equivalent lifted properties

In this section, we investigate extensional equality of lifted properties. We show that,
starting from the basic property set from Def. 1, a of total 81 different equivalence classes
exist (Thm. 22).

To obtain an approximation of equivalence, we implemented a partition-refinement
routine: initially, all 384 lifted properties are in one partition; cycling through each relation
R on a small finite set, we split each partition according to the property behavior on
R. Figure 7 shows a snapshot of the algorithm, when it is about to split the partition
{3-LfUnique, C-LfSerial} into two singleton sets, since the current relation is not left
unique, but its complement is left serial. Running the routine on the relations over a 5-
element set, we ended up with 80 partitions; for a 6-element set, the very same partitions
were obtained; checking on a 7-element set would take far too long.

The raw output about the computed partitions is available in the ancillary file
`lpEqns.txt`; each partition is represented as an equation chain like `5-Trans = 3-Trans`.
Most of them are easily seen to be in fact equivalences, we give the formal proofs in the
following. Some equivalences allow us to define one property in terms of another, see
Fig. 8 and Lem. 14 below.

Figure 9 shows the partitions, omitting the redundant properties for brevity. Each box
in the left part denotes one partition. The two topmost boxes denote the trivial partitions,
viz. that of properties that hold for no relation at all (left) and for every relation (right);
only two of the 46 and 17 members, are shown, respectively. These two partitions together
contain all lifted properties starting with 0- or F-,<fnref n="6" /> along with many others, like 2-Refl
and 7-Sym.

Partitions containing only different operations prepended to a single basic property
are called pure partitions. They are not shown as a box, but listed in the right part of
Fig. 9. For example, the first line is short notation for the raw output chains `1-ASym =
3-ASym = 5-ASym` and `8-ASym = A-ASym = C-ASym`. Singleton partitions are a subclass
of pure partitions; they are listed separately. For example, the first line is short notation
for the trivial raw output chains `7-ASym` and `E-ASym`.<fnref n="7" />

<footnote n="6">⁶ The property 0-*prop* applies to a relation *R* iff *prop* applies to the empty relation, independent of *R*. Hence, 0-*prop* is either true on all relations or false on all. Similar for F-*prop*.</footnote>

<footnote n="7">⁷ Note that the actual chains in file *lpEqns.txt* are longer than shown here, since they still contain</footnote>
<figure><img src="image_5.png" /><figcaption>Figure 8: Redundant properties</figcaption></figure>

By construction, the computed partitioning is a coarsening of the proper extensional
equality partitioning. To obtain the latter, it sufficient to split the largest box partition
along the dotted line, as we will show in Sect. 4.1, in particular in Thm. 22. We thus arrive
at a total of 81 equivalence classes of lifted properties. We chose a default representation
for each class, they are shown in Figure 10.<fnref n="8" /> Considering all of them in our naive Quine-
McCluskey implementation from [1, Sect.6] would require more than 2⁸¹ bits, i.e. 274877
millions of Tera bytes. This still renders that approach infeasible.

However, it could be used to investigate small subsets of properties, looking for law
suggestions including complement, converse, etc. For example, to investigate the connec-
tions between quasi-transitivity and semi-orders, one may restrict oneself to QuasiTrans,
SemiOrd1, SemiOrd2, and ASym. From Fig. 10, it can seen that 21 distinct properties
would be needed.<fnref n="9" /> However, we didn’t yet perform such an investigation.

Instead, we checked all possible implications between default representations up to a
length of 3, i.e. with at most 2 antecedents. This is presented in Sect. 5.

<footnote>redundant properties.</footnote>

<footnote n="8">⁸ The figure shows, for each unary operation *q* and each basic property *prop*, the default representation to which *q-prop* is extensionally equal. If *q-prop* is its own default representation, it is highlighted in blue and cyan, for a non-singleton and a singleton equivalence class, respectively. The trivial partitions are denoted by + and -.</footnote>

<footnote n="9">⁹ +, -, as, 7-as, C-as, E-as, s1, 1-s1, 2-s1, 7-s1, C-s1, s2, 2-s2, C-s2, sy, 1-tr, 2-tr, 7-tr, 8-tr, 9-tr, E-tr.</footnote>
<table><tr><td>F-AntiSym<br>0-Refl ...</td><td>F-LfSerial<br>0-Sym ...</td></tr><tr><td>D-Sym<br>D-LfEucl<br>C-Sym<br>B-Sym<br>B-LfEucl<br>A-Sym<br>9-SemiOrd2<br>9-SemiOrd1<br>6-AntiSym<br>6-LfQuasiRefl<br>6-SemiOrd1<br>6-Trans<br>6-ASym<br>6-LfEucl<br>5-Sym<br>4-LfQuasiRefl<br>4-Sym<br>4-LfEucl<br>3-Sym<br>2-LfQuasiRefl<br>2-Sym<br>2-LfEucl<br>..................<br>4-Dense<br>2-Dense</td><td>D-AntiSym<br>B-AntiSym<br>9-AntiSym<br>9-LfUnique<br><br>1-LfEucl<br>E-SemiOrd2<br>1-Trans<br><br>7-LfEucl<br>8-SemiOrd2<br>7-Trans<br><br>8-LfEucl<br>7-SemiOrd2<br>8-Trans<br><br>9-LfEucl<br>6-SemiOrd2<br>9-Trans<br><br>E-LfEucl<br>1-SemiOrd2<br>E-Trans</td></tr></table>

### Pure Partitions

ASym: $1 \leftrightarrow 3 \leftrightarrow 5$, $8 \leftrightarrow A \leftrightarrow C$
AntiSym: $1 \leftrightarrow 3 \leftrightarrow 5$, $8 \leftrightarrow A \leftrightarrow C$
Refl: $1 \leftrightarrow 3 \leftrightarrow 5 \leftrightarrow 7$, $8 \leftrightarrow A \leftrightarrow C \leftrightarrow E$

SemiOrd1: $1 \leftrightarrow E$, $2 \leftrightarrow 4$, $3 \leftrightarrow 5$, $7 \leftrightarrow 8$, $A \leftrightarrow C$
SemiOrd2: $2 \leftrightarrow 4$, $3 \leftrightarrow 5$, $A \leftrightarrow C$
AntiTrans: $2 \leftrightarrow 4$, $3 \leftrightarrow 5$, $A \leftrightarrow C$
Trans: $2 \leftrightarrow 4$, $3 \leftrightarrow 5$, $B \leftrightarrow D$, $A \leftrightarrow C$
Dense: $3 \leftrightarrow 5$, $A \leftrightarrow C$

### Singleton Partitions

ASym: 7, E
AntiSym: 7, E
AntiTrans: 1, 6, 7, 8, E
Dense: 1, 6, 7, 8, E
LfEucl: 3, 5, A, C
LfSerial: 1, 2, 3, 4, 5, 6, 7, 8, A, C, E
LfUnique: 1, 2, 3, 4, 5, 6, 7, 8, A, C, E
LfQuasiRefl: 1, 3, 5, 7, 8, A, C, E

<caption>Figure 9: Computed partitions of lifted properties</caption>
<table><caption>Figure 10: Default representations of lifted properties</caption><thead><tr><th></th><th></th><th>0</th><th>1</th><th>2</th><th>3</th><th>4</th><th>5</th><th>6</th><th>7</th><th>8</th><th>9</th><th>A</th><th>B</th><th>C</th><th>D</th><th>E</th><th>F</th></tr></thead><tbody><tr><td>em</td><td>Empty</td><td>+</td><td>as</td><td>sy</td><td>7-as</td><td>sy</td><td>7-as</td><td>sy</td><td>7-as</td><td>C-as</td><td>-</td><td>E-as</td><td>-</td><td>E-as</td><td>-</td><td>E-as</td><td>-</td></tr><tr><td>un</td><td>Univ</td><td>-</td><td>E-as</td><td>-</td><td>E-as</td><td>-</td><td>E-as</td><td>-</td><td>C-as</td><td>7-as</td><td>sy</td><td>7-as</td><td>sy</td><td>7-as</td><td>sy</td><td>3-as</td><td>+</td></tr><tr><td>rf</td><td>Refl</td><td>-</td><td>rf</td><td>-</td><td>rf</td><td>-</td><td>rf</td><td>-</td><td>rf</td><td>C-rf</td><td>+</td><td>C-rf</td><td>+</td><td>C-rf</td><td>+</td><td>C-rf</td><td>+</td></tr><tr><td></td><td>Irrefl</td><td>+</td><td>C-rf</td><td>+</td><td>C-rf</td><td>+</td><td>C-rf</td><td>+</td><td>C-rf</td><td>rf</td><td>-</td><td>rf</td><td>-</td><td>rf</td><td>-</td><td>rf</td><td>-</td></tr><tr><td></td><td>CoRefl</td><td>+</td><td>an</td><td>sy</td><td>7-an</td><td>sy</td><td>7-an</td><td>sy</td><td>7-an</td><td>C-an</td><td>9-an</td><td>E-an</td><td>-</td><td>E-an</td><td>-</td><td>E-an</td><td>-</td></tr><tr><td>lq</td><td>LfQuasiRefl</td><td>+</td><td>1-lq</td><td>sy</td><td>lq</td><td>sy</td><td>5-lq</td><td>sy</td><td>7-lq</td><td>8-lq</td><td>+</td><td>A-lq</td><td>+</td><td>C-lq</td><td>+</td><td>E-lq</td><td>+</td></tr><tr><td></td><td>RgQuasiRefl</td><td>+</td><td>1-lq</td><td>sy</td><td>5-lq</td><td>sy</td><td>lq</td><td>sy</td><td>7-lq</td><td>8-lq</td><td>+</td><td>C-lq</td><td>+</td><td>A-lq</td><td>+</td><td>E-lq</td><td>+</td></tr><tr><td></td><td>QuasiRefl</td><td>+</td><td>1-lq</td><td>sy</td><td>7-lq</td><td>sy</td><td>7-lq</td><td>sy</td><td>7-lq</td><td>8-lq</td><td>+</td><td>E-lq</td><td>+</td><td>E-lq</td><td>+</td><td>E-lq</td><td>+</td></tr><tr><td>sy</td><td>Sym</td><td>+</td><td>+</td><td>sy</td><td>sy</td><td>sy</td><td>sy</td><td>+</td><td>+</td><td>+</td><td>+</td><td>sy</td><td>sy</td><td>sy</td><td>sy</td><td>+</td><td>+</td></tr><tr><td>as</td><td>ASym</td><td>+</td><td>as</td><td>+</td><td>as</td><td>+</td><td>as</td><td>sy</td><td>7-as</td><td>C-as</td><td>-</td><td>C-as</td><td>-</td><td>C-as</td><td>-</td><td>E-as</td><td>-</td></tr><tr><td>an</td><td>AntiSym</td><td>+</td><td>an</td><td>+</td><td>an</td><td>+</td><td>an</td><td>sy</td><td>7-an</td><td>C-an</td><td>9-an</td><td>C-an</td><td>9-an</td><td>C-an</td><td>9-an</td><td>E-an</td><td>-</td></tr><tr><td></td><td>SemiConnex</td><td>-</td><td>E-an</td><td>9-an</td><td>C-an</td><td>9-an</td><td>C-an</td><td>9-an</td><td>C-an</td><td>7-an</td><td>sy</td><td>an</td><td>+</td><td>an</td><td>+</td><td>an</td><td>+</td></tr><tr><td></td><td>Connex</td><td>-</td><td>E-as</td><td>-</td><td>C-as</td><td>-</td><td>C-as</td><td>-</td><td>C-as</td><td>7-as</td><td>sy</td><td>as</td><td>+</td><td>as</td><td>+</td><td>as</td><td>+</td></tr><tr><td>tr</td><td>Trans</td><td>+</td><td>1-tr</td><td>2-tr</td><td>tr</td><td>2-tr</td><td>tr</td><td>sy</td><td>7-tr</td><td>8-tr</td><td>9-tr</td><td>C-tr</td><td>D-tr</td><td>C-tr</td><td>D-tr</td><td>E-tr</td><td>+</td></tr><tr><td>at</td><td>AntiTrans</td><td>+</td><td>1-at</td><td>2-at</td><td>at</td><td>2-at</td><td>at</td><td>6-at</td><td>7-at</td><td>8-at</td><td>-</td><td>C-at</td><td>-</td><td>C-at</td><td>-</td><td>E-at</td><td>-</td></tr><tr><td></td><td>QuasiTrans</td><td>+</td><td>+</td><td>2-tr</td><td>2-tr</td><td>2-tr</td><td>2-tr</td><td>+</td><td>+</td><td>+</td><td>+</td><td>2-tr</td><td>2-tr</td><td>2-tr</td><td>2-tr</td><td>+</td><td>+</td></tr><tr><td></td><td>RgEucl</td><td>+</td><td>1-tr</td><td>sy</td><td>5-le</td><td>sy</td><td>le</td><td>sy</td><td>7-tr</td><td>8-tr</td><td>9-tr</td><td>C-le</td><td>sy</td><td>A-le</td><td>sy</td><td>E-tr</td><td>+</td></tr><tr><td>le</td><td>LfEucl</td><td>+</td><td>1-tr</td><td>sy</td><td>le</td><td>sy</td><td>5-le</td><td>sy</td><td>7-tr</td><td>8-tr</td><td>9-tr</td><td>A-le</td><td>sy</td><td>C-le</td><td>sy</td><td>E-tr</td><td>+</td></tr><tr><td>s1</td><td>SemiOrd1</td><td>+</td><td>1-s1</td><td>2-s1</td><td>s1</td><td>2-s1</td><td>s1</td><td>sy</td><td>7-s1</td><td>7-s1</td><td>sy</td><td>C-s1</td><td>+</td><td>C-s1</td><td>+</td><td>1-s1</td><td>+</td></tr><tr><td>s2</td><td>SemiOrd2</td><td>+</td><td>E-tr</td><td>2-s2</td><td>s2</td><td>2-s2</td><td>s2</td><td>9-tr</td><td>8-tr</td><td>7-tr</td><td>sy</td><td>C-s2</td><td>+</td><td>C-s2</td><td>+</td><td>1-tr</td><td>+</td></tr><tr><td></td><td>RgSerial</td><td>-</td><td>1-ls</td><td>4-ls</td><td>5-ls</td><td>2-ls</td><td>ls</td><td>6-ls</td><td>7-ls</td><td>8-ls</td><td>+</td><td>C-ls</td><td>+</td><td>A-ls</td><td>+</td><td>E-ls</td><td>+</td></tr><tr><td>ls</td><td>LfSerial</td><td>-</td><td>1-ls</td><td>2-ls</td><td>ls</td><td>4-ls</td><td>5-ls</td><td>6-ls</td><td>7-ls</td><td>8-ls</td><td>+</td><td>A-ls</td><td>+</td><td>C-ls</td><td>+</td><td>E-ls</td><td>+</td></tr><tr><td>de</td><td>Dense</td><td>+</td><td>1-de</td><td>2-de</td><td>de</td><td>2-de</td><td>de</td><td>6-de</td><td>7-de</td><td>8-de</td><td>+</td><td>C-de</td><td>+</td><td>C-de</td><td>+</td><td>E-de</td><td>+</td></tr><tr><td></td><td>IncTrans</td><td>+</td><td>E-tr</td><td>9-tr</td><td>8-tr</td><td>9-tr</td><td>8-tr</td><td>9-tr</td><td>8-tr</td><td>7-tr</td><td>sy</td><td>1-tr</td><td>+</td><td>1-tr</td><td>+</td><td>1-tr</td><td>+</td></tr><tr><td>lu</td><td>LfUnique</td><td>+</td><td>1-lu</td><td>2-lu</td><td>lu</td><td>4-lu</td><td>5-lu</td><td>6-lu</td><td>7-lu</td><td>8-lu</td><td>9-an</td><td>A-lu</td><td>-</td><td>C-lu</td><td>-</td><td>E-lu</td><td>-</td></tr><tr><td></td><td>RgUnique</td><td>+</td><td>1-lu</td><td>4-lu</td><td>5-lu</td><td>2-lu</td><td>lu</td><td>6-lu</td><td>7-lu</td><td>8-lu</td><td>9-an</td><td>C-lu</td><td>-</td><td>A-lu</td><td>-</td><td>E-lu</td><td>-</td></tr></tbody></table>
### 4.1. *Proof of equivalence classes*

**Lemma 13.** 1. If $R$ is symmetric, then $R^0 = R^2 = R^4 = R^6$ are the empty relation, and $R^9 = R^B = R^D = R^F$ are the universal relation.

2. If $R$ is asymmetric, then $R^0 = R^1$ are the empty relation, and $R^E = R^F$ are the universal relation.

**PROOF.** 1. Symmetry implies $R = R^7$, hence $R^2 = R^{(2 \circ 7)} = R^0$, similar for the other operations.

2. Asymmetry implies $R = R^2$, hence $R^1 = R^{(1 \circ 2)} = R^0$, similar for $E$. $\square$

<figure><img src="image_6.png" /></figure>

### Lemma 14. (Redundant properties)

1. $RgSerial \Leftrightarrow 5-LfSerial$

2. $RgEucl \Leftrightarrow 5-LfEucl$

3. $RgUnique \Leftrightarrow 5-LfUnique$

4. $RgQuasiRefl \Leftrightarrow 5-LfQuasiRefl$

5. $QuasiRefl \Leftrightarrow 7-LfQuasiRefl$

6. $Univ \Leftrightarrow E-ASym$

7. $Empty \Leftrightarrow 7-ASym$

8. $Irrefl \Leftrightarrow C-Refl$

9. $Connex \Leftrightarrow C-ASym$

10. $SemiConnex \Leftrightarrow C-AntiSym$

11. $IncTrans \Leftrightarrow 8-Trans$

12. $CoRefl \Leftrightarrow 7-AntiSym$

13. $QuasiTrans \Leftrightarrow 2-Trans$

In Fig. 8, we summarize these redundancies.

**PROOF.** 1–4 From the definitions in Def. 1 is obvious that each “$Rg$” property is the converse of the corresponding “$Lf$” property.

5. First, observe that $xRx$ iff $xR^7x$ by definition.

“⇒”: If $xR^7y$, then $xRy \lor yRx$; both cases imply $xRx$ by quasi-reflexivity.

“ ⇐”: If $xRy$, then $xRy \lor yRx$ by weakening, hence $xR^7y$, and similarly $yR^7x$, hence $xR^7x$ and $yR^7y$.

6. “⇒”: Let $xR^Ey$, then $
eg xRy \lor \neg yRx$; both cases contradict universality.

“ ⇐”: Let $R^E$ be asymmetric; it is also symmetric by Lem. 10.14, hence empty by [1, Lem.16, p.25], hence $
eg xRy \lor \neg yRx$ never holds, hence $R$ is universal.

7. “⇒”: $xR^7y$ would imply $xRy \lor yRx$, contradicting $R$'s emptiness.

“ ⇐”: $xRy$ would imply $xRy \lor yRx$ by weakening, hence $xR^7y$ and $yR^7x$, contradicting asymmetry.

8. Since $
eg xRx$ iff $xR^Cx$, for all $x$.

9. “⇒”: Let $xR^Cy$, then $
eg xRy$ by definition, hence $yRx$ by connexity, hence $
eg yR^Cx$.

“ ⇐”: If $
eg xRy$, then $xR^Cy$, hence $
eg yR^Cx$ by asymmetry, hence $yRx$.
10. Similar to 9:

“⇒”: Let $xR^Cy$, then $
eg xRy$ by definition, then $x = y$ or hence $yRx$ by semi-connexity, hence $x = y$ or $
eg yR^Cx$.

“ ⇐”: If $
eg xRy$, then $xR^Cy$, hence $x = y$ or $
eg yR^Cx$ by anti-symmetry, hence $x = y$ or $yRx$.

11. By definition.

12. “⇒”: If $xR^7y$ and $yR^7x$, then $xRy \lor yRx$; both cases imply $x = y$ by co-reflexivity.

“ ⇐”: Let $xRy$, then $xRy \lor yRx$ by weakening; this implies both $xR^7y$ and $yR^7x$, hence $x = y$ by anti-symmetry.

13. By definition.

☐

**Lemma 15.** 1. If $R$ is transitive, then its complement $R^C$ satisfies semi-order property 2.

2. If $R$ is symmetric and satisfies semi-order property 2, then its complement $R^C$ is transitive.

**PROOF.** 1. Let $xR^Cy$ and $yR^Cz$ hold, assume for contradiction that neither $wR^Cx$ nor $xR^Cw$ nor $wR^Cy$ nor $yR^Cw$ nor $wR^Cz$ nor $zR^Cw$ holds. From $xRw$ and $wRy$, we obtain $xRy$ by transitivity, contradicting our assumption.

2. Let $xR^Cy$ and $yR^Cz$ hold, assume for contradiction $xRz$. Then $zRx$ by symmetry, and $xRy \lor yRx \lor yRz \lor zRy$ by semi-order property 2. Due to symmetry, the latter disjunction boils down to $xRy \lor yRz$, contradicting our assumption. ☐

**Lemma 16.** For $q \in \{0, 1, 6, 7, 8, 9, E, F\}$, a relation $R$ is $q$-left-Euclidean iff it is $q$-transitive.

**PROOF.** By Lem. 10.14, $R^q$ is symmetric. Hence $q$-left-Euclideanness and $q$-transitivity coincide by [1, Lem.36, p.33]. ☐

**Lemma 17. (Characterization of symmetry)** All of the following properties are equivalent:

1. 6-AntiSym

2. 6-ASym

3. 2-, 4-, 6-LfQuasiRefl

4. 2-, 4-, 6-, B-, D-LfEucl

5. 6-, 9-SemiOrd1

6. 9-SemiOrd2

7. 2-, 3-, 4-, 5-, A-, B-, C-, D-Sym

8. 6-Trans
PROOF. We show for each property that is applies to a relation $R$ iff $R$ is symmetric.

For the “if” part, observe that for a symmetric $R$, we have $R^0 = R^2 = R^4 = R^6$ empty by Lem. 13.1, and hence asymmetric and anti-symmetric by [1, Exm.74.6, p.48], left Euclidean by [1, Exm.74.2, p.48], quasi-reflexive by [1, Exm.74.1, p.48], symmetric by [1, Exm.74.3, p.48], transitive by [1, Exm.74.7, p.48], and satisfy semi-order property 1 and 2 by [1, Exm.74.9, p.48]. Moreover, for a symmetric $R$, we have that $R^9 = R^B = R^D = R^F$ are universal by Lem. 13.1, and hence left Euclidean by [1, Exm.75.1, p.48], symmetric by [1, Exm.75.2, p.48] and satisfy semi-order property 1 and 2 by [1, Exm.75.5, p.48]. And for symmetric $R$ we have $R^5$ symmetric by self-duality, $R^C$ symmetric by contraposition, and $R^A$ symmetric by duality to $R^C$.

For the “only if” part:

1. Let $R^6$ be anti-symmetric, we show that $R$ is symmetric. Let $xRy$, assume for contradiction $
eg yRx$; then $x 
eq y$. Moreover, $xR^6y$ by definition, hence $
eg yR^6x$ by anti-symmetry, contradicting Lem. 10.14.

2. Follows from 1 and [1, Lem.13.2, p.25].

3. Case 2: Let $xRy$, assume for contradiction $
eg yRx$. Then $xR^2y$, hence $xR^2x$ by left quasi-reflexivity; this contradicts Lem. 10.4.

* Cases 4 and 6 are shown similar.

4. Cases 2, 4, and 6 follow from 3, using [1, Lem.46, p.37].

* Case B: Let $xRy$, then $xR^B y$ by definition. Moreover $yR^B y$ by Lem. 10.8, hence $yR^B x$ by Euclideaness, hence $yRx \lor \neg xRy$ by definition, hence $yRx$ by our assumption.

* Case D is similar.

5. Case 6: Let $xRy$, assume for contradiction $
eg yRx$. Then $xR^6y$ by definition, hence $yR^6x$ by Lem. 10.14. Moreover, $
eg xR^6x$ by Lem. 10.8. Applying semi-order property 1 to $yR^6x$, $
eg xR^6x$, and $xR^6y$ infers $yR^6y$, contradicting Lem. 10.4.

* Case 9: Let $xRy$, assume for contradiction $
eg yRx$. Then $
eg xR^9y$ and also $
eg yR^9x$ by definition. Moreover, $xR^6x$ and $yR^9y$ by Lem. 10.8. Applying semi-order property 1 to $xR^9x$, $x, y$ incomparable w.r.t. $R^9$, and $yR^9y$ infers $xR^9y$, contradicting the incomparability of $x, y$.

6. By Lem. 10.8, $R^9$ is reflexive, hence also connex by [1, Lem.66, p.45]. Since $R^9$ is also symmetric by Lem. 10.14, it is universal by [1, Lem.53.2, p.40]. By definition, this means that $xRy$ and $yRx$ agree everywhere, i.e. that $R$ is symmetric.

7. Case 2: Let $xRy$, assume for contradiction $
eg yRx$. Then $xR^2y$ by definition, hence $yR^2$ by symmetry, hence $yRx$ by definition, contradicting our assumption.

* Case B: Let $xRy$, then $xR^B y$ by definition, hence $yR^B x$ by symmetry, hence $yRx$ by definition, since $
eg xRy$ cannot hold.

* Cases 4 and D follow by duality.

* Case 3 is trivial.

* Cases 5, A, and C follow by duality and contraposition.

8. Let $xRy$, assume for contradiction $
eg yRx$. Then, $xR^6y$ and also $yR^6x$ by definition, hence $xR^6x$ by transitivity, contradicting Lem. 10.4. □
**Lemma 18.** (Symmetry and semi-order property 1) If $R$ is symmetric and satisfies semi-order property 1, then $R^C$ does, too.

**PROOF.** First, we have $R$ symmetric iff $xRy \leftrightarrow yRx$ iff $
eg xRy \leftrightarrow \neg yRx$ iff $R^C$ symmetric.

Now let $R$ be symmetric and satisfy semi-order property 1, let $wR^Cx$, $
eg xR^Cy$, $
eg yR^Cx$, and $yR^Cz$ hold. Assume for contradiction $
eg wR^Cz$. Then by definition $xRy$, $
eg yRz$, and $wRz$, hence by symmetry $
eg zRy$, and $zRw$. Applying semi-order property 1 to these facts implies $xRw$, hence $wRx$, contradicting $wR^Cx$. □

**Lemma 19.** 1. A relation is 2-dense iff it is 4-dense.

2. If $R$ is symmetric, then $R^2$ is dense.

3. The converse direction does not hold if the universe set has $\ge 7$ elements.

**PROOF.** 1. $R^4$ is the converse relation of $R^2$, since $4 = 5 \circ 2$. Since the definition of density is self-dual, we are done.

2. By Lem. 13.1, $R^2$ is empty, hence dense by [1, Exm.74.11, p.48].

3. [1, Exm.76, p.49] and Fig. 12 here show an example relation on a 7-element domain that is 2-dense and not symmetric. □

**Lemma 20.** The following are equivalent:

1. $R$ is anti-symmetric and semi-connex.

2. $R^9$ is the identity relation.

3. $R^9$ is left-unique.

4. $R^9$ is anti-symmetric.

5. $R^B$ is anti-symmetric.

6. $R^D$ is anti-symmetric.

**PROOF.** By Lem. 10.14 and Lem. 10.8, $R^9$ is always symmetric and reflexive.

• **1** ⇒ **2**: Let $xR^9y$ hold, by definition, we have two cases:

– If $xRy \wedge yRx$, then $x = y$ by anti-symmetry of $R$.

– If $
eg xRy \wedge \neg yRx$, then $x = y$ since $R$ is semi-connex.

This shows that $R^9$ is co-reflexive. Since it is also reflexive, it must be the identity, by [1, Lem.5.1, p.21].

• **2** ⇒ **1**:

– Anti-symmetry: Let $xRy \wedge yRx$, then $xR^9y$ by definition, hence $x = y$.

– Semi-connex: Let $
eg xRy \wedge \neg yRx$, then again $xR^9y$ by definition, hence $x = y$.

• **2** ⇒ **3** ∧ **4**: trivial.
• **4** ⇒ **2**: If $R^9$ is anti-symmetric, then it is co-reflexive by [1, Lem.7.7, p.22], hence the identity by [1, Lem.5.1, p.21].

• **3** ⇒ **2**: $R^9$ is co-reflexive by [1, Lem.7.1, p.22], hence the identity by [1, Lem.5.1, p.21].

• **5** ∨ **6** ⇒ **4**: By Lem. 7.4, both $R^B$ and $R^D$ are supersets of $R^9$, by Lem. 5.4, anti-symmetry is antitonic.

• **1** ⇒ **5** ∧ **6**: Let $xR^By$ and $yR^Bx$, then by definition $xRy \lor \neg yRx$ and $yRx \lor \neg xRy$. This is logically equivalent to $(xRy \land yRx) \lor (\neg xRy \land \neg yRx)$, that is, to $xR^9y$. Since $R^9$ is the identity as shown above, we have $x = y$. The proof for **6** is dual. □

**Lemma 21.** (Derived equivalences) Let $prop$, $prop_i$ denote properties of binary relations.

1. If $\forall R. prop_1(R^{p1}) \to prop_2(R^{p2})$, then $\forall R. prop_1(R^{p1\ or}) \to prop_2(R^{p2\ or})$ for every operation $r$.

2. If 3-$prop \leftrightarrow$ 5-$prop$, then 2-$prop \leftrightarrow$ 4-$prop$, A-$prop \leftrightarrow$ C-$prop$, and B-$prop \leftrightarrow$ D-$prop$. This applies to the properties Refl, QuasiRefl, Sym, ASym, AntiSym, Trans, Anti-Trans, SemiOrd1, SemiOrd2, and Dense.

3. If 1-$prop \leftrightarrow$ 3-$prop$, then 0-$prop \leftrightarrow$ 4-$prop$, 1-$prop \leftrightarrow$ 5-$prop$, 8-$prop \leftrightarrow$ A-$prop$, 9-$prop \leftrightarrow$ B-$prop$, and 8-$prop \leftrightarrow$ C-$prop$. This applies to the properties Refl, ASym, and AntiSym.

4. If 3-$prop \leftrightarrow$ 7-$prop$, then 2-$prop \leftrightarrow$ 6-$prop$, 4-$prop \leftrightarrow$ 6-$prop$, 5-$prop \leftrightarrow$ 7-$prop$, A-$prop \leftrightarrow$ E-$prop$, B-$prop \leftrightarrow$ F-$prop$, C-$prop \leftrightarrow$ E-$prop$, and D-$prop \leftrightarrow$ F-$prop$. This applies to the properties Refl, and QuasiRefl.

5. If 1-$prop \leftrightarrow$ E-$prop$, then 0-$prop \leftrightarrow$ F-$prop$, 6-$prop \leftrightarrow$ 9-$prop$, and 7-$prop \leftrightarrow$ 8-$prop$. This applies to the properties Sym, and SemiOrd1.

**PROOF.** 1. Since $R^{p_i \ or} = (R^r)^{p_i}$, the consequent is an instance of the antecedent.

2. Apply **1** to $r = 2, A, B$. The listed properties are self-dual by Def. **1**.

3. Apply **1** to $r = 4, 5, A, B, C$. To prove the list:

• If $R$ is reflexive, then $R^1$ is, too, by Lem. 10.5. If $R^1$ is reflexive, then its superset $R^3$ is, too, by Lem. 5.3.

• If $R$ is asymmetric, then its subset $R^1$ is, too, by Lem. 5.4. If $R^1$ is asymmetric, it is empty by [1, Lem.16, p.25] using Lem. 10.14, that is, $xRy \land yRx$ can never happen, that is, $R$ is asymmetric.

• If $R$ is anti-symmetric, then its subset $R^1$ is, too, by Lem. 5.4. If $R^1$ is anti-symmetric, then it is co-reflexive by [1, Lem.7.7, p.22] using Lem. 10.14, that is, $xRy \land yRx$ can happen only for $x = y$, that is, $R$ is anti-symmetric.

4. Apply **1** to $r = 2, 4, 5, A, B, C, D$. To prove the list:

• If $R$ is reflexive, then $R^7$ is, too, by Lem. 10.5. If $R^7$ is reflexive, then $xRx \lor xRx$ for all $x$, hence $R$ is reflexive.
* Let $R$ be quasi-reflexive, let $xR^7y$ hold. Then $xRy \lor yRx$ by definition. Each alternative implies $xRx \land yRy$, and hence $xR^7x \land yR^7y$. Conversely, let $R^7$ be quasi-reflexive, let $xRy$ hold. Then $xR^7y$, hence $xR^7x \land yR^7y$, which boils down to $xRx \land yRy$.

5. Apply 1 to $r = 0, 6, 7$. To prove the list:

* Both $R^1$ and $R^E$ are always symmetric by Lem. 10.14.

* For semi-order property 1, the equivalence follows from Lem. 18, since $R^E = (R^1)^C$ and $R^1 = (R^E)^C$. $\square$

**Theorem 22. (Equivalent lifted properties)** On a set with $\ge 7$ elements, the equivalence classes of lifted properties coincide with the partition shown in Fig. 9, except that an own class {2-Dense, 4-Dense} must be split off from the partition of 3-Sym (indicated by the dotted line).

**PROOF.** First, 2-Dense is not equivalent to 3-Sym: for the usual $<$ relation on the rational numbers, 3-Dense and 2-Dense coincide since $<$ is asymmetric; therefore $<$ satisfies 2-Dense, but not 3-Sym; see also [1, Exm.76, p.49]. This shows the split is necessary.

By construction of the partition split algorithm from Fig. 7, no two lifted properties from different partitions in Fig. 9 can agree on all relations. Therefore, it is sufficient to show that each two members of a partition are equivalent, with the above exception.

* **Boxes:**

All properties in the topmost left and right box are equivalent by Lem. 11 and 10, respectively. The two members of the split-off class are equivalent by Lem. 19.1; all members of the remainder of that partition are equivalent by Lem. 17.

The bottommost 5 right boxes are covered by Lem. 15 (using symmetry of $R^1, R^7, R^8, R^9, R^E$ by Lem. 10.14) and 16.

The right box second from top is covered by Lem. 20.

* **Pure partitions:**

The ASym and the AntiSym partitions are covered by Lem. 21.3; the Refl partitions by this and Lem. 21.4.

The SemiOrd1 partition are covered by Lem. 21.2 and Lem. 21.5; the SemiOrd2, AntiTrans, Trans, and Dense partitions by Lem. 21.2.

Note that not all equivalences implied by Lem. 21 lead to pure partitions, e.g. B-Dense $\leftrightarrow$ D-Dense holds trivially (by Lem. 10.8 and [1, 48.1, p.38]) and is therefore reflected in the universal ("+") partition.

* **Singleton Partitions:**

Nothing to show. $\square$

**Lemma 23. (Default representations)**
1. For every “+” in the matrix in Fig. 10, the operation of its column always yields a relation satisfying the property of its row. For example, operation 9 always yields a reflexive and symmetric relation.

2. For every “-”, the column operation never yields a relation satisfying the row property. For example, operation $B$ never yields a anti-transitive or left-unique relation.

3. Whenever in a row *prop* the default representations coincide for column *p* and *q*, and *q* = *p* ◦ *r*, then *r* preserves *p-prop*. For example, operations 2, 3, 4, 5, A, B, C, D all preserve symmetry.

This generalizes Lem. 10.

PROOF. By Thm. 22, two properties are equivalent iff Fig. 10 shows the same default representation for them.

1. If operation *p-prop* has default representation +, then $R^p$ always satisfies *prop*.

2. If operation *p-prop* has default representation -, then $R^p$ never satisfies *prop*.

3. Let $R$ satisfy *p-prop*, then $R$ equivalently satisfies *q-prop*. That is, $(R^r)^p = R^q$ satisfies *prop*, hence $R^r$ satisfies *p-prop*. $\square$

**Lemma 24.** A relation $R$ is E-AntiSym iff its complement is CoRefl.

PROOF. $R^E$ is AntiSym iff $R^{7 \circ C}$ is AntiSym iff $R^C$ is 7-AntiSym iff $R^C$ is CoRefl. $\square$
## 5. Implications between lifted properties

The approach of Sect. 4 could produce only “equivalence laws”, of the form

$$ \forall R. \text{prop}_1(\text{op}_1(R)) \leftrightarrow \text{prop}_2(\text{op}_2(R)). $$

On the other hand, investigating all “disjunction laws”, of the form

$$ \forall R. \text{prop}_1(\text{op}_1(R)) \lor \dots \lor \text{prop}_n(\text{op}_n(R)), $$

for $prop_i$ a negated or unnegated property, is computationally infeasible for large $n$, as discussed in Sect. 4. As a compromise, we investigate in this section “3-implication laws”, of the form

$$ \forall R. \text{prop}_1(\text{op}_1(R)) \land \text{prop}_2(\text{op}_2(R)) \rightarrow \text{prop}_3(\text{op}_3(R)), $$

that is, implications of unnegated lifted properties with up to 2 antecedents and one conclusion.<fnref n="10" /> Note that we don't cover the negation of a lifted property; in particular, it cannot be obtained by composing it with the C operation; for example, “R is not reflexive” is usually different from “R is C-reflexive, a.k.a. irreflexive”. However, we can express true and false as 0-Sym and 0-Refl, respectively;<fnref n="11" /> hence we can express incompatibility between two lifted properties.

Since the Quine-McCluskey procedure would require too much computational resources, we used a different approach. We cycled through all $81^3 = 531441$ triples $(op_1-prop_1, op_2-prop_2, op_3-prop_3)$ of default representation of lifted properties, and for each of them searched a counter-example relation $R$ such that $prop_1(op_1(R)) \land prop_2(op_2(R)) \land \neg prop_3(op_3(R))$ holds. We recorded the search result in an array, indexed by the rank of the three default representations.<fnref n="12" /> In case no counter-example was found, we asked an external resolution prover<fnref n="13" /> to prove $prop_1(op_1(R)) \land prop_2(op_2(R)) \rightarrow prop_3(op_3(R))$, which might, or might not, succeed. In the former case, we recorded this result in the array. The remaining array cells were handled manually, unless they were trivial (Sect. 5.2).

### 5.1. Referencing an implication

To reference a 3-implication under consideration, we use its array indices, encoded in base 27, with digits represented as 0, a, b, c, ..., z. For example, the implication “SemiOrd1 $\land$ Refl $\rightarrow$ Connex” corresponds to array indices [18] [14] [11], that is, to array cell $(18 \cdot 81 + 14) \cdot 81 + 11 = 119243 = ((6 \cdot 27 + 1) \cdot 27 + 15) \cdot 27 + 11$, and is therefore encoded as faok. This encoding ensures an implication is referenced by a fixed code, unique across multiple program runs, and independent of the order in which laws

<footnote n="10">¹⁰ In [1], 58 of the found “disjunction laws” (of basic properties only) had $\ge 4$ literals; another 10 involved 3 literals, but no negation; the remaining 206 laws (= 75%) could be written as “3-implication laws”. This supports our speculation that for lifted properties, too, “3-implication laws” will cover the majority of “disjunction laws”.</footnote>

<footnote n="11">¹¹ The latter presupposes a nonempty relation domain.</footnote>

<footnote n="12">¹² The equivalence classes of lifted properties shown in Fig. 9 are numbered in the following order, cf. the list lpnfList[] in file lpImplicationsTables.c: boxed partitions starting at rank 0: 0-rf, 0-sy, 3-sy, 2-de, 9-an, 1-tr, 7-tr, 8-tr, 9-tr, E-tr; pure partitions starting at rank 10, top to bottom, left to right: 3-as, C-as, 3-an, C-an, ..., C-de; singleton partitions starting at rank 33, in the same order: 7-as, E-as, 7-an, E-an, ..., E-lq.</footnote>

<footnote n="13">¹³ EProver version E 2.3 Gielle, from http://www.eprover.org</footnote>
are found. The shell script `resolveImplCode.sh` can be used to convert base-27 codes into implications; the call `"nonprominentProperties -lpImpl resolve"` can be used for the reverse direction.

## 5.2. Trivial inferences

We implemented routines to draw trivial conclusions from a found negative (counter-example) or positive (proof) result. An inference is considered trivial if it doesn't require any knowledge about basic property definitions (as given in Def. 1), except for monotonicity information as provided in Lem. 5.3 and 5.4.

The trivial inference mechanism is intended to reduce the load on both the counter-example search and the external theorem prover. For example, when `"LfEucl → LfQuasiRefl"` is already established, we needn't attempt to prove `"RgEucl → RgQuasiRefl"` since this follows trivially by taking the converse relation. When a trivial proof or disproof of an implication is already known, we run neither the counter-example search nor the external theorem prover for it. All trivial proofs are printed to a log file during a program run; that output may subsequently be used to extract the trivial part of a proof tree of a given implication, by running program `justify`. As an example, Fig. 43 shows the proof tree for `"Trans ∧ Irrefl → ASym"` (base-27 code `ijrj`); it also demonstrates that trivial proofs needn't be intuitively obvious. Figure 44 shows the disproof tree of `"ASym ∧ Trans ↣ Refl"` (`clcn`); right to each base-27 code, the corresponding index triple is shown.

**Definition 25.** (*Trivial inference rules*) Using $I, J, K, I(·), \dots$ to denote default representations of lifted properties, our trivial inference rules are:

1. if $I \wedge J \rightarrow K$, then $J \wedge I \rightarrow K$;

2. if $J \wedge I \not\rightarrow K$, then $I \wedge J \not\rightarrow K$;

3. if $I \wedge J \rightarrow K$, and $H \wedge I \rightarrow J$, then $H \wedge I \rightarrow K$, and variants thereof;

4. if $H \wedge I \not\rightarrow K$, and $H \wedge I \rightarrow J$, then $I \wedge J \not\rightarrow K$, and variants thereof;

5. if $\forall R. I(R) \wedge J(R) \rightarrow K(R)$, then $\forall R, p. I(R^p) \wedge J(R^p) \rightarrow K(R^p)$;

6. if $\exists R, p. I(R^p) \wedge J(R^p) \not\rightarrow K(R^p)$ then $\exists R. I(R) \wedge J(R) \not\rightarrow K(R)$.

□

The above example trivial inference from `"LfEucl → LfQuasiRefl"` to `"RgEucl → RgQuasiRefl"` is achieved by applying rule 25.5 with $op = 5$.

In the last two rules, it does make sense to consider all lifted properties equivalent to a given one during the search for a common operation $op$. For example, from the implication $C-tr \wedge 3-rf \rightarrow C-as$ (`isok`), we may infer $A-tr \wedge 1-rf \rightarrow 8-as$ by equivalences, and then $3-tr \wedge 8-rf \rightarrow 1-as$ from rule 25.5 with $op = A$, which normalizes to the default representation $3-tr \wedge C-rf \rightarrow 3-as$ (`ijrj`); cf. the two topmost lines in the proof tree in Fig. 43.

Initially, we fill all array cells corresponding to trivial implications, including monotonicity information:

**Definition 26.** (*Trivial initialization rules*) Our trivial initialization rules are:

1. $x \wedge y \rightarrow true$,

2. $x \wedge false \rightarrow z$,

3. $false \wedge y \rightarrow z$,
<figure><img src="image_7.png" /><figcaption>Figure 11: Approach to find implications</figcaption></figure>

4. $x \wedge y \rightarrow x'$ if $x \rightarrow x'$ is known by monotonicity or antitonicity, and

5. $x \wedge y \rightarrow y'$ if $y \rightarrow y'$ is known, similarly. $\square$

For example, since ASym is antitonic, we initialize array cell [33] [3] [10], corresponding to “7-ASym $\wedge$ 2-Dense $\rightarrow$ 3-ASym” (k0ij), to true, by rule 26.4.

It turned out that no other than the above 6 inference rules are needed. For example, we don't need an extra “explosion” rule: if $I \wedge J \rightarrow false$ is known to hold, we can infer $I \wedge J \rightarrow K$ for an arbitrary lifted property K using an appropriate variant of rule 25.3 and the trivial implication $J \wedge false \rightarrow K$ from 26.2.

### 5.3. Finding implications

Figure 11 shows an overview of our architecture for searching for 3-implications. The array mentioned above is our central data structure. Various actions on it can be triggered by command-line options. We first perform the trivial initializations, then usually load results from previous runs, infer all possible trivial conclusions, and perform a proof/proof search for still undecided array cells. The latter action cycles through all undecided array cells, and runs the counter-example generator and (in case of not finding a counter-example) the external prover; once a decision has been found, trivial conclusions are drawn from it.

During the early runs, when most cells were yet undecided, we drew from each new information as much conclusions as possible, in order to prune generator and prover calls. Since this amounted to a depth-first search, it often lead to extremely long proofs.<fnref n="14" /> In

<footnote n="14">¹⁴ In Fig. 43 and 44 length-minimized proof trees of ijrj and clcn are shown. The corresponding depth-first versions have 13148 and 124989 nodes, even when their 3083 and 34310 repeated subtrees are counted as one node each, respectively.</footnote>
later runs, when we tried to optimize trivial proofs w.r.t. human readability, we did a
breadth-first search to obtain short proofs.

It took us a couple of program runs to prove or disprove every possible 3-implication.
Moreover, we modified details of our approach between successive runs.<fnref n="15" /> Using a save
/ load mechanism, we could reuse results from earlier runs.<fnref n="16" /> Consistency over varying
implementations is ensured as the notions of counter-example and external proof remained
unchanged.

We kept the log files of all external proof attempts. If an implication couldn't be
proven true immediately, we retried it with increased minimum domain cardinality, up
to 8. A domain cardinality of ≥ n was expressed by a first-order formula introducing
n constants c₁, ..., cₙ, and requiring their pairwise distinctness; for n = 1 we used the
formula ¬∀x>false. In Fig. 42, we noted any nontrivial minimum domain cardinality.

Whenever the external prover noted that an implication $I \wedge J \rightarrow K$ could be proven without using its conclusion $K$ (EProver outcome “contradictory axioms”), we validated that by manually calling the prover for $I \wedge J \rightarrow false$. Altogether, we collected log files of successful proof attempts of 4422 implications of the latter form, and 34727 other implications.

A few implications that couldn't be proven this way needed to be proven manually, viz. g0rw, uivk, uklu, uydr, voye, voyr, wfyp, see Sect. 5.8. All remaining implications were invalid; we provided counter examples on finite (Sect. 5.4) or countably infinite (Sect. 5.5) domains manually. Knowing about the validity / invalidity of every 3-implication is the basis to achieve completeness of our axiom set in Sect. 5.7 below.

5.4. Finite counter-examples

**Example 27. (Finite counter-examples)** The following implications are not universally valid:

1. (aiir) 9-AntiSym ∧ 2-Dense ⏝ 3-SemiOrd1

2. (qij0) 2-LfSerial ∧ 2-Dense ⏝ 2-Trans

3. (eiit) 1-SemiOrd1 ∧ 2-Dense ⏝ C-SemiOrd1

4. (g0ih) 2-SemiOrd2 ∧ 2-Dense ⏝ 9-Trans

5. (jijo) 3-Dense ∧ 2-Dense ⏝ 1-Dense

6. (qbvk) 1-LfSerial ∧ 3-AntiTrans ⏝ 6-AntiTrans

7. (qiiu) 2-LfSerial ∧ 2-Dense ⏝ 2-SemiOrd2

8. (r0jq) 4-LfSerial ∧ 4-Dense ⏝ 7-Dense

9. (reuu) 4-LfSerial ∧ 2-LfSerial ⏝ 2-SemiOrd2

10. (qism) 2-LfSerial ∧ 7-Trans ⏝ 8-AntiTrans

11. (qisr) 2-LfSerial ∧ 7-Trans ⏝ 8-Dense

12. (rg0u) 4-LfSerial ∧ 2-LfUnique ⏝ 2-SemiOrd2

13. (rgak) 4-LfSerial ∧ 2-LfUnique ⏝ 6-AntiTrans

<footnote n="15">¹⁵ For example, we originally recorded an implication as “presumably true” when no counter-example was found and no external proof was available. This turned out to be tedious to implement, and inferences from presumably true implications weren’t of great use; so we dropped this kind of truth value.</footnote>

<footnote n="16">¹⁶ Originally, we implemented saving and loading the complete array in binary format. However, we abandoned this approach in favor of a print / scan mechanism for lists of base-27 codes, since such files are easier to maintain.</footnote>
14. (rylq) 6-LfSerial ∧ 6-LfUnique ↛ 2-SemiOrd1

15. (rymo) 6-LfSerial ∧ 6-LfUnique ↛ 1-Dense

16. (xrkv) 3-LfQuasiRefl ∧ 4-Dense ↛ 7-LfQuasiRefl

PROOF. We show in Fig. 12 to 21 a counter-example relation on a finite domain<fnref n="17" /> for each of the implications. In each picture, an arrow from $x$ (light blunt end) to $y$ (dark peaked end) indicates $xRy$, colors have only didactic purpose. All properties have been machine-checked by our implementation. Additionally, we give a witness for each dissatisfied implication conclusion:

1. In Fig. 12, we have $bRa$, $a$ incomparable to itself, $aRd$, but not $bRd$. Hence, $R$ is not SemiOrd1.
Note that this relation is the same as in [1, Exm.76, p.49]; variations of this relation appear in the counter-examples for qij0, eiit, g0ih, qiiu, r0jq, reuu, and xrkv.

2. The same elements in this relation demonstrate that $R$ is not Trans, and hence not QuasiTrans, since $R$ coincides with $R^2$.

3. In Fig. 13, we have $bR^Cm$, $mR^1n$, and $nR^Cc$, but not $bR^Cc$.

4. In Fig. 14, we have $aR^9h$ and $hR^9b$, but not $aR^9b$.

5. The counter-example relation is obtained from Fig. 13 by removing the loops $mRm$ and $nRn$. We then have no intermediate element for $mR^1n$.

6. In Fig. 15, we have $aR^6b$ and $bR^6c$, but $aR^6c$.

7. In Fig. 16, we have $bR^2a$ and $aR^2c$, while $h$ is incomparable to each of $a, b, c$.

8. In the same figure, $R$ is not 7-Dense, since $aR^7n$ has no intermediate element.

9. In the same figure, $R$ is not 2-SemiOrd2, since $bR^2a$ and $aR^2c$, but $h$ is incomparable to all of them.

10. In Fig. 17, we have $xR^8y$, and $yR^8z$, but $xR^8z$.

11. In Fig. 18, $xR^8y$ has no intermediate element w.r.t. $R^8$: each element is comparable w.r.t. $R$ to $x$ or to $y$.

12. In Fig. 19, we have $x_1R^2y_1$ and $y_1R^2z_1$, but $x_2$ is comparable with none of them.

13. In the same figure, we have $x_1R^6y_1$ and $y_1R^6z_1$, but $x_1R^6z_1$, i.e. $R^6$ is not anti-transitive.

14. In Fig. 20, $aR^2b$, $b, c$ incomparable w.r.t. $R^2$, and $dR^2d$, but not $aR^2d$.

15. In the same figure, $bR^1c$ has no intermediate element.

16. In Fig. 21, we have $hR^7c$, but not $hR^7h$. □

<footnote n="17">¹⁷ The shown counter-examples might not be the simplest possible.</footnote>
<figure><img src="image_8.png" /><figcaption>Figure 12: Counter-example relation for *aiir* and *qij0*</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Figure 13: Counter-example relation for *eiit*</figcaption></figure>
<figure><img src="image_10.png" /><figcaption>Figure 14: Counter-example relation for g0ih</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Figure 15: Counter-example relation for qbvk</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>Figure 16: Counter-example relation for qiiu, r0jq, and reuu</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Figure 17: Counter-example relation for qism</figcaption></figure>
<figure><img src="image_14.png" /><figcaption>Figure 18: Counter-example relation for qisr</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>Figure 19: Counter-example relation for rg0u and rgak</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>Figure 20: Counter-example relation for rylq and rymo</figcaption></figure>

<figure><img src="image_17.png" /><figcaption>Figure 21: Counter-example relation for xrkv</figcaption></figure>
### 5.5. Infinite counter-examples

**Example 28. (Non-negative rational numbers)** The set $Q_+ = \{q \in Q \mid q \ge 0\}$ of non-negative rational numbers with the usual order ($<$) can be used to disprove the following implications:

1. (a0mz) 4-Dense $\wedge$ 9-AntiSym $\not\to$ 3-LfSerial,

2. (acib) 2-Dense $\wedge$ D-Trans $\not\to$ 3-Sym,

3. (afay) 2-Dense $\wedge$ 4-LfSerial $\not\to$ 2-LfSerial.

**PROOF.** We define $R = (<)$ to establish the usual notation. Since $R$ is asymmetric, $R^{2i}$ coincides with $R^{2i+1}$, for $i = 0, \dots, 7$. We therefore have $R^2 = R^3 = (<)$, $R^4 = (>)$, $R^9 = (=)$, and $R^D = (\ge)$. It is well known that ($<$) and ($>$) are dense, ($>$) is left-serial, ($=$) is trivially anti-symmetric, and ($\ge$) is transitive. However, ($<$) is neither left-serial (consider $x = 0$) nor symmetric. $\square$

**Example 29. (Integer numbers)** The set $\mathbb{Z}$ of integer numbers with the usual order ($<$) can be used to disprove the following implications:

1. (jeuc) D-Trans $\wedge$ 2-LfSerial $\not\to$ 2-Dense,

2. (jeux) D-Trans $\wedge$ 2-LfSerial $\not\to$ 2-AntiTrans.

**PROOF.** As in Exm. 28, we write $R$ for ($<$), and observe $R^2 = (<)$ and $R^D = (\ge)$. The former is left-serial, and the latter is transitive. However, ($<$) is neither dense nor anti-transitive. $\square$

**Example 30. (aaje)** 2-Dense and 3-AntiSym doesn't imply C-Dense.

**PROOF.** Consider $Q \cup \{\infty\}$ with $R$ being the usual order ($\le$) on $Q$, extended by $xR\infty$ for all $x \in Q \cup \{\infty\} \setminus \{0\}$. We have that $R$ is anti-symmetric, since it is so on $Q$, and $\infty Rx$ doesn't hold, except for $x = \infty$. $R^2$ is ($<$) $\cup$ $\{\langle x, \infty\rangle \mid 0 \neq x \neq \infty\}$, which is dense: observe that $Q \setminus \{-1\} \ni xR^2\infty$ has e.g. $x+1$ as intermediate element, similar for $x = -1$. But $R^C$ is not dense, since $0R^C\infty$ has no intermediate element, as $xR^C\infty$ implies $x = 0$, but neither $0R^C0$ nor $\infty R^C\infty$ holds. $\square$

**Example 31. (aaxu)** 2-Dense and 2-SemiOrd1 doesn't imply 2-SemiOrd2.

**PROOF.** Consider $Q \cup \{\infty\}$ with $R$ being the usual order ($<$), and with $\infty$ incomparable to all elements. Since this ordering is asymmetric, $R^2$ coincides with $R$. Hence, it is dense, since it is dense on $Q$, and $\infty$ is not involved in any relation pair. Moreover, $R$ satisfies semi-order property 1, since $xR^8y \wedge yRz$ can hold only if $x = y \neq \infty$; in this case, $wRx$ implies $wRz$ by transitivity. But $R$ doesn't satisfy semi-order property 2, since $0 < 1 < 2$, but $\infty$ is incomparable to all of them. $\square$

**Example 32. (i0iq)** 2-Trans and 2-Dense doesn't imply 2-SemiOrd1.
<figure><img src="image_18.png" /><figcaption>Figure 22: Relation in Exm. 34</figcaption></figure>

**PROOF.** Consider {$a, b$} × $\mathcal{Q}$ with $R$ defined by $\langle x, y \rangle R \langle u, v \rangle$ iff $x = u$ and $y < v$, employing the usual order <. This results in two independent copies of the rational numbers $\mathcal{Q}$. Since this ordering is asymmetric, 2-Trans coincides with 3-Trans; both properties are well-known to be satisfied by <. Since no elements of different copies of $\mathcal{Q}$ are related, $R$ itself is also both 2- and 3-Transitive, and moreover 2-Dense. However, $R^2$ doesn't satisfy semi-order property 1, since $\langle a, 0 \rangle R^2 \langle a, 1 \rangle$, and $\langle a, 1 \rangle$ is incomparable w.r.t. $r^2$ to $\langle b, 0 \rangle$, and $\langle b, 0 \rangle R^2 \langle b, 1 \rangle$, but not $\langle a, 0 \rangle R^2 \langle b, 1 \rangle$. $\square$

**Example 33.** (*jevo*, *jew0*) D-Trans and 2-LfSerial implies neither 1-Dense (*jevo*) nor 4-LfSerial (*jew0*).

**PROOF.** Consider the set $\mathcal{N}$ with $xRy$ defined as $x > y$ or $x = 0 \wedge y = 1$. Then $R^2$ is left serial, since e.g. $x + 1R^2x$ for $x > 0$ and $2R^20$. The relation $R^D$ can be obtained as $(R^5) \cup (R^8)$; with $xR^5y$ iff $x < y$ or $x = 1 \wedge y = 0$, and $xR^8y$ iff $x = y$; hence $xR^Dy$ iff $x \le y$ or $x = 1 \wedge y = 0$. Therefore, $R^D$ is transitive: Let $xR^Dy$ and $yR^Dz$.

* If $x \le y$ and $y \le z$, then $x \le z$, hence $xR^Dz$.

* If $x \le y$ and $y = 1 \wedge z = 0$, then $x = 0$ or $x = 1$, in both cases, $xR^D0$ holds.

* If $x = 1 \wedge y = 0$ and $y \le z$ and $z = 0$, then $1R^D0$ holds.

* If $x = 1 \wedge y = 0$ and $y \le z$ and $z > 0$, then $1 \le z$, hence $xR^Dz$.

* The case $x = 1 \wedge y = 0$ and $y = 1 \wedge z = 0$ is a contradiction.

However, $R^1 = \{\langle 0, 1 \rangle, \langle 1, 0 \rangle\}$ is not dense. Moreover, $R^4$ is not left serial, i.e. $R^2$ is not right serial, since $0R^2x$ applies to no $x$. $\square$

**Example 34.** (*qjxu*) 2-LfSerial and 2-SemiOrd1 doesn't imply 2-SemiOrd2.

**PROOF.** Consider the universe set $\mathcal{N}$ and its usual order ($>$), define $R = (>) \setminus \{\langle 1, 0 \rangle, \langle 2, 0 \rangle, \langle 3, 0 \rangle\}$, cf. Fig. 22. Since ($>$), and therefore $R$, is asymmetric, it coincides with $R^2$. The latter is left serial since e.g. $i + 1R^2i$ for each $i \ge 1$, and $4R^20$.

$R^2$ also satisfies semi-order property 1: Let $wR^2x$, $x, y$ incomparable w.r.t. $R^2$, and $yR^2z$.

* If $x = y$ and $z > 0$,
  then $w > x = y > z > 0$, i.e. 0 is not involved, hence $wR^2z$ by transitivity of ($>$).

* If $x = y$ and $z = 0$, then $w > x = y \ge 4 > 0 = z$, hence again $wR^2z$ by transitivity.
<figure><img src="image_19.png" /><figcaption>Figure 23: Relation in Exm. 35</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>Figure 24: Relation in Exm. 36</figcaption></figure>

• The case $x \in \{1, 2, 3\}$ and $y = 0$ is impossible due to $yR^2z$.

• If $x = 0$ and $y \in \{1, 2, 3\}$, then $yR^2z$ implies $3 \ge y > z > 0$, and $wR^20$ implies $w \ge 4$, hence $wR^2z$.

However, $R^2$ doesn't satisfy semi-order property 2, since 0 is incomparable to all elements involved in $3R^22R^21$. $\square$

**Example 35.** (qlas) 2-LfSerial and 2-Trans doesn't imply E-Dense.

**PROOF.** Consider the universe set $\{a, b\} \times IN$, and the relation $R$ defined by $\langle x, y \rangle R \langle u, v \rangle$ iff $x = u \wedge y > v$ or $y = 0 \wedge v \ne 0$ or $y \ne 0 \wedge v = 0$. Figure 23 sketches the relation: it consists of two copies of $\langle \rangle$ on $IN$, but additionally relates each zero to each non-zero universe member, and vice versa. We have $\langle x, y \rangle R^2 \langle u, v \rangle$ iff $x = u \wedge y > v > 0$; this relation is ls and tr. $R$ is not E-de since $\langle a, 0 \rangle R^E \langle b, 0 \rangle$ has no intermediate element by construction. $\square$

**Example 36.** (qldr) 2-LfSerial and 3-Trans doesn't imply 8-Dense.

**PROOF.** On the set $\{a, b\} \times IN$, define $R'$ such that for all $x, y, u$:

1. $\langle x, y+1 \rangle R' \langle x, y \rangle$,

2. $\langle x, 1 \rangle R' \langle u, 0 \rangle$,

3. $\langle x, 0 \rangle R' \langle x, 0 \rangle$,

4. $R'$ applies to no other pairs than given above.

Figure 24 sketches that relation; it is left serial due to rule 1. Let $R$ be the transitive closure of $R'$, then $R$ is transitive by construction. $R^2$ is obtained from $R$ by removing the pairs $\langle\langle a, 0 \rangle\rangle$, $\langle\langle a, 0 \rangle\rangle$ and $\langle\langle b, 0 \rangle\rangle$, $\langle\langle b, 0 \rangle\rangle$; it is left serial, since $R'$ is. However, $R^8$ is not dense: $\langle a, 0 \rangle R^8 \langle b, 0 \rangle$ has no intermediate element, since $\langle a, 0 \rangle$ is comparable w.r.t. $R$ to each element except $\langle b, 0 \rangle$, and similar for $\langle b, 0 \rangle$. $\square$
<figure><img src="image_21.png" /><figcaption>Figure 25: Relation in Exm. 37</figcaption></figure>

<figure><img src="image_22.png" /><figcaption>Figure 26: Relation in Exm. 39</figcaption></figure>

**Example 37.** (*qmkh*) 2-LfSerial and 7-AntiTrans doesn't imply 1-LfUnique.

**PROOF.** Consider the universe set {$a, b, c$} × $\mathcal{N}$, and the relation $R$ defined as follows: $\langle x, y \rangle R \langle u, v \rangle$ iff $x = u \land y = v + 1$ or $y = v = 0 \land x \neq u \land b \in \{x, u\}$. The universe consists of three copies of $\mathcal{N}$, connected only at 0; see Fig. 25. The relation $R$ is 2-LfSerial, since $\langle x, i + 1 \rangle R \langle x, i \rangle$, but not $\langle x, i \rangle R \langle x, i + 1 \rangle$ for each $x \in \{a, b, c\}$ and $i \in \mathcal{N}$. It is 7-AntiTrans, since it doesn't contain an undirected cycle of length 3. In fact, the only cycles are $\langle b, 0 \rangle R \langle a, 0 \rangle R \langle b, 0 \rangle$ and $\langle b, 0 \rangle R \langle c, 0 \rangle R \langle b, 0 \rangle$, and compositions thereof, all of which have an even length. However, it is not 1-LfUnique, since $\langle b, 0 \rangle R^1 \langle a, 0 \rangle$ and $\langle b, 0 \rangle R^1 \langle c, 0 \rangle$. $\square$

**Example 38.** (*qpkw*) 2-LfSerial and 5-LfUnique doesn't imply 8-LfQuasiRefl.

**PROOF.** Consider the set $\mathcal{N}$ with $xRy$ defined as $x = y + 1$ or $x = y = 0$. Then $R^2$ is left serial, since $x + 1R^2x$ for all $x$. Moreover, $R$ is right-unique, since a successor number $y+1$ is related only to $y$, and 0 is only related to 0. However, $R^8$ is not left quasi-reflexive, since e.g. $0R^82$, but not $0R^80$. $\square$

**Example 39.** (*ufbk*) 2-LfUnique and 4-LfSerial does not imply 4-LfUnique

**PROOF.** Consider $\mathcal{N} \setminus \{0\}$ and the relation $xRy :\Leftrightarrow x = y \parallel 2$, where $\parallel$ denotes truncating integer division, see Fig. 26. It is 2-LfUnique, since $x_1 = y \parallel 2 = x_2$ implies $x_1 = x_2$. It is 4-LfSerial, since for a given $y$, choosing $x = y \cdot 2$ will satisfy $x \neq y \parallel 2$ and $y = x \parallel 2$, that is, $xR^4y$. However, it is not 4-LfUnique, since e.g. $1 = 2 \parallel 2$ and $1 = 3 \parallel 2$, that is, $2R^41$ and $3R^41$. $\square$

**Example 40.** (*uo0e*) 3-LfUnique and 4-LfSerial doesn't imply 1-Trans.
<figure><img src="image_23.png" /><figcaption>Figure 27: Relation in Exm. 40</figcaption></figure>

PROOF. On the set $\{a, b\} \times \mathbb{N}$, define $R$ such that:

1. $\langle x, y \rangle R \langle x, y+1 \rangle$,

2. $\langle x, 0 \rangle R \langle u, 0 \rangle$ if $x \neq u$,

3. $R$ applies to no other pairs than given above.

Figure 27 sketches $R$ and allows us to verify that $R$ is left-unique (no two arrows end at the same point) and $R^4$ is left serial (a one-sided arrow starts from each point). However, $R^1$ is not transitive, since $\langle a, 0 \rangle R^1 \langle b, 0 \rangle$, and $\langle b, 0 \rangle R^1 \langle a, 0 \rangle$, but not $\langle a, 0 \rangle R^1 \langle a, 0 \rangle$. $\square$

5.6. *Reported laws*

After several attempts, we eventually achieved to decide for every 3-implication its
truth value. We found 156384 valid and 375057 invalid implications; the former include
42657 from trivial initialization.

In the ancillary file lpImpl.log each implication can be found together with its truth
value and a justification. The executable justify can be used to obtain the truth values
(and justifications) of given implications. Figure 43 and 44 show examples; note that
we don't print proof parts contributed by the external prover or the counter-example
generator.

Implications with one antecedent<fnref n="18" /> can be visualized as a directed graph (Hasse dia-
gram), with lifted properties as vertices and implications as edges. This has been done
for basic properties in [1, Fig.18, p.20]. For lifted properties, the graph is still too large
to be depicted in one piece. We have split it by basic property and show the pieces in
Fig. 28 to 38. In each figure, vertices and edges for the depicted basic property are shown
in blue, while others, for implied or implying properties, are shown in red. We have two
exceptions: edges contained in our minimal axiom set (Sect. 5.7 below) are colored green,
and edges following from monotonicity or antitonicity are colored cyan (for the depicted
basic property) or magenta (for others). For brevity, the two-character codes from Def. 1
are used, and the separating hyphen between operation and property name is omitted.
For example, the bottommost vertex in Fig. 28 represents the lifted property 9-AntiSym.
Since the vertices represent equivalence classes, all implications are strict.

Figure 39 summarizes the part about all basic properties; co-transitivity is included
(as “Ctr”) although we didn’t define it as a basic property. In this figure, in order to
obtain a feasible complexity, a red vertex is shown only if it is both implied by a blue
vertex and implying another one.

<footnote n="18">¹⁸ in our approach, they appear as 3-implications of the form e.g. $I \wedge I \rightarrow K$</footnote>
<figure><img src="image_24.png" /><figcaption>Figure 28: Implications about anti-symmetry (an)</figcaption></figure>

Figure 40 shows the inconsistencies<fnref n="19" /> between lifted properties. Clusters of incompatibilities are presented using disjunctions of lifted properties. For example, the topmost horizontal red edge, from “Alu,Clu,Cat” to “1at,1lu”, indicates that each property from the set {A-LfUnique, C-LfUnique, C-AntiTrans} is inconsistent with each property from {1-AntiTrans, 1-LfUnique}. Nested boxes indicate implications between properties, that is, subset relations between their extensions. For example, the “as” box is inside the “1at” box since each ASym relation is 1-AntiTrans (cjdj). The red lines’ end points should be considered carefully; for example, the topmost vertical line connects “1ls” with “as” but not with the surrounding “1at” box, since 1-LfSerial is inconsistent with ASym, but not necessarily with 1-AntiTrans. All found inconsistencies are covered in Fig. 40; however, some of them require application of some implications, viz.

<figure><img src="image_25.png" /></figure>

For example, the inconsistency of SemiConnex and CoRefl known from [1, Lem.8.8, p.23] is tacitly understood as a consequence of the inconsistency of 1-LfUnique and 7-LfUnique shown at the bottom of Fig. 40.

Together, Fig. 28 to 40 show a refinement of the graph from [1, Fig.18, p.20].

<footnote n="19">¹⁹ i.e. 3-implications of the form $I \wedge J \rightarrow 0$-Refl</footnote>
<figure><img src="image_26.png" /><figcaption>Figure 29: Implications about anti-transitivity (at)</figcaption></figure>

<figure><img src="image_27.png" /><figcaption>Figure 30: Implications about density (de)</figcaption></figure>
<figure><img src="image_28.png" /><figcaption>Figure 31: Implications about left Euclideanness (le)</figcaption></figure>

<figure><img src="image_29.png" /><figcaption>Figure 32: Implications about left quasi-reflexivity (lq)</figcaption></figure>
<figure><img src="image_30.png" /><figcaption>Figure 33: Implications about left seriality (ls)</figcaption></figure>

<figure><img src="image_31.png" /><figcaption>Figure 34: Implications about left uniqueness (lu)</figcaption></figure>
<figure><img src="image_32.png" /><figcaption>Figure 35: Implications about semi-order property 1 (s1)</figcaption></figure>

<figure><img src="image_33.png" /><figcaption>Figure 36: Implications about semi-order property 2 (s2)</figcaption></figure>
<figure><img src="image_34.png" /><figcaption>Figure 37: Implications about transitivity (tr)</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>Figure 38: Implications about symmetry (sy), asymmetry (as), and reflexivity (rf)</figcaption></figure>
<figure><img src="image_36.png" /><figcaption>Figure 39: Implications about basic properties</figcaption></figure>
<figure><img src="image_37.png" /><figcaption>Figure 40: Inconsistencies between lifted properties</figcaption></figure>
<figure><img src="image_38.png" /><figcaption>Figure 41: Proof sketch in Lem. 42 (lf)</figcaption></figure>

Order-based axiom set computation (rg)

### 5.7. Axiom set

In order to obtain a human-comprehensible result, we searched for a small set of “axioms” from which all valid 3-implications could be derived by trivial inferences in the sense of Sect. 5.2. Our approach is described in an abstract way by Def. 41 and Lem. 42.

**Definition 41. (Abstract derivation)** Let $U$ (“universe”) be a set of “abstract propositions”. An abstract inference rule $r$ on $U$ is a partial mapping from finite subsets of $U$ to $U$. If $r(X)$ is defined for a finite $X \subseteq U$, we say that $r(X)$ is directly derivable from $X$.

We say that $p$ is derivable from a set $Y$ if an abstract derivation tree exists with $p$ at its root and members of $Y$ as its leaves such that each non-leaf node corresponds to a valid direct derivation. The set $Y$ needn't be finite, and not each of its members need to appear as a leaf. We will assume a fixed given set of inference rules in the following.

Moreover, let a fixed well-founded total order $<$ on $U$ be given. We say a derivation tree is ordered if every of its nodes is larger than all its (direct) descendants; we call its root orderly derivable from the set of its leaves. $\square$

**Lemma 42. (Axiomatization)** Let $V$ (“valid”) be a set of propositions; let $K$ (“kernel”) be a subset of $V$ such that each member of $V$ can be derived from $K$. Let $A$ (“axioms”) be the set of propositions $k \in K$ such that $k$ is not orderly derivable from $K \setminus \{k\}$. Then:

1. $A$ is a subset of $K$;

2. Each member of $V$ is derivable already from $A$;

3. No member $a$ of $A$ is orderly derivable from $A \setminus \{a\}$.

**PROOF.** We first show, by induction on $ (<) $, that each $ k \in K $ is orderly derivable from $ A $: If $ k $ is not orderly derivable from $ K \setminus \{k\} $, the $ k \in A $ by construction, and we are done (trivial one-node derivation tree). Else, let $ k $ be orderly derivable from $ \{k_1, \dots, k_n\} \subseteq K \setminus \{k\} $ (red tree in the left part of Fig. 41). Then $ k_i < k $, and hence by I.H. $ k_i $ is orderly derivable from $ A $ (green tree). Composing the tree to derive $ k $ from $ \{k_1, \dots, k_n\} $ with the trees for all $ k_i $ gives an ordered derivation tree for $ k $ from $ A $.

Now we show the claimed properties:

1. By construction of $ A $.
2. If $v \in V$, then $v$ has a derivation tree with leaves in $K$ by assumption. Each of its leaves has an (even ordered) derivation tree from $A$. Composing the trees appropriately yields a derivation tree for $v$ from $A$ (note that it needn't be ordered).

3. If $a \in A$ was orderly derivable from $A \setminus \{a\}$, then it was also orderly derivable from the superset $K \setminus \{a\}$, contradicting the construction of $A$.
Note, however, that some $a \in A$ may still be unordered derivable from larger members of $A$. $\square$

Figure 41 (rg) shows a geometrical analogy of this approach of order-based axiom set computation. A member of the set $V$ is represented by 3 adjacent circles in different colors (red, green, blue). Each color corresponds to an own proof ordering. A colored arrow indicates an ordered derivation; for simplicity we assume each inference rule to work on a singleton set. A full circle indicates an axiom w.r.t. the proof order of its color; a hollow circle represents a non-axiom. The proof order shown in red, green, and blue, needs 3, 6, and 6 axioms, respectively. Note that the set of red axioms can be further reduced by applying, in turn, e.g. the green order to it.

In our implementation, an abstract proposition consists of a valid or invalid 3-implication, like "C-Refl ∧ 3-Trans → 3-ASym" and "3-Trans ∧ 3-Trans ⇝ 3-Sym" (eccj and ilcb, respectively). We represented such a proposition by its base-27 code, using different permutations of character positions. For example, the implications "3-Trans ∧ C-Refl → 3-ASym" and "3-SemiOrd1 ∧ 3-Refl → C-ASym" correspond to ijrj and faok, respectively; so a derivation of the former from the latter is unordered w.r.t. the identity permutation, but orderly when comparing the reverse codes (jrji and koaf). Applying xor masks to the characters before comparing, we obtain more possible orderings. In order to obtain best-comprehensible axioms, we prepended symbol encoding the "human simplicity" of an implication.<fnref n="20" />

We used an ad hoc evolutionary algorithm based on Lem. 42 to minimize the cardinality of the axiom set as far as we could. Starting from the set of all 34727 proven implications, we applied Lem. 42 in parallel for a couple of different orderings. One of them resulted in a set of 360 axioms, the minimum number we could achieve. Repeating that procedure 5 times, we obtained axiom sets comprising 285, 265, 256, 253, and 252 axioms. After that we manually tried to omit axioms one by one, and ended up with a set of 124 axioms.

Subsequently, we manually exchanged a few axioms by equivalent ones for presentation reasons. For example, we replaced "Refl → LfQuasiRefl" (dsqt) by "Refl → QuasiRefl" (dsqv), to get a nicer Hasse diagram in Fig. 39; in the presence of the remaining 123 axioms, both are equivalent. Similarly, we replaced right by left properties where possible, e.g. "RgEucl → QuasiTrans" (pej0) by the equivalent "LfEucl → QuasiTrans" (owg0).

The result is shown in Fig. 42; each valid 3-implication can be inferred from these axioms using the trivial inference rules from Sect. 5.2 (Thm. 56).

In Fig. 42, we marked implications where all atoms share the same basic property. We used "*" when this can be obtained by applying just the redundancies from Fig. 8, and "+" when equivalences from Fig. 9 are needed in addition; for example, the top left implication "IncTrans → SemiOrd2" can be rephrased as "7-SemiOrd2 → SemiOrd2".

<footnote n="20">²⁰ For example, the list "Refl ∧ LfEucl → 1-RgSerial", "Refl → 1-RgSerial", "Refl → RgSerial", "Refl → LfSerial" is ordered from worst to best simplicity.</footnote>
When a minimum cardinality is required for an implication, we noted it in the same column; for example, the last axiom, **wfzb**, can be falsified on a 2-element set, but is valid for all relation domains of $≥ 3$ elements.

Moreover, we marked axioms for which some kind of converse also holds. An axiom $I \wedge J \rightarrow K$ is marked “=” if also $K \rightarrow I \wedge J$ holds; it is marked “>” if also $K \rightarrow J$ holds, and “>” if also $I \wedge K \rightarrow J$ holds. The axioms could be manually tuned such that the cases $J \wedge K \rightarrow I$ and $K \rightarrow I$ don't occur. Note that the reverse or semi-reverse versions are not part of the axiomatization; for example, the bottom right axiom “ASym $\wedge$ Dense $\rightarrow$ 2-Dense” (**cllc**) is marked “>” since ASym and 2-Dense also implies Dense (**cijd**), but the latter can be proved from axioms **adsd**, **cixg**, **cpbj**, **dcaa**, **owht**, **pgrm**, and **xzgd**.

Figure 42 shows the 20 “2-implication laws” first, then the single “2-inconsistency law” **hpr0**, then the 103 proper “3-implication laws”. We additionally grouped implications by the basic/lifted distinctions of their atoms.

As for invalid implications, we minimized the set of implications obtained from finite (Sect. 5.4) and infinite (Sect. 5.5) counter-examples by manual ad-hoc removals; we didn't apply Lem. 42 for them, and we didn't try to minimize the set of computer-generated counter-examples. 17 implications were falsified by examples on an infinite domain, 133 on a 5-element domain (computer-generated), and 16 on another finite domain.

## 5.8. Some proofs of axioms

All axioms from Fig. 42 could be proven by EProver, except **g0rw**, **uivk**, **uklu**, **uydr**, **voye**, **voyr**, and **wfyp**. In this section, we give manual proofs for these and a few other axioms. Moreover, we include references to all proofs of axioms that were already given in [1].

**Lemma 43. (2-Implications group 0)**

1. (biuv) IncTrans $\rightarrow$ SemiOrd2

2. (dsqv) Refl $\rightarrow$ 7-LfQuasiRefl

3. (ild0) Trans $\rightarrow$ QuasiTrans

4. (owg0) LfEucl $\rightarrow$ QuasiTrans

5. (owht) LfEucl $\rightarrow$ LfQuasiRefl

6. (xzgd) LfQuasiRefl $\rightarrow$ Dense

7. (yqnt) QuasiRefl $\rightarrow$ LfQuasiRefl

**PROOF.** 1. See [1, Lem.34, p.31].

2. Since Refl implies QuasiRefl by [1, Lem.9, p.23]; the latter is equivalent to 7-LfQuasiRefl by Lem. 14.5.

3. See [1, Lem.18, p.27].

4. See [1, Lem.40, p.34].

5. See [1, Lem.46, p.37].

6. See [1, Lem.48.3, p.38].

7. By Def. 1.6. □

**Lemma 44. (2-Implications group 1)**

1. (dspx) Refl $\rightarrow$ 1-LfSerial
<table><caption>Figure 42: Minimal axiom set</caption>
  <tbody>
    <tr>
      <td>biuv +</td>
      <td>it →</td>
      <td>s2</td>
    </tr>
    <tr>
      <td>dsqv</td>
      <td>rf →</td>
      <td>qr</td>
    </tr>
    <tr>
      <td>ild0 *</td>
      <td>tr →</td>
      <td>qt</td>
    </tr>
    <tr>
      <td>owht</td>
      <td>le →</td>
      <td>lq</td>
    </tr>
    <tr>
      <td>owg0</td>
      <td>le →</td>
      <td>qt</td>
    </tr>
    <tr>
      <td>xzgd</td>
      <td>lq →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>yqnt *</td>
      <td>qr →</td>
      <td>lq</td>
    </tr>
    <tr>
      <td>dspx</td>
      <td>rf →</td>
      <td>1-ls</td>
    </tr>
    <tr>
      <td>fbao</td>
      <td>s1 →</td>
      <td>1-de</td>
    </tr>
    <tr>
      <td>fbar</td>
      <td>s1 →</td>
      <td>8-de</td>
    </tr>
    <tr>
      <td>gknw</td>
      <td>s2 →</td>
      <td>8-lq</td>
    </tr>
    <tr>
      <td>ilce *</td>
      <td>tr →</td>
      <td>1-tr</td>
    </tr>
    <tr>
      <td>jlmq *</td>
      <td>de →</td>
      <td>7-de</td>
    </tr>
    <tr>
      <td>owgk</td>
      <td>le →</td>
      <td>6-at</td>
    </tr>
    <tr>
      <td>xzhs *</td>
      <td>lq →</td>
      <td>1-lq</td>
    </tr>
    <tr>
      <td>fkdd</td>
      <td>7-s1 →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>lmco</td>
      <td>1-at →</td>
      <td>ir</td>
    </tr>
    <tr>
      <td>pwog +</td>
      <td>C-le →</td>
      <td>it</td>
    </tr>
    <tr>
      <td>vpm0</td>
      <td>6-lu →</td>
      <td>qt</td>
    </tr>
    <tr>
      <td>fkdo</td>
      <td>7-s1 →</td>
      <td>1-de</td>
    </tr>
    <tr>
      <td>hpr0 4</td>
      <td>8-lu →</td>
      <td>¬at</td>
    </tr>
    <tr>
      <td>0udt ></td>
      <td>sy</td>
      <td>tr →</td>
      <td>le</td>
    </tr>
    <tr>
      <td>d0gh +=</td>
      <td>an</td>
      <td>sy →</td>
      <td>cr</td>
    </tr>
    <tr>
      <td>dcaa ▷</td>
      <td>an</td>
      <td>qt →</td>
      <td>tr</td>
    </tr>
    <tr>
      <td>faok =</td>
      <td>s1</td>
      <td>rf →</td>
      <td>co</td>
    </tr>
    <tr>
      <td>hlmf =</td>
      <td>at</td>
      <td>de →</td>
      <td>em</td>
    </tr>
    <tr>
      <td>ikuv</td>
      <td>tr</td>
      <td>at →</td>
      <td>s2</td>
    </tr>
    <tr>
      <td>oskj ></td>
      <td>le</td>
      <td>an →</td>
      <td>lu</td>
    </tr>
    <tr>
      <td>phfb ></td>
      <td>re</td>
      <td>lq →</td>
      <td>sy</td>
    </tr>
    <tr>
      <td>ujry ▷</td>
      <td>lu</td>
      <td>ir →</td>
      <td>at</td>
    </tr>
    <tr>
      <td>ukaa</td>
      <td>lu</td>
      <td>s1 →</td>
      <td>tr</td>
    </tr>
    <tr>
      <td>ulmt ▷</td>
      <td>lu</td>
      <td>de →</td>
      <td>le</td>
    </tr>
    <tr>
      <td>xtlr</td>
      <td>lq</td>
      <td>s2 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>xxcn =</td>
      <td>lq</td>
      <td>rs →</td>
      <td>rf</td>
    </tr>
    <tr>
      <td>xzkv *=</td>
      <td>lq</td>
      <td>rq →</td>
      <td>qr</td>
    </tr>
    <tr>
      <td>0t0p +&gt;</td>
      <td>sy</td>
      <td>s1 →</td>
      <td>1-s1</td>
    </tr>
    <tr>
      <td>0ucf +&gt;</td>
      <td>sy</td>
      <td>tr →</td>
      <td>7-tr</td>
    </tr>
    <tr>
      <td>0wyx ▷</td>
      <td>sy</td>
      <td>ls →</td>
      <td>1-ls</td>
    </tr>
    <tr>
      <td>0yen ▷</td>
      <td>sy</td>
      <td>lu →</td>
      <td>7-lu</td>
    </tr>
    <tr>
      <td>bldc *</td>
      <td>it</td>
      <td>tr →</td>
      <td>D-tr</td>
    </tr>
    <tr>
      <td>cllc ></td>
      <td>as</td>
      <td>de →</td>
      <td>2-de</td>
    </tr>
  </tbody>
</table>
<table>
  <tbody>
    <tr>
      <td>cnyy ▷</td>
      <td>as</td>
      <td>ls →</td>
      <td>2-ls</td>
    </tr>
    <tr>
      <td>djid *=</td>
      <td>sc</td>
      <td>an →</td>
      <td>9-an</td>
    </tr>
    <tr>
      <td>ik0q</td>
      <td>tr</td>
      <td>s1 →</td>
      <td>2-s1</td>
    </tr>
    <tr>
      <td>ikvl ▷</td>
      <td>tr</td>
      <td>at →</td>
      <td>7-at</td>
    </tr>
    <tr>
      <td>ot0q</td>
      <td>le</td>
      <td>s1 →</td>
      <td>2-s1</td>
    </tr>
    <tr>
      <td>qtaq</td>
      <td>ls</td>
      <td>s1 →</td>
      <td>7-de</td>
    </tr>
    <tr>
      <td>qudq</td>
      <td>ls</td>
      <td>tr →</td>
      <td>7-de</td>
    </tr>
    <tr>
      <td>uivk 4</td>
      <td>lu</td>
      <td>it →</td>
      <td>6-at</td>
    </tr>
    <tr>
      <td>uklu 5</td>
      <td>lu</td>
      <td>s2 →</td>
      <td>2-s2</td>
    </tr>
    <tr>
      <td>uodr 3</td>
      <td>lu</td>
      <td>rs →</td>
      <td>8-de</td>
    </tr>
    <tr>
      <td>uoed 2</td>
      <td>lu</td>
      <td>rs →</td>
      <td>8-ls</td>
    </tr>
    <tr>
      <td>xt0s</td>
      <td>lq</td>
      <td>s1 →</td>
      <td>7-s1</td>
    </tr>
    <tr>
      <td>0vcy ▷</td>
      <td>sy</td>
      <td>1-at →</td>
      <td>at</td>
    </tr>
    <tr>
      <td>0vyd ▷</td>
      <td>sy</td>
      <td>7-de →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>0xjz ▷</td>
      <td>sy</td>
      <td>7-ls →</td>
      <td>ls</td>
    </tr>
    <tr>
      <td>0xzj ▷</td>
      <td>sy</td>
      <td>1-lu →</td>
      <td>lu</td>
    </tr>
    <tr>
      <td>0zet + ▷</td>
      <td>sy</td>
      <td>1-lq →</td>
      <td>lq</td>
    </tr>
    <tr>
      <td>cpbj ></td>
      <td>as</td>
      <td>2-lu →</td>
      <td>lu</td>
    </tr>
    <tr>
      <td>cixg ></td>
      <td>as</td>
      <td>9-tr →</td>
      <td>it</td>
    </tr>
    <tr>
      <td>ckry ▷</td>
      <td>as</td>
      <td>2-at →</td>
      <td>at</td>
    </tr>
    <tr>
      <td>ikcr</td>
      <td>tr</td>
      <td>7-s1 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>otcr ></td>
      <td>le</td>
      <td>7-s1 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>pgrm 3 ▷</td>
      <td>re</td>
      <td>8-lu →</td>
      <td>sc</td>
    </tr>
    <tr>
      <td>ulfl 3</td>
      <td>lu</td>
      <td>C-tr →</td>
      <td>an</td>
    </tr>
    <tr>
      <td>umxl</td>
      <td>lu</td>
      <td>7-de →</td>
      <td>an</td>
    </tr>
    <tr>
      <td>unrb</td>
      <td>lu</td>
      <td>1-ls →</td>
      <td>sy</td>
    </tr>
    <tr>
      <td>unuj</td>
      <td>lu</td>
      <td>2-ls →</td>
      <td>as</td>
    </tr>
    <tr>
      <td>xtg0</td>
      <td>lq</td>
      <td>C-s1 →</td>
      <td>qt</td>
    </tr>
    <tr>
      <td>xxjz ▷</td>
      <td>lq</td>
      <td>7-ls →</td>
      <td>ls</td>
    </tr>
    <tr>
      <td>xzog ▷</td>
      <td>lq</td>
      <td>8-lq →</td>
      <td>it</td>
    </tr>
    <tr>
      <td>ykcr ></td>
      <td>qr</td>
      <td>7-s1 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>bioh *</td>
      <td>it</td>
      <td>1-tr →</td>
      <td>9-tr</td>
    </tr>
    <tr>
      <td>cmyp ></td>
      <td>as</td>
      <td>7-de →</td>
      <td>6-de</td>
    </tr>
    <tr>
      <td>cokb ▷</td>
      <td>as</td>
      <td>7-ls →</td>
      <td>6-ls</td>
    </tr>
    <tr>
      <td>cpnn ▷</td>
      <td>as</td>
      <td>6-lu →</td>
      <td>7-lu</td>
    </tr>
    <tr>
      <td>ioas</td>
      <td>tr</td>
      <td>4-ls →</td>
      <td>E-de</td>
    </tr>
    <tr>
      <td>jljo</td>
      <td>de</td>
      <td>D-tr →</td>
      <td>1-de</td>
    </tr>
    <tr>
      <td>otfp ></td>
      <td>le</td>
      <td>C-s1 →</td>
      <td>1-s1</td>
    </tr>
    <tr>
      <td>owae</td>
      <td>le</td>
      <td>8-de →</td>
      <td>C-de</td>
    </tr>
    <tr>
      <td>uiyr 3</td>
      <td>lu</td>
      <td>9-tr →</td>
      <td>8-de</td>
    </tr>
    <tr>
      <td>ukfp</td>
      <td>lu</td>
      <td>C-s1 →</td>
      <td>1-s1</td>
    </tr>
  </tbody>
</table>
<table>
  <tbody>
    <tr>
      <td>unae</td>
      <td>lu</td>
      <td>8-de →</td>
      <td>C-de</td>
    </tr>
    <tr>
      <td>uoge</td>
      <td>lu</td>
      <td>6-ls →</td>
      <td>C-de</td>
    </tr>
    <tr>
      <td>vhqx ▷</td>
      <td>ru</td>
      <td>8-lq →</td>
      <td>A-lq</td>
    </tr>
    <tr>
      <td>ykfq</td>
      <td>qr</td>
      <td>C-s1 →</td>
      <td>2-s1</td>
    </tr>
    <tr>
      <td>btlg + ▷</td>
      <td>9-tr</td>
      <td>s2 →</td>
      <td>it</td>
    </tr>
    <tr>
      <td>eqgt ▷</td>
      <td>1-s1</td>
      <td>lq →</td>
      <td>le</td>
    </tr>
    <tr>
      <td>npkj ></td>
      <td>6-de</td>
      <td>ru →</td>
      <td>lu</td>
    </tr>
    <tr>
      <td>ntuj</td>
      <td>7-de</td>
      <td>at →</td>
      <td>as</td>
    </tr>
    <tr>
      <td>pudt ></td>
      <td>C-le</td>
      <td>tr →</td>
      <td>le</td>
    </tr>
    <tr>
      <td>qbad</td>
      <td>1-ls</td>
      <td>s1 →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>vtlj 3 ></td>
      <td>7-lu</td>
      <td>s2 →</td>
      <td>as</td>
    </tr>
    <tr>
      <td>vncb</td>
      <td>7-lu</td>
      <td>rs →</td>
      <td>sy</td>
    </tr>
    <tr>
      <td>gtlu *</td>
      <td>C-s2</td>
      <td>s2 →</td>
      <td>2-s2</td>
    </tr>
    <tr>
      <td>ituh</td>
      <td>C-tr</td>
      <td>at →</td>
      <td>9-tr</td>
    </tr>
    <tr>
      <td>itui</td>
      <td>C-tr</td>
      <td>at →</td>
      <td>E-tr</td>
    </tr>
    <tr>
      <td>j0vb * ▷</td>
      <td>D-tr</td>
      <td>it →</td>
      <td>C-tr</td>
    </tr>
    <tr>
      <td>ltvl *=</td>
      <td>6-at</td>
      <td>at →</td>
      <td>7-at</td>
    </tr>
    <tr>
      <td>pxdx ▷</td>
      <td>C-le</td>
      <td>rs →</td>
      <td>1-ls</td>
    </tr>
    <tr>
      <td>uydr 5</td>
      <td>4-lu</td>
      <td>lu →</td>
      <td>8-de</td>
    </tr>
    <tr>
      <td>wcch</td>
      <td>8-lu</td>
      <td>tr →</td>
      <td>9-tr</td>
    </tr>
    <tr>
      <td>wxdx ▷</td>
      <td>C-lu</td>
      <td>rs →</td>
      <td>1-ls</td>
    </tr>
    <tr>
      <td>adsd *</td>
      <td>2-de</td>
      <td>1-de →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>etfr * &gt;</td>
      <td>2-s1</td>
      <td>C-s1 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>jbcr</td>
      <td>D-tr</td>
      <td>7-s1 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>pkcr ></td>
      <td>A-le</td>
      <td>7-s1 →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>pxjz ▷</td>
      <td>C-le</td>
      <td>7-ls →</td>
      <td>ls</td>
    </tr>
    <tr>
      <td>qavd</td>
      <td>1-ls</td>
      <td>1-s1 →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>qbgd</td>
      <td>1-ls</td>
      <td>C-s1 →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>rwpd</td>
      <td>6-ls</td>
      <td>C-le →</td>
      <td>de</td>
    </tr>
    <tr>
      <td>vxfj</td>
      <td>7-lu</td>
      <td>6-ls →</td>
      <td>as</td>
    </tr>
    <tr>
      <td>wgba3</td>
      <td>8-lu</td>
      <td>2-lu →</td>
      <td>rs</td>
    </tr>
    <tr>
      <td>xlfr</td>
      <td>1-lq</td>
      <td>C-tr →</td>
      <td>s1</td>
    </tr>
    <tr>
      <td>ewvq</td>
      <td>2-s1</td>
      <td>2-ls →</td>
      <td>7-de</td>
    </tr>
    <tr>
      <td>fjvk</td>
      <td>7-s1</td>
      <td>1-s1 →</td>
      <td>6-at</td>
    </tr>
    <tr>
      <td>g0rw +</td>
      <td>2-s2</td>
      <td>7-tr →</td>
      <td>C-s2</td>
    </tr>
    <tr>
      <td>nnas *</td>
      <td>6-de</td>
      <td>8-de →</td>
      <td>E-de</td>
    </tr>
    <tr>
      <td>voye 5</td>
      <td>6-lu</td>
      <td>1-lu →</td>
      <td>C-de</td>
    </tr>
    <tr>
      <td>voyr 5</td>
      <td>6-lu</td>
      <td>1-lu →</td>
      <td>8-de</td>
    </tr>
    <tr>
      <td>vozd 3</td>
      <td>6-lu</td>
      <td>1-lu →</td>
      <td>8-ls</td>
    </tr>
    <tr>
      <td>wfxh</td>
      <td>8-lu</td>
      <td>1-lu →</td>
      <td>9-tr</td>
    </tr>
    <tr>
      <td>wfyp 5</td>
      <td>8-lu</td>
      <td>1-lu →</td>
      <td>6-de</td>
    </tr>
    <tr>
      <td>wfzb 3</td>
      <td>8-lu</td>
      <td>1-lu →</td>
      <td>6-ls</td>
    </tr>
  </tbody>
</table>
<figure><img src="image_39.png" /><figcaption>Figure 43: Proof tree of "Trans ∧ Irrefl → ASym"</figcaption></figure>

<figure><img src="image_40.png" /><figcaption>Figure 44: Disproof tree of "ASym ∧ Trans ⇌ Refl"</figcaption></figure>

2. (fbao) SemiOrd1 → 1-Dense

3. (fbar) SemiOrd1 → 8-Dense

4. (gknw) SemiOrd2 → 8-LfQuasiRefl

5. (jlmq) Dense → 7-Dense

6. (owgk) LfEucl → 6-AntiTrans

7. (xzhs) LfQuasiRefl → 1-LfQuasiRefl

PROOF. 1. Refl implies LfSerial and RgSerial by [1, Lem.54, p.40]; the latter conjunction is equivalent to 1-LfSerial by Lem. 7.2 and 14.1.

2. Let $xR^1z$, that is, $xRz \wedge zRx$. If $xRx$, then $xR^1x$, and we can choose $x$ as intermediate element. If $
eg xRx$, then $zRz$ by semi-order property 1 applied to $zRx$, $x, x$ incomparable, $xRz$; so we can choose $z$ as intermediate element.

3. Let $xR^8z$, that is, $
eg xRz \wedge \neg zRx$, we distinguish three cases:

* If $
eg xRx$, then $xR^8x$, so $x$ can be used as intermediate element.

* if $
eg zRz$, then $z$ can be used, in a similar way.

* If $xRx \wedge zRz$, then applying semi-order property 1 yields $xRz$, contradicting $xR^8z$.

4. Let $xR^8y$, assume for contradiction $
eg xR^8x$. The latter means $xRx$ by definition. Hence $x, y$ must be comparable w.r.t. $R$, by semi-order-property 2 applied to $xRx$ and $xRx$. But $xR^8y$ means that $x, y$ are incomparable w.r.t. $R$.

5. Let $xR^7z$, then $xRz$ or $zRx$ by definition. In the first case, we have $xRy \wedge yRz$ for some $y$, by density of $R$, hence $xR^7y \wedge yR^7z$ by Lem. 7.4. The second case is similar.

6. Let $xR^6y$ and $yR^6z$, we show $
eg xR^6z$. By definition, we have to distinguish the following cases:

* $xRy \wedge \neg yRx$ and $yRz \wedge \neg zRy$:
  Then $yRy$ by left Euclideanness, hence $yRx$ by the same property, contradicting the case assumption.
* $xRy \wedge \neg yRx$ and $\neg yRz \wedge zRy$:
Then $xRz$ and $zRx$ by left Euclideanness, that is, $\neg xR^6z$.

* $\neg xRy \wedge yRx$ and $yRz \wedge \neg zRy$:
Then $xRz$ would imply the contradiction $xRy$, and $zRx$ would imply the contradiction $zRy$. But $\neg xRz \wedge \neg zRx$ implies $\neg xR^6z$.

* $\neg xRy \wedge yRx$ and $\neg yRz \wedge zRy$:
Then $zRx$ would imply the contradiction $yRz$, and $xRz$ would imply $zRx$ (since $zRz$) which just has been shown to contradict. Again, $\neg xRz \wedge \neg zRx$ implies $\neg xR^6z$.

7. Let $xR^1y$, then $xRy \wedge yRx$ by definition, hence $xRx$ by left quasi-reflexivity, hence $xR^1x$ by definition. $\square$

**Lemma 45. (2-Implications group 2)**

1. (fkdd) $7$-SemiOrd$1 \rightarrow$ Dense

2. (lmco) $1$-AntiTrans $\rightarrow$ C-Refl

**PROOF.** 1. Let $xRz$, we distinguish two cases:

* If $xRx$, we can use $x$ as intermediate element.

* If $\neg xRx$, then applying semi-order property 1 to $zR^7x$, $x$, $x$ incomparable w.r.t. $R^7$, $xR^7z$ yields $zR^7z$, that is, $zRz$, and we can use $z$ as intermediate element.

2. Assume for contradiction $\neg xR^Cx$ for some $x$. Then $xRx$, hence $xR^1x \wedge xR^1x$ by definition, hence $\neg xR^1x$ by anti-transitivity. $\square$

**Lemma 46. (2-Implications group 3)**

1. (fkdo) $7$-SemiOrd$1 \rightarrow$ 1-Dense

**PROOF.** 1. The proof is similar to that of 45.1: Let $xR^1z$, that is, $xRz \wedge zRx$, then $xR^7z$ and $zR^7x$. We distinguish two cases:

* If $xRx$, then $xR^1x$, and we can use $x$ as intermediate element.

* If $\neg xRx$, then applying semi-order property 1 to $zR^7x$, $x$, $x$ incomparable w.r.t. $R^7$, $xR^7z$ yields $zR^7z$, that is, $zRz$, that is $zR^1z$, and we can use $z$ as intermediate element. $\square$

**Lemma 47. (2-Contradictions group 0)**

1. (hpr0) No relation on a set of $\ge 4$ elements can be both AntiTrans and 8-LfUnique.

**PROOF.** 1. Assume for contradiction that $R$ is AntiTrans and $R^8$ is LfUnique. By [1, Lem.22, p.28], AntiTrans implies Irrefl. Let $w, x, y, z$ be 4 distinct elements. By 8-LfUnique, since each element is incomparable to itself, it must be comparable to the other three. Hence, in the directed graph corresponding to $R$, the vertex of $w$ must have two incoming edges or two outgoing ones, leading w.l.o.g. to $x$ and $y$ such that, moreover, w.l.o.g. $xRy$. In the incoming case, we have $xRy$ and $yRw$, but $xRw$. In the outgoing case, we have $wRx$ and $xRy$, but $wRy$. Both contradict AntiTrans. $\square$
**Lemma 48. (3-Implications group 0)**

1. (Oudt) Sym ∧ Trans → LfEucl

2. (d0gh) AntiSym ∧ Sym → CoRefl

3. (dcaa) AntiSym ∧ QuasiTrans → Trans

4. (faok) SemiOrd1 ∧ Refl → Connex

5. (hlmf) AntiTrans ∧ Dense → Empty

6. (ikuv) Trans ∧ AntiTrans → SemiOrd2

7. (oskj) LfEucl ∧ AntiSym → LfUnique

8. (phfb) RgEucl ∧ LfQuasiRefl → Sym

9. (ujry) LfUnique ∧ Irrefl → AntiTrans

10. (ukaa) LfUnique ∧ SemiOrd1 → Trans

11. (ulmt) LfUnique ∧ Dense → LfEucl

12. (xtlr) LfQuasiRefl ∧ SemiOrd2 → SemiOrd1

13. (xxcn) LfQuasiRefl ∧ RgSerial → Refl

14. (xzkv) LfQuasiRefl ∧ RgQuasiRefl → QuasiRefl

**PROOF.** 1. See [1, Lem.36, p.33].

2. See [1, Lem.7.7, p.22].

3. See [1, Lem.19, p.27].

4. See [1, Lem.66, p.45].

5. See [1, Lem.49, p.39].

6. See [1, Lem.24, p.28].

7. See [1, Lem.45, p.37].

8. See [1, Lem.37, p.33].

9. Assume for contradiction $xRy$ and $yRz$, but $xRz$. then $x = y$ by LfUnique, contradicting Irrefl.

10. See [1, Lem.62.2, p.43].

11. See [1, Lem.47.1, p.37].

12. See [1, Lem.73, p.47].

13. See [1, Lem.55.2, p.40].

14. By Def. 1.6. □

In Lem. 48.6, note that a relation $R$ is both Trans and AntiTrans iff $R$ is vacuously transitive, i.e. $\neg\exists x, y, z. xRy \land yRz$. Such a relation also is ASym, 1-, 2-, 6-, 7-AntiTrans, 1-, 8-, C-, E-Dense, 1-, 8-, A-, C-, E-LfQuasiRefl, 8-, A-, C-, E-LfSerial, 1-LfUnique, 1-, C-SemiOrd1, 2-, 3-, C-SemiOrd2, and 1-, 2-, E-Trans.

As a side remark, a relation is both LfQuasiRefl and C-LfQuasiRefl iff it is “right-constant”, i.e. it satisfies $\forall x, y_1, y_2 \in X. xRy_1 \leftrightarrow xRy_2$. Such a relation also satisfies 2- and 6-AntiTrans, 1-, 3-, 7-, 8-, C- E-Dense, 3-, C-LfEucl, 1-, 8-LfQuasiRefl, 1-, 2-, 3-, 7-, C-SemiOrd1, 2-, 3-, C-SemiOrd2, and 1-, 2-, 3-, 8-, 9-, C-, D-Trans. Dually, $R$ is 5-LfQuasiRefl and A-LfQuasiRefl iff it is left-constant (defined similarly). A relation is LfQuasiRefl and A-LfQuasiRefl iff it is totally constant, i.e. it satisfies $\forall x_1, x_2, y_1, y_2 \in X. x_1Ry_1 \leftrightarrow x_2Ry_2$.

It seems promising to investigate more classes of relations that are characterizable by conjunctions of lifted properties.
**Lemma 49. (3-Implications group 1)**

1. (0t0p) Sym $\wedge$ SemiOrd1 $\to$ 1-SemiOrd1

2. (0ucf) Trans $\wedge$ Sym $\to$ 7-Trans

3. (0wyx) Sym $\wedge$ LfSerial $\to$ 1-LfSerial

4. (0yen) Sym $\wedge$ LfUnique $\to$ 7-LfUnique

5. (cnyy) ASym $\wedge$ LfSerial $\to$ 2-LfSerial

6. (qudq) LfSerial $\wedge$ Trans $\to$ 7-Dense

7. (uivk) On a set of $\ge 4$ elements, 3-LfUnique $\wedge$ 8-Trans $\to$ 6-AntiTrans

8. (uklu) On a set of $\ge 5$ elements, 3-LfUnique $\wedge$ 3-SemiOrd2 $\to$ 2-SemiOrd2

**PROOF.** 1. If $R$ is symmetric, then it coincides with its symmetric kernel $R^1$; hence, if the former is SemiOrd1, so is the latter.

2. Similar to 1.

3. Similar to 1.

4. Similar to 1.

5. Given $y$, we find some $x$ with $xRy$ by LfSerial, this implies $
eg yRx$ by ASym, hence $xR^2y$.

6. Let $xR^7y$ hold; w.l.o.g. let $xRy$ hold. By left seriality of $R$, we find some $x'$ such that $x'Rx$; by transitivity, this implies $x'Ry$. Therefore, $xR^7x'$ and $x'R^7y$.

7. Assume for contradiction $xR^6y$ and $yR^6z$, but $xR^6z$. That is, we have exactly one of $xRy$ and $yRx$, and similar for $y, z$ and for $x, z$. Of the 8 cases, only 2 satisfy LfUnique, viz. those corresponding to directed cycles. By 8-Trans, any fourth element $w$ must be comparable to (w.l.o.g.) $x$ and $y$; this is impossible due to LfUnique.

8. Assume for contradiction $xR^2y$ and $yR^2z$, let $w \neq w'$ be both distinct from $x, y, z$. From 3-SemiOrd2, we obtain that $w$ is related (w.r.t. $R$) to one of $x, y, z$. By 3-LfUnique, neither $wRz$ nor $wRy$ can hold, so the only case that could violate 2-SemiOrd2 is $xRw \wedge wRx$. By the same argument, we obtain $xRw' \wedge w'Rx$. However, $wRx \wedge w'Rx$ violates 3-LfUnique. $\square$

**Lemma 50. (3-Implications group 2)**

1. (0vcy) Sym $\wedge$ 1-AntiTrans $\to$ AntiTrans

2. (0vyd) Sym $\wedge$ 7-Dense $\to$ Dense

3. (0xjz) Sym $\wedge$ 7-LfSerial $\to$ LfSerial

4. (0xzj) Sym $\wedge$ 1-LfUnique $\to$ LfUnique

5. (0zet) Sym $\wedge$ 1-LfQuasiRefl $\to$ LfQuasiRefl

6. (xzog) LfQuasiRefl $\wedge$ 8-LfQuasiRefl $\to$ 8-Trans

**PROOF.** 1. If $R$ is symmetric, then its symmetric kernel $R^1$ coincides with $R$ itself; hence, if the former is anti-transitive, so is the latter.

2. Similar to 1, using the symmetric closure instead of the kernel.

3. Similar to 1.

4. Similar to 1.

5. Similar to 1.
6. Let $x, y$ and $y, z$ be incomparable w.r.t. $R$. Then $x, x$ and $y, y$ are incomparable w.r.t. $R$ by 8-LfQuasiRefl. Assume for contradiction $xRz \lor zRx$. In the first case, we have the contradiction $xRx$ by 3-LfQuasiRefl. In the second case, we have $zRz$ by 3-LfQuasiRefl; but $y, y$ and $y, z$ incomparable should imply $z, z$ incomparable. □

**Lemma 51. (lu, de)** Let $\mathbf{Sym} = \{0, 1, 6, 7, 8, 9, E, F\}$ denote the set of all unary operations that are guaranteed to yield always a symmetric relation by Lem. 10.14. Let $p, q, r$ be unary operations such that

1. $(p \land q) = 0$,

2. $(p \lor q) \supseteq (\neg r)$, and

3. $(\neg r) \in \mathbf{Sym}$, or $p, q \in \mathbf{Sym}$.

Then $p$-LfUnique and $q$-LfUnique implies $r$-Dense.

**PROOF.** First, we prove the case $(\neg r) \in \mathbf{Sym}$. Assume for contradiction that $xR^r z$, but (using symmetry of $R^{-r}$) that $yR^{-r} x \lor yR^{-r} z$ for all $y$. Let $p' = (p \land \neg r)$ and $q' = (q \land \neg r)$, then $p'$ and $q'$ are disjoint like $p$ and $q$, and $(\neg r) = (p' \lor q')$, so we can make the following case distinction for all $y$:

1. If $yR^{p'} x$, then $yR^p x$ by Lem. 7.4;

2. if $yR^{q'} x$, then similarly $yR^q x$;

3. if $yR^{p'} z$, then $yR^p z$;

4. if $yR^{q'} z$, then $yR^q z$.

Choosing 5 distinct elements $y_1, \dots, y_5$, one of the cases must appear twice. Double appearance of case 1 or 3 contradicts $p$-LfUnique, double appearance of case 2 or 4 contradicts $q$-LfUnique.

For the case $p, q \in \mathbf{Sym}$, we use a similar reasoning: Assume for contradiction that $xR^r z$, but $xR^{-r} y \lor yR^{-r} z$ for all $y$. Defining $p', q'$ as above, we get these cases:

1. If $xR^{p'} y$, then $xR^p y$ by Lem. 7.4, hence $yR^p x$ by symmetry of $R^p$;

2. if $yR^{q'} x$, then similarly $yR^q x$;

3. if $yR^{p'} z$, then $yR^p z$;

4. if $yR^{q'} z$, then $yR^q z$.

Again, double appearance of 1 or 3 contradicts $p$-LfUnique, and double appearance of case 2 or 4 contradicts $q$-LfUnique. □

**Lemma 52. (3-Implications group 5)**

1. (gtlu) C-SemiOrd2 $\land$ SemiOrd2 $\rightarrow$ 2-SemiOrd2

2. (uydr) On a domain of $\ge 5$ elements, 3-LfUnique $\land$ 4-LfUnique $\rightarrow$ 8-Dense

**PROOF.** 1. The proof extensively uses boolean connectives on operations (Lem. 7) to shorten the proof presentation. Let $x_1 R^2 x_2$ and $x_2 R^2 x_3$, and let $w$ be given; we have to show $wR^6 x_i$ for some $i \in \{1, 2, 3\}$. Assume for contradiction there is no such $i$, that is, $wR^9 x_i$ for all $i$. We distinguish two cases:
* If $wRw$,
then $wRw$ and $wRw$ implies $wR^7y$ for each $y$, by SemiOrd2. Hence $wR1x_i$ for each $i$ by assumption. But $x_3R^C x_2$ and $x_2R^C x_1$ requires $wR^E x_i$ for some $i$, by C-SemiOrd2, which is a contradiction.

* If $\neg wRw$,
then $wR^Cw$ and $wR^Cw$ implies $wR^E y$ for each $y$, by C-SemiOrd2. Hence, $wR8x_i$ for each $i$ by assumption. But this contradicts SemiOrd2.

2. Follows from Lem. 51 with $p = 3$, $q = 4$, and $r = 8$, since $(\neg r) = 7 \in \text{Sym}$. $\square$

**Lemma 53.** (3-Implications group 6)

1. (vxfj) 7-LfUnique $\wedge$ 6-LfSerial $\rightarrow$ ASym

2. (xlfr) 1-LfQuasiRefl $\wedge$ C-Trans $\rightarrow$ SemiOrd1

**PROOF.** 1. Let $xRy$, assume for contradiction $yRx$, i.e. $xR^1y$. By 6-LfSerial, we obtain some $w$ such that $wR^6x$. Since $xR^1y$ implies $xR^7y$, and similarly $wR^6x$ implies $xR^7w$, we get $w = y$ by 7-LfUnique. But $xR^1y$ and $xR^6y$ (using symmetry of $R^6$) implies $xR^0y$ by Lem. 7.2, a contradiction.

2. Let $wRx$ and $xR^8y$ and $yRz$. Assume for contradiction $\neg wRz$. Then also $zRy$, since else, we had $\neg wRy$ by C-Trans, and $\neg wRx$ by C-Trans again. Applying 1-LfQuasiRefl, we obtain $yR^1y$. But $\neg xRy$ and $\neg yRx$ imply the contradiction $\neg yRy$ by C-Trans. $\square$

**Lemma 54.** (3-Implications group 7)

1. (ewvq) 2-SemiOrd1 $\wedge$ 2-LfSerial $\rightarrow$ 7-Dense

2. (g0rw) 2-SemiOrd2 $\wedge$ 7-Trans $\rightarrow$ C-SemiOrd2

3. (voye) On a domain of $\ge 5$ elements, 1-LfUnique $\wedge$ 6-LfUnique $\rightarrow$ C-Dense

4. (voyr) On a domain of $\ge 5$ elements, 1-LfUnique $\wedge$ 6-LfUnique $\rightarrow$ 8-Dense

5. (wfyp) On a domain of $\ge 5$ elements, 1-LfUnique $\wedge$ 8-LfUnique $\rightarrow$ 6-Dense

**PROOF.** 1. Let $xR^7y$, w.l.o.g. let $xRy$. By 2-LfSerial, we obtain $x'$, $y'$ with $x'R^2x$ and $y'R^2y$. We have two cases:

* If $x, y'$ are comparable w.r.t. $R$, then $xR^7y'$, that is, $y'$ is an intermediate element, and we are done.

* Else, we apply 2-SemiOrd1 to $x'R^2x$, $x, y'$ incomparable w.r.t. $R^2$, $y'R^2y$ to obtain $x'R^2y$, hence $x'R^7y$, hence $x'$ being an intermediate element.

2. Assume for contradiction $\neg xRy \wedge \neg yRz$, but $wRx \wedge xRw \wedge wRy \wedge yRw \wedge wRz \wedge zRw$ for some $x, y, z, w$. By 7-Trans, we get $xRy \lor yRx$ and $yRz \lor zRy$, that is, $yRx$ and $zRy$. That is, $zR^2y \wedge yR^2x$, but $w$ is incomparable (w.r.t. $R^2$) to $x, y$, and 2, contradicting 2-SemiOrd2.

3. Follows from Lem. 51 with $p = 1$, $q = 6$, and $r = C$, since $p, q \in \text{Sym}$.

4. Follows from Lem. 51 with $p = 1$, $q = 6$, and $r = 8$. since $(\neg r) = 7 \in \text{Sym}$.

5. Follows from Lem. 51 with $p = 1$, $q = 8$, and $r = 6$, since $(\neg r) = 9 \in \text{Sym}$. $\square$
**Lemma 55. (cjdj)** If $R$ is ASym, then $R^1$ is CoRefl, LfEucl, LfUnique, Sym, AntiTrans, ASym, AntiSym, Trans, SemiOrd1, Dense (cjdj).

**PROOF.** From the assumption follows that $R^1$ is empty, hence has all claimed properties by [1, Exm. 74, p.48]. □

**Theorem 56. (3-implication axioms)** Recall that a “3-implication” is a formula of the form $\forall R. lprop_1(R) \land lprop_2(R) \rightarrow lprop_3(R)$, where $lprop_i$ are unnegated lifted properties. Consider the inference system from Def. 25 and 26; inferences are understood to apply the equivalences from Thm. 22 as needed.

A 3-implication is valid (w.r.t. a relation domain of $\ge 7$ elements) iff it can be inferred from the set of axioms shown in Fig. 42.

**PROOF.** “$\Leftarrow$”: All axioms have been proven to be valid, by EProver, or manually (Sect. 5.8), or both. The inference rules of Def. 25 and 26 are obviously sound.

“$\Rightarrow$”: All 3-implications that couldn’t be inferred were proven to be invalid, either by a computer-generated counter-example on a domain of 5 elements, or a manual counter-example w.r.t. a finite (Sect. 5.4) or infinite (Sect. 5.5) domain. □
6. References

[1] J. Burghardt, Simple Laws about Nonprominent Properties of Binary Relations, Technical Report, URL https://arxiv.org/abs/1806.05036v2, 2018.

[2] A. K. Sen, Quasi-Transitivity, Rational Choice and Collective Decisions, Review of Economic Studies 36 (3) (1969) 381–393, URL https://www.jstor.org/stable/2296434.