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