Formal Definition of a Lattice I am new to lattices, having some difficulty understanding the main definition. First, here are my main questions.


*

*What it means for every pair in a lattice to have a lub/glb. For example, what can $\{x,y,z\}$ be paired with in the diagram to give it a lub/glb.

*How to formalize the definition: $\forall \{a, b\} \in P, \{a,b\}\ has\ lub\ and\ glb$



Second, here is my understanding so far if that's helpful...
A partial order is a binary relation $\prec$ over a set $X$, creating a poset, written as $P = (X, \prec)$, satisfying:


*

*$a \prec a$ (reflexivity)

*$a \prec b \land b \prec a \Rightarrow a = b$ (anti-symmetry)

*$a \prec b \land b \prec c \Rightarrow a \prec c$ (transitivity)


Posets can be drawn graphically as Hasse diagrams.
A maximal element of $p_{max} \in P$ satisfies:
$$\neg (\exists x \in P : p_{max}\prec x)$$
A minimal element of $p_{min} \in P$ satisfies:
$$\neg (\exists x \in P : x \prec p_{min})$$
An upper bound of $S \subset P$ is an element $p_{(+)} \in P$ such that:
$$p_{(+)} \succeq x, \forall x \in S$$
A least upper bound of $S \subset P$ is an element $p_{(<)} \in P$ satisfying:
$$\forall p_{(+)} \in S,\ p_{(<)} \preceq p_{(+)}$$
A lower bound of $S \subset P$ is an element $p_{(-)} \in P$ such that:
$$p_{(-)} \preceq x, \forall x \in S$$
A greatest lower bound of $S \subset P$ is an element $p_{(>)} \in P$ satisfying:
$$\forall p_{(-)} \in S,\ p_{(>)} \succeq p_{(-)}$$
A join semi-lattice is a poset $P$ where every pair of elements has a least upper bound (join).
A meet semi-lattice is a poset $P$ where every pair of elements has a greatest lower bound (meet).
A lattice arises when every pair of elements in $P$ has a least upper bound and greatest lower bound.
$$\forall \{a, b\} \in P, \{a,b\}\ has\ lub\ and\ glb$$
Not sure how to write that formally.

 A: Assuming that $\prec$ is reflexive, the sentence
$$\forall a\forall b\exists p\forall x(p\prec x\leftrightarrow(a\prec x\land b\prec x))$$
says that every pair of elements has a least upper bound, while the sentence
$$\forall a\forall b\exists q\forall x(x\prec q\leftrightarrow(x\prec a\land x\prec b))$$
says that every pair of elements has a greatest lower bound.
A: As already said in the comments: every pair means every unordered pair, that can be formed of elements of the given base set, in our case the lattice or ordered set.
An upper bound of a set $S$ is an element $u$ such that it fulfils the following condition: “If an element $b$ is in $S$ then it is equal or below $u$.” Given $S=∅$ this means the precondition is always false so this implication is always true. That means every element is an upper bound of the empty set. The same is true for the lower bound. As an intuition: In the Order diagrams you provided an upper bound of a set is a point, that can be reached from every element of the set by following the arrows. Dually, a lower bound is a starting point that has paths to all nodes representing the Set elements.
The set of upper bounds can have an infinite descending chain of the order relation, so that all elements below the chain are not upper bounds. In that case there is no least upper bound. The lub is also missing if the Set of upper bounds as at least two different minimal elements. In that case none of the minima is below the others, which mean the set of upper bounds has no least element. This is helpful to see whether a Hasse diagram describes a lattice. And there is a third case where an ordereded set is not a lattice: The set of lower bounds is empty. This can happen in many different situations. One easy to recognise case is when the ordered set has two distinct maximal elements. Neither is above the other so there is no common upper bound, which means that there is no least upper bound. Finally, there is the case that the set of common upper bounds has a smallest element. This is equivalent to the fact that every common upper bound can be reached on a path through this least upper bound and this common element is unique.
Why are we discussing pairs? Actually in a lattice every finite subset has both an lub and glb this can be shown by induction. This implication is one-way only. The set of two-element subsets (aka unordered pairs) is the smallest subset that must be checked. From sets that consist only of larger subsets you cannot conclude that it is a lattice.
