Syntax | Terms | Equations | Horn formulas | Universal formulas | First-order formulas | Theories

Here we list equations, with the shorter term on the right (if possible).

1 trivial equations: $x = y$ $\quad f(x) = y$ $\quad x*y = z$ $\Rightarrow$ one-element algebras
2 identity operation: $f(x) = x$
3 involutive operation: $f(f(x)) = x$
4 inverse operations: $f(g(x)) = x$
5 inside absorption: $f(g(x)) = f(x)$
6 outside absorption: $f(g(x)) = g(x)$
7 order-$n$ operation: $f^n(x) = x$
8 $f$-idempotent $f(f(x)) = f(x)$
9 constant operations: $f(x) = 1$ $\quad f(x) = f(y)$ $\quad x*y = 1$ $x*y = f(z)$ $x*y = z*w$
10 left projection: $x*y = x$ right projection: $x*y = y$
11 idempotent: $x*x = x$
12 $n$-potent: $x^{n+1} = x^n$
13 left identity: $1*x = x$ right identity: $x*1 = x$
14 left zero: $0*x = 0$ right zero: $x*0 = 0$
15 left $f$-projection: $x*y = f(x)$ right $f$-projection: $x*y = f(y)$
16 square constant: $x*x = 1$
17 square definition: $x*x = f(x)$
18 left constant multiple: $1*x = f(x)$ right constant multiple: $x*1 = f(x)$
19 commutative: $x*y = y*x$
20 left inverse: $f(x)*x = 1$ right inverse: $x*f(x) = 1$
21 left $f$-identity: $f(x)*x = x$ right $f$-identity: $x*f(x) = x$
22 interassociative: $x*(y+z) = (x+y)*z$
23 associative: $x*(y*z) = (x*y)*z$
24 left commutativity: $x*(y*z) = y*(x*z)$ right commutativity: $(x*y)*z = (x*z)*y$
25 left idempotent: $x*(x*y) = x*y$ right idempotent: $(x*y)*y = x*y$
26 left rectangular: $(x*y)*x = x$ right rectangular: $x*(y*x) = x$
27 left absorption: $(x*y)+x = x$ right absorption: $x+(y*x) = x$
28 left absorption1: $(x*y)+y = y$ right absorption1: $y+(x*y) = y$
29 left subtraction: $x*(x+y) = y$ right subtraction: $(y+x)*x = y$
30 left distributive: $x*(y+z) = (x*y)+(x*z)$ right distributive: $(x+y)*z = (x*z)+(y*z)$
31 left self-distributive: $x*(y*z) = (x*y)*(x*z)$ right distributive: $(x*y)*z = (x*z)*(y*z)$
32 $f$-commutative: $f(x)*f(y) = f(y)*f(x)$
33 $f$-involutive: $f(x*y) = f(y)*f(x)$
34 $f$-interdistributive: $f(x*y) = f(x)+f(y)$
35 $f$-distributive: $f(x*y) = f(x)*f(y)$ also $f$-linear
36 left $f$-constant multiple: $f(1*x) = 1*f(x)$ right $f$-constant multiple: $f(x*1) = f(x)*1$
37 left twisted: $f(x*y)*x = x*f(y)$ right twisted: $x*f(y*x) = f(y)*x$
38 left locality: $f(f(x)*y) = f(x*y)$ right locality: $f(x*f(y)) = f(x*y)$
39 left $f$-distributive: $f(f(x)*y) = f(x)*f(y)$ right $f$-distributive: $f(x*f(y)) = f(x)*f(y)$
40 left $f$-absorbtive: $f(x)*f(x*y) = f(x*y)$ right $f$-absorbtive: $f(x*y)*f(y)) = f(x*y)$
41 flexible: $(x*y)*x = x*(y*x)$
42 entropic: $(x*y)*(z*w) = (x*z)*(y*w)$
43 paramedial: $(x*y)*(z*w) = (w*y)*(z*x)$
44 Moufang1: $((x*y)*x)*z = x*(y*(x*z))$ Moufang2: $((x*y)*z)*y = x*(y*(z*y))$
45 Moufang3: $(x*y)*(z*x) = (x*(y*z))*x$ Moufang4: $(x*y)*(z*x) = x*((y*z)*x)$

Here are the identities in the syntax of the Lean Theorem Prover

section identities

variables {α: Type u} {β: Type v}
variables f g: α → α → α
variables h k: α → α
variable  c: α
local notation a⬝b  := f a b
local notation a+b := g a b
local notation a⁻¹ := h a
local notation 1   := c
local notation 0   := c

