Equations of order greater than \(4\)

We note some selected laws of order more than \(5\), which are used in some later chapters of the blueprint.

DefinitionEquation 5093 #

Equation 5093 is the law \(0 \simeq 1 \diamond (1 \diamond (1 \diamond (0 \diamond (2 \diamond 1))))\) (or the equation \(x = y \diamond (y \diamond (y \diamond (x \diamond (z \diamond y))))\)).

Lean

Formalized as Equation5093.

Sources

Equational Theories blueprint: chapter/equations.tex, line 310

LeanEquation5093

Uses 1 · Used by 1

Statement usesMagma

Used byEquation 5093 has no non-trivial finite models

This law of order \(5\) was mentioned in (Kisielewicz 1997). See Equation 5093 has no non-trivial finite models.

A law that characterizes natural central groupoids; see Natural central groupoid axiom.

DefinitionEquation 28770 #

Equation 28770 is the law \(0 \simeq (((1 \diamond 1) \diamond 1) \diamond 0) \diamond (1 \diamond 2)\) (or the equation \(x = (((y \diamond y) \diamond y) \diamond x) \diamond (y \diamond z)\)).

Lean

Formalized as Equation28770.

Sources

Equational Theories blueprint: chapter/equations.tex, line 326

LeanEquation28770

Uses 1 · Used by 1

Statement usesMagma

Used byKisielewicz's second Austin law

This law of order \(5\) was introduced by Kisielewicz (Kisielewicz 1990). See Kisielewicz's second Austin law.

This law of order \(6\) was shown in (McCune et al. 2002) to characterize the Sheffer stroke in a boolean algebra; see Sheffer stroke axiom.

DefinitionEquation 374794 #

Equation 374794 is the law \(0 \simeq (((1 \diamond 1) \diamond 1) \diamond 0) \diamond ((1 \diamond 1) \diamond 2)\) (or the equation \(x = (((y \diamond y) \diamond y) \diamond x) \diamond ((y \diamond y) \diamond z)\)).