[SCL] Re: SCL

[Pat Hayes]

>I noticed the following in the "SCL: Simple Common Logic" document.
>
>     (R @x)
>   
>    has the same meaning as the infinite conjunction:
>   
>    (and
>      (forall (x)(R x))
>      (forall (x y)(R x y))
>      (forall (x y z)(R x y z))
>      ... )
>
>    Strictly, one should also the 'trivial' case for zero arguments
>    (forall ( ) (R))
>    but since this is trivially true for any R it is omitted.
>
>
>
>I believe this is wrong.  Indeed, what you call the trivial case should
>be included as in
>    (and
>      (forall ()(R))
>      (forall (x)(R x))
>      (forall (x y)(R x y))
>      (forall (x y z)(R x y z))
>      ... )
>
>I believe you misinterpret the meaning of (forall ()(R)).
>You say it is trivially true, but I believe that
>    (forall ()(R))
>    (exists ()(R))
>    (R)
>should all be interpreted to have the same meaning.
>An empty variable list should not be interpreted to yield
>a vacuously true quantification.
>
>Thus, (forall ()(R)) in the expansion means (R), which should be included.
>After all, wouldn't you expect the meaning of (R @x) to be
>    (and
>      (R)
>      (forall (x) (R x))
>      (forall (x y) (R x y))
>      (forall (x y z) (R x y z))
>      ... )
>i.e. R is true of every sequence including the empty one?
>
>A rationale for this interpretation is that
>    (forall (x1 ... xn) F)
>means
>        (forall (x1) (forall (x2) ... (forall (xn) F) ...))
>i.e., F is embedded in one quantifier per variable.
>The n = 0 case with no quantified variables should be
>that (forall () F) means F.

Yes, you are right, thanks for pointing it out. I had 'checked' the 
semantics in my head while typing, and got it wrong (of course).  Now 
fixed.

Pat
-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes