[r6rs-discuss] Comparison procedures' number of arguments
r6rs at jdev.users.panix.com
Sun Oct 26 17:48:44 EDT 2008
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.
#!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;)))-)
More information about the r6rs-discuss