[Haskell-cafe] What puts False before True?

[Derek Elkins]

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.