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 f(x)=y x∗y=z | ⇒ 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: | fn(x)=x | ||
| 8 | f-idempotent | f(f(x))=f(x) | ||
| 9 | constant operations: | f(x)=1 f(x)=f(y) 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: | xn+1=xn | ||
| 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