def involutive              := ∀x,     h(h x) = x
def inverse_operations      := ∀x,     h(k x) = x
def left_absorption         := ∀x,     h(k x) = k x
def right_absorption        := ∀x,     h(k x) = h x
def unary_idempotent        := ∀x,     h(h x) = h x
def idempotent              := ∀x,     x⬝x = x
def left_identity           := ∀x,     1⬝x = x
def right_identity          := ∀x,     x⬝1 = x
def left_zero               := ∀x,     0⬝x = 0
def right_zero              := ∀x,     x⬝0 = 0
def left_inverse            := ∀x,     x⁻¹⬝x = 1
def right_inverse           := ∀x,     x⬝x⁻¹ = 1
def left_const_mult         := ∀x,     c⬝x = h x
def right_const_mult        := ∀x,     x⬝c = h x
def square_constant         := ∀x,     x⬝x = c
def square_unary            := ∀x,     x⬝x = h x
def left_unary_identity     := ∀x,     (h x)⬝x = x
def right_unary_identity    := ∀x,     x⬝(h x) = x
def left_unary_const_mult   := ∀x,     h(c⬝x) = c⬝(h x)
def right_unary_const_mult  := ∀x,     h(x⬝c) = (h x)⬝c
def commutative             := ∀x y,   x⬝y = y⬝x
def left_unary_projection   := ∀x y,   x⬝y = h x
def right_unary_projection  := ∀x y,   x⬝y = h y
def left_idempotent         := ∀x y,   x⬝(x⬝y) = x⬝y
def right_idempotent        := ∀x y,   (x⬝y)⬝y = x⬝y
def left_rectangular        := ∀x y,   (x⬝y)⬝x = x
def right_rectangular       := ∀x y,   x⬝(y⬝x) = x
def left_absorption1        := ∀x y,   (x⬝y)+y = y
def right_absorption1       := ∀x y,   y+(x⬝y) = y
def left_absorption2        := ∀x y,   (x⬝y)+x = x
def right_absorption2       := ∀x y,   x+(y⬝x) = x
def left_subtraction        := ∀x y,   x⬝(x+y) = y
def right_subtraction       := ∀x y,   (y+x)⬝x = y
def unary_commutative       := ∀x y,   (h x)⬝(h y) = (h y)⬝(h x)
def unary_involutive        := ∀x y,   h(x⬝y) = (h y)⬝(h x)
def interdistributive       := ∀x y,   h(x⬝y) = (h x)+(h y)
def unary_distributive      := ∀x y,   h(x⬝y) = (h x)⬝(h y) 
def left_twisted            := ∀x y,   (h(x⬝y))⬝x = x⬝(h y) 
def right_twisted           := ∀x y,   x⬝(h(y⬝x)) = (h y)⬝x
def left_locality           := ∀x y,   h((h x)⬝y) = h(x⬝y)
def right_locality          := ∀x y,   h(x⬝(h y)) = h(x⬝y)
def left_unary_distributive := ∀x y,   h((h x)⬝y) = (h x)⬝(h y)
def right_unary_distributive:= ∀x y,   h(x⬝(h y)) = (h x)⬝(h y)
def left_absorbtive         := ∀x y,   (h x)⬝(h(x⬝y)) = h(x⬝y)
def right_absorbtive        := ∀x y,   (h(x⬝y))⬝(h y) = h(x⬝y)
def flexible                := ∀x y,   (x⬝y)⬝x = x⬝(y⬝x)
def associative             := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝z
def left_commutative        := ∀x y z, x⬝(y⬝z) = y⬝(x⬝z)
def right_commutative       := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝y
def interassociative1       := ∀x y z, x⬝(y+z) = (x⬝y)+z
def interassociative2       := ∀x y z, x⬝(y+z) = (x+y)⬝z
def left_distributive       := ∀x y z, x⬝(y+z) = (x⬝y)+(x⬝z)
def right_distributive      := ∀x y z, (x+y)⬝z = (x⬝z)+(y⬝z)
def left_self_distributive  := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝(x⬝z)
def right_self_distributive := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝(y⬝z)
def Moufang1                := ∀x y z, ((x⬝y)⬝x)⬝z = x⬝(y⬝(x⬝z))
def Moufang2                := ∀x y z, ((x⬝y)⬝z)⬝y = x⬝(y⬝(z⬝y))
def Moufang3                := ∀x y z, (x⬝y)⬝(z⬝x) = (x⬝(y⬝z))⬝x
def Moufang4                := ∀x y z, (x⬝y)⬝(z⬝x) = x⬝((y⬝z)⬝x)
def entropic                := ∀x y z w, (x⬝y)⬝(z⬝w) = (x⬝z)⬝(y⬝w)
def paramedial              := ∀x y z w, (x⬝y)⬝(z⬝w) = (w⬝y)⬝(z⬝x)


end identities