Let $(P,\le)$ be a partially ordered set and $\preceq$ the Hoare pre-order on its subsets, i.e. for $X,Y\subseteq P$, $X\preceq Y$ iff $\forall x\in X:\exists y\in Y:x\le y$.

Let $\sim$ be the equivalence on the power set $2^P$ generated by $\preceq$, i.e. $X\sim Y$ iff $X\preceq Y$ and $Y\preceq X$. Let $M=2^P/\mathord\sim$ be the quotient, then $\preceq$ passes to a partial order, also denoted $\preceq$, on $M$.

Is $(M,\preceq)$ a complete lattice?

  • $\begingroup$ As far as I can see, a union of a family of sets is its lub in $\preceq$, or am I missing something? $\endgroup$ May 5 '15 at 13:58
  • 1
    $\begingroup$ In fact, $(M,\preceq)$ is apparently (isomorphic to) the complete lattice of downsets in $P$, as $X\preceq Y$ iff $X{\downarrow}\subseteq Y{\downarrow}$. This is an upside-down complete Heyting algebra. $\endgroup$ May 5 '15 at 14:03
  • $\begingroup$ Thank you Emil, this looks right to me. But (next question) is it well-known? I'm not familiar with the old papers on domain theory, but it seems like something which should be in there. $\endgroup$ May 20 '15 at 12:46

Your Answer

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

Browse other questions tagged or ask your own question.