[SCL] proposition variables in SCL??

[Bill Andersen]

Hi, Pat

See below.

> Here's how it would go: a name P can now have *three* kinds of 
> extension: a truth-value, a relation(al extension) and a function; and 
> they all can be 'folded' onto the denotation of the name. You CAN 
> write things like
> (iff P (P))
> but you aren't obliged to specify any connection. And you can (that 
> is, it makes semantic sense to) write things like
> (exists (P)  P)
> which could even be false in some interpretations. As far as I can 
> see, this introduces no new tautologies.

I could certainly use something like this.  If one wants to do things 
like a 'holds in' kind of temporal
model.  For example...

      (=> (and (holdsIn T Phi) (subInterval T T'))
            (holdsIn T' Phi))

where Phi is some proposition, this could be useful.  We'd need 
propositions to provide signatures
for predicates like holdsIn.  A general capability like this would have 
to extend to propositions that
can't be represented by a simple constant.

    .bill