[SCL] Pred vars

[Chris Menzel]

SCLers,

The introduction of predicate variables forces a couple of decisions.
Currently we don't require the set R of relations to be a subset of the
set I of individuals.  This may no longer feasible with predicate
variables in the mix.  The reason for this is that we have to allow pred
vars to occur in subject position in order to be able to say things
that we really want to be able to say like:

  (F)(Symmetric(F) -> (x,y)(F(x,y) -> F(y,x)))

But with a classical semantics, we have to have a guarantee that terms
occurring in argument position denote something.  Hence, it seems that
the only way we can guarantee that (without some monstrous kludge) is to
stipulate that R is a subset of I in every interpretation.

This of course reintroduces the question of first-order "Horrocks"-
sentences like 

  (x)(Px <-> ~Qx) -> ~(x,y)x=y

whose logical properties under SCL's semantics differ from their
logical properties under Tarskian semantics.

My own self, I don't find this a particularly noisome problem, though it
is obviously off-putting to some people -- notably Ian.  Fact is,
KR generally needs to be able to quantify over properties and relations,
and also treat them as first-class citizens, i.e., to stay first-order.
To do it right, you either need to use SCL, which offers a more faithful
representation of this "dual role" of properties and relations, or you
need to mask their predicative nature and move to an "App/Pred"
framework predicates are replaced by constants and there is only one
function symbol "App" and infinitely many n-place predicates "App_n",
for all n (or for as many n as you need).

I actually think the more uniform SCL semantics (R always a subset of I)
brings more order to things anyway.  When a standard first-order
language can count as an SCL language, there is no telling in general
what the semantics of a sentence should be from its logical form --
Horrocks-sentences being the most dramatic cases of this.  On the
uniform appraoch, a sentence from an SCL language always has the same
semantics in any interepretation.  If one wants pure first-order, one
*always* translates to an App/Pred language.

Of course, we still want a notion of SCL conformance, and I think the
idea of an SCL-conformant *sublanguage* can be used for that (see the
implementation of this in the CL document).

Comments?

-chris