How is a complete lattice defined solely by a least-upper bound?

Question

I'm pretty far into "Concrete Semantics With Isabelle HOL" and I've come to a section on complete lattices. Their definition of "complete lattice" goes like this:

A type $'a$ with a partial order $\leq$ is a complete lattice if every set $S ::\; 'a\; set$ has a greatest lower bound $\sqcap S ::\; 'a$

By "a type 'a with a partial order $\leq$", they mean that the values of 'a (not the type hierarchy) form a partial order. The definition of partial order is conventional (ie reflexive, anti-symmetric, transitive).

The greatest lower bound $\sqcap S$ is defined as:

• $\forall s \in S. \sqcap S \leq s$

• If $\forall s \in S. l \leq s$ then $l \leq \sqcap S$

I am far from understanding this but, to me, this looks like a partial lattice, not complete. In particular, I don't understand how this is supposed to provide a glb (I can see how this produces an lub). The following exercise from the book sums up my confusion:

Where is the confusion in the following argument? The natural numbers form a complete lattice because any set of natural numbers has an infimum, its least element.

I know that the naturals do not form a complete lattice - e.g. ${x > 3}$ has no glb. And I assume that the answer to this question is that the empty set doesn't work but I might be wrong since it seems fine by their definition to define that {0} is the glb of {}.

Extra points for an answer that tells me how to prove the existence of the lub given just that glb (ie why is the lattice complete, which I always defined as having an lub AND a glb?). I know from other books that this is the key takeaway from this theorem and I figure its about time I understood how.

Answer 1

If $P$ is a poset such that every $S\subseteq P$ has a supremum (i.e., lub), then the the infimum (i.e., glb) of a fixed set $S$ is the the supremum of all the lower bounds of $S$. The proof is obtained just by deciphering the definitions.

Answer 2

The problem is here:

fine by their definition to define that $\{0\}$ is the lub of $\{\}$.

I think you meant "that $0$ is the greatest lower bound of $\{\}$." But $1$ is a lower bound of $\{\}$ as well: for all $x\in \{\}, x\geq 1$. So $0$ couldn't be the greatest lower bound.

The upshot is that for $\Bbb N$ you did not actually find a suitable candidate for the glb of $\{\}$, nor will you be able to. If you think about the last paragraph long enough, you'll see that that any element is a lower bound of the emptyset, so if we truly did have greatest lower bounds, the glb would have to be the greatest element of the entire poset.

So while nonempty subsets of $\Bbb N$ are cooperative with greatest lower bounds, the emptyset is not so cooperative :)

how to prove the existence of the glb given just that lub

The next paragraph in the book you're citing tells you everything you need to know. (I think you've reversed glb and lub again here too.) Just verify that the glb of all upper bounds to a set is actually the lub of the set. It exists because glb's exist for all subsets.