[Haskell-cafe] What puts False before True?

[Scott Brickner]

You're right. I didn't put that precisely enough. But, the inverse of 
/any/ partial order is still a partial order.

With the set of natural numbers, is it still reasonable to say that the 
order that puts 2 ≤ 1 is "just as natural" as the conventional order? 
Probably not.

So, ⊆ is the /conventional/ order for sets, ⇒ is the conventional order 
for predicates, ≤ is the conventional order for numbers, and so on. That 
still dictates that False < True is the conventional order for booleans.

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.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe


-- 
-----
What part of "ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn" don't you understand?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070605/646d78f6/attachment.htm