# [Haskell-cafe] What puts False before True?

PR Stanley prstanley at ntlworld.com
Tue Jun 5 01:39:20 EDT 2007

```Hello
What do the â‰¤ symbols represent?
Thanks,
Paul
At 06:21 05/06/2007, you wrote:
>On Tue, 2007-06-05 at 01:16 -0400, Albert Y. C. Lai wrote:
> > Scott Brickner wrote:
> > > It's actually not arbitrary.
> > [...]
> > > A â‰¤ B iff A âŠ† B
> > > A âŠ† B iff (x âˆŠ A) â‡’ (x âˆŠ B)
> >
> > Alternatively and dually but equally naturally,
> >
> > A â‰¥ B iff A âŠ† B iff (x âˆŠ A) â‡’ (x âˆŠ B)
> >
> > and then we would have False > True.
> >
> > Many of you are platonists rather than formalists; you have a strong
> > conviction in your intuition, and you call your intuition natural. You
> > think âˆ
â‰¤U is more natural than âˆ
â‰¥U
> because âˆ
has fewer elements than U.
> > (Why else would you consider it unnatural to associate â‰¥ with âŠ†?) But
> > that is only one of many natural intuitions.
> >
> > There are two kinds of natural intuitions: disjunctive ones and
> > conjunctive ones. The elementwise intuition above is a disjunctive one.
> > It says, we should declare {0}â‰¤{0,1} because {0} corresponds to the
> > predicate (x=0), {0,1} corresponds to the predicate (x=0 or x=1), you
> > see the latter has more disjuncts, so it should be a larger predicate.
> >
> > However, {0} and {0,1} are toy, artificial sets, tractible to enumerate
> > individuals. As designers of programs and systems, we deal with real,
> > natural sets, intractible to enumerate individuals. For example, when
> > you design a data type to be a Num instance, you write down two
> > QuickCheck properties:
> > x + y = y + x
> > x * y = y * x
> > And lo, you have specified a conjunction of two predicates! The more
> > properties (conjuncts) you add, the closer you get to âˆ
and further from
> > U, when you look at the set of legal behaviours. Therefore a conjunctive
> > intuition deduces âˆ
â‰¥U to be more natural.
>
>So as I said (not really directed at you Albert), there are intuitive
>reasons but no formal ones.  And incidentally, implication was one of
>the first things mentioned in the thread.
>
>_______________________________________________