0
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ You quote a perfectly fine definition of the greatest lower bound = glb = infimum $\sqcap S$ of a set $S$, and then you say that you don't understand how this [definition of a glb] is supposed to provide a glb, and then you say that you can see how this [definition of a glb] produced a lub. So you see how the definition of a glb produces a lub, but you don't see how it produces a glb???? I am confused. Is there a typo in your question? Did you type glb where you meant lub? $\endgroup$ – bof Oct 5 '14 at 10:43
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I had indeed switched glb and lub in a few places. I've updated the question. $\endgroup$ – Dave Oct 5 '14 at 19:35
  • $\begingroup$ I had indeed switched glb and lub in a few places. I've updated the question. Thanks for the answer -- that clarifies things. I'm missing that sense of understanding -- I don't have a feel for what the empty-set condition has to do with completeness, but now I at least understand the proof, if not the essence. $\endgroup$ – Dave Oct 5 '14 at 19:41
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.