On Mon, Oct 20, 2008 at 06:14:47PM -0400, John Cowan wrote: > > ObDigression: This is only true on the assumption of unrestricted > quantification, which translates "All witches are green" as (Ax)(Wx->Gx). > We call this kind of quantification unrestricted because it quantifies > over all objects whatsoever, and then makes the claim "if a witch, then > green" which is equivalent to "either not a witch or green", which is > obviously true in a universe in which all objects are not witches. > > Restricted quantification, however, is (AWx)(Gx), and is *false* if > there are no witches, just as "Each rhinoceros in my workplace is painted > purple" is false. There are no such rhinocerotes, and so the claim fails.
Ah, but the corresponding item using the typed quantification of the Calculus of Inductive Constructions, or presumably any other flavor of intuitionistic type theory, is *true* -- to prove something of the form "forall x : Witch, ...", one can begin with "lambda x : Witch, ...", and then apply the "there are no witches" axiom (which has type "Witch -> False") to this alleged witch "x" and obtain a proof of false, from which anything (including the greenness of that witch) can be derived; /ex falso quodlibet/ is just a special case of structural induction. I will now prepare myself for the torch- and pitchfork-wielding mob that will result from bringing a typed lambda calculus into a Scheme list, to say nothing of extending this remarkably long thread by one more post. -- #!/usr/bin/env scheme-script #!r6rs (import (rename (rnrs) (lambda \x3bb;) (set! \x5316;))) ((\x3bb; ':['"JdDvs" '"e ai\n"]) (\x3bb; (\x3a3;) (\x3bb; (set!) (string-for-each (\x3bb; (\x3c7;) (display \x3c7;) (\x5316; set! (call/cc set!))) \x3a3;)))-) _______________________________________________ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
