| symbol | name |
|---|---|
| \( a \land b \) | conjunction / meet |
| \( a \lor b \) | disjunction / join |
| \( \top \) | true / top |
| \( \bot \) | false / bottom |
| \( \forall x . a \) | universal quantification |
| \( \exists x . a \) | existential quantification |
| \( \square a \) | necessity |
| \( \lozenge a \) | possibility |
| \( a \to b \) | implication |
| \( a \setminus b \) | subtraction |
| \( \neg a \) | negation / complement |
| \( a = b \) | equality |
| \( a : b \) | typing |
| formula | name | combinator |
|---|---|---|
| \( a \to b \to a \) | weakening | \( f a b = a \) |
| \( (a \to a \to b) \to a \to b \) | contraction | \( f a b = a b b \) |
| \( a \to a \) | identity | \( f a = a \) |
| \( (a \to b) \to (b \to c) \to a \to c \) | composition | \( f a b c = b (a c) \) |
| \( (a \to b \to c) \to b \to a \to c \) | exchange | \( f a b c = a c b \) |
| \( a \land b \to a \) | left projection | \( f \langle a, b \rangle = a \) |
| \( a \land b \to b \) | right projection | \( f \langle a, b \rangle = b \) |
| \( a \to a \lor b \) | left injection | |
| \( b \to a \lor b \) | right injection | |
| \( a \to b \to a \land b \) | ||
| \( a \to b \to c \to a \land b \to c \) | ||
| \( (a \to c) \to (b \to c) \to (a \lor b) \to c \) |
| formula | name |
|---|---|
| \( a b = b a \) | commutative |
| \( a (b c) = (a b) c \) | associative |
| \( (a b) (c d) = (a c) (b d) \) | medial |
| \( (a a) (b c) = (a b) (a c) \) | left semimedial |
| \( (b c) (a a) = (b a) (c a) \) | right semimedial |
| \( (a a) b = a (a b) \) | left alternative |
| \( b (a a) = (b a) a \) | right alternative |
| \( a (b a) = (a b) a \) | flexible |
| \( (a b = a c) \to b = c \) | left cancellative |
| \( (b a = b c) \to b = c \) | right cancellative |
| \( a (b c) = (a b) (a c) \) | left distributive |
| \( (a b) c = (a c) (b c) \) | right distributive |
| \( a = b \) | trivial |
| \( a a = a \) | idempotent |
| \( a a = b b \) | unipotent |
| \( (a a) b = a a = b (a a) \) | zeropotent |
| \( a b = a \) | left zero |
| \( a b = b \) | right zero |
| \( a b = c d \) | null |
| \( (a b) (b c) = b \) | central |
| \( a (a b) = b \) | left symmetric |
| \( (a b) b = a \) | right symmetric |
| property | primal | dual |
|---|---|---|
| commutativity | \( a \land b = b \land a \) | \( a \lor b = b \lor a \) |
| associativity | \( a \land (b \land c) = (a \land b) \land c \) | \( a \lor (b \lor c) = (a \lor b) \lor c \) |
| idempotence | \( a \land a = a \) | \( a \lor a = a \) |
| identity | \( a \land \top = a \) | \( a \lor \bot = a \) |
| annihilation | \( a \land \bot = \bot \) | \( a \lor \top = \top \) |
| absorption | \( a \land (a \lor b) = a \) | \( a \lor (a \land b) = a \) |
| complementarity | \( a \land \neg a = \bot \) | \( a \lor \neg a = \top \) |
| implication and subtraction | \( a \to b = \neg a \lor b \) | \( a \setminus b = a \land \neg b \) |
| contraposition | \( a \to b = \neg b \to \neg a \) | \( a \setminus b = \neg b \setminus \neg a \) |
| de Morgan laws | \( \neg (a \land b) = \neg a \lor \neg b \) | \( \neg (a \lor b) = \neg a \land \neg b \) |
| distributivity | \( a \lor (b \land c) = (a \lor b) \land (a \lor c) \) | \( a \land (b \lor c) = (a \land b) \lor (a \land c) \) |
| \( \square (a \land b) = \square a \land \square b \) | \( \lozenge (a \lor b) = \lozenge a \lor \lozenge b \) | |
| \( \square \top = \top \) | \( \lozenge \bot = \bot \) |
| name | commutativity | associativity | idempotence | identity |
| magma | ||||
| semigroup | ||||
| monoid | ||||
| band | ||||
| group | ||||
| quasigroup | ||||
| loop |