[SCL] Re: Observation

[pat hayes]

Chris: copying this to SCL, hope you don't mind.

>Note that on our new semantics there is no way to force R to be a subset
>of I.  More generally, we can't put constraints on all relations the way
>we could with true pred quantification.  However, I do think it will
>probably be worthwhile to introduce a "Rel" predicate true of those
>individuals that are also relations (i.e., "Rel" denotes the
>intersection of R and I).

Right.  Slightly odd suggestion: make Rel be true of all sequences of 
things in the intersection of I and R, and make it be false (even of 
the empty sequence) if there aren't any.  That way, one could write 
Rel(P Q R ...) to 'declare' a lot of them at once, and more 
pointedly, (not Rel( ) ) is true inside GOFOL, not otherwise. so it 
can be used to say that one is inside the GOFOL sublanguage. Note 
that this last one doesn't require any non-GOFOL quantifiers, so it 
is legal GOFOL :-) .  Outside GOFOL, we have

(exists (?x) Rel(?x) ) iff Rel( )

and

Rel(?x @y) iff ( Rel(?x) and Rel(@y) )

neither of which are syntactically legal in GOFOL, so their failure 
to mean the same thing there doesn't matter ;-)

>I think we were a little unclear on the following point yesterday.  So
>long as "P" has been designated a constant in our particular SCL
>language, we get all theorems of the form:
>
>...P... -> (EF)...F...
>
>e.g.,
>
>Px -> (EF)Fx
>
>regardless of whether or not "P" occurs as an argument to another
>predicate in our axioms somewhere.

Seems to me that this brings back the Horrocks sentences. So 
conformity to GOFOL just becomes a matter of stipulation. We could 
have done that long ago, right?

>Being a possible argument is not a
>property conferred upon an expression in real time, so to say, but ahead
>of time in virtue, before we write anything down, in virtue of
>stipulating that the given expression is a constant.

Well, Im not sure what this stipulating amounts to. Like, here I am, 
a softbot somewhere, and I come across a piece of SCL: how do I know 
which of the relation symbols have been designated a constant? 
Designated where, and by who? I think we have to have some way of 
recognizing from the syntax how to interpret the language. If that 
requires knowing what has been stipulated, then the syntax has to 
have a way to indicate stipulation.

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 ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam