[Haskell-cafe] What puts False before True?

Derek Elkins derek.a.elkins at gmail.com
Tue Jun 5 01:21:52 EDT 2007

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.

More information about the Haskell-Cafe mailing list