The conventional signature for a Bounded Lattice (for example on wikipedia) specifies 5 components:
- (L,
v,^,0,1)
If we're told it's a Bounded Lattice, and given L and the join operation v:
0is the identity forv, and must be in L.1is the absorbing element forv, and must be in L.^is dual ofv, and can be specified as(x = (x v z) & y = (y v z)) <-> ((x ^ y) = (x ^ y) v z).(
x ^ yis the greatest element less than bothx, y. From this spec we can infer the properties of^, and the absorption laws.)
Or ...? Is there some freedom of choice of the bottom, top elements or of the meet operation?
There is no over-specification.
When we talk about a bounded lattice $\mathbf L = (L, \wedge, \vee, 0, 1)$, which is an type of algebra, we mean that any sub-algebra (a sub-bounded lattice) must include $0,1$ (we would require this if the constants were not in the signature); likewise, any homomorphism must preserve these constants (and so it must be between bounded lattices, and not every lattice is bounded).
Having a neutral and/or absorbing elements is not part of the signature of lattices in general (think of $(\mathbb Z, \leq)$, where $\leq$ is the usual ordering).
Expressions like $$s_1(x,y,z) = t_1(x,y,z) \Leftrightarrow s_2(x,y,z) = t_2(x,y,z)$$ are not equations, and they don't always can be expressed as equations (sometimes they can), and equations are usually preferred, in algebra.
Being the greatest lower bound of two elements is also not an algebraic definitions. It happens that for some algebras (like lattices), that notion can be formulated in algebraic (equational) terms. That's why lattices are often defined that way.
You can use the definition of lattice just using order-theoretic concepts, that's ok, but if you want an algebraic definition, you have to stick with equations.