[SCL] A few questions about the new SCL version

[Tanel Tammet]

Hi,

Chris Menzel wrote:

>I have made some changes that I believe make this whole question moot.
>Let's note a couple of things.  First, our constraints on an SCL lexicon
>*permit* but do not *require* that predicate constants also be
>individual constants.  Second, I've made sequence variables optional.
>(Consider this a proposal, not a decision by fiat from On High, but it
>seems pretty trivial to me).  The effect of these two features is that:
>
>(*)  Every traditional first-order language is an SCL language.
>
>Just keep your predicate constants, function symbols, and individual
>constants mutually disjoint and don't include sequence variables and
>there you go.  You'll have a fully conformant SCL language that is
>completely traditional.
>
>Now, an important change -- better, correction -- I've made to the 1.0
>document is to clobber the semantic condition that relations constitute
>a subset of the individuals in every interpretation of an SCL.  That
>does not square with our syntactic conditions above.  The appropriate
>condition is that we simply *permit* (partial or complete) overlap
>between the two classes; but they can be disjoint, and indeed that would
>be the most natural sort of interpretation for traditional first-order
>languages.
>
>Semantically, this has a very important consequence for the sorts of
>examples we've been looking at:
>
>(**)  For a traditional first-order SCL language L, the class of 
>      valid (hence, satisfiable) formulas relative to SCL model theory 
>      is exactly the class of valid (hence, satisfiable) formulas
>      relative to standard "Tarskian" model theory.
>
>Thus, we can't in general sensibly talk about whether or not a given
>formula is or isn't satisfiable independently of a specification of the
>signature of the language it purports to belong to.  So, for instance,
>In a traditional first-order SCL language in which "P" and "Q" are
>predicates only, 
>
>(***)  (forall x. P(x) & -Q(x)) & (forall x,y. x=y)
>
>IS satisfiable; 
>
...

>
>SCL 1.01, which incorporates the changes noted as well corrections of a
>number of errors spotted by Tanel's eagle eye, can be found at the usual
>place:  http://cl.tamu.edu/docs/scl/scl-latest.html .
>  
>
Great! Looked through the new version, and it seems to be significantly
clearer and - for several parts - easier to understand. The new feature
that the traditional FOL is an OK SCL language - semantics preserved -
is extremely nice, IMHO.

However, in the light of the goals of SCL, the previous versions of SCL
and all the discussions, I am unsure whether I understand some important 
parts of
the paper correctly though. So I'll simply ask for clarifications for
two questions in the rest of this email, without trying to say
what would be IMHO good or bad.

The first question: variables at the predicate position allowed
or not?

You write in the paper:

"For this we simply require that there be a one-to-one function *
Pred* on (/PredCon/ × /Trm/*) ? (/Con/ × /Trm/* × /SeqVar/); that is,
given a constant, /n/ terms, and -- optionally -- a sequence variable,
*Pred* returns a unique formula."

Does this mean that a formula like
forall x,y. x(y)
where a quantified variable x is used in the predicate position
is not legal in SCL, or have I misunderstood the paper?

It seems to me that unless one can use a quantified variable in the
predicate position, there is no point in allowing I and R
domains to overlap: cannot use the statements like "Commutative(P)"
for anything useful unless we can axiomatise
forall x,y,z. (Commutative(z) => (z(x,y) <=> z(y,x))).

Perhaps I should have interpreted the constructor
*"Pred* on (/PredCon/ × /Trm/*) ? (/Con/ × /Trm/* × /SeqVar/)"
as saying that "variable can occur in the predicate position
only in case the variable is generated from the SeqVar",
ie one has to use SeqVars to get the RDFS-ish semantics
and write axioms like the commutative-predicate axiom
above?

I am simply worried that I may interpret the issue
described in the paper incorrectly. What is the right
way to understand it?

The second question: different SCL languages in practice.

How does one in practice say whether we use a traditional FOL semantics
or free semantics. Ie, if we take the same example

(***)  (forall x. P(x) & -Q(x)) & (forall x,y. x=y)

and now want to interpret it in the nonstandard way that P and Q
are in the set I of ordinary objects, quantified over (as it seems
to be the natural way for RDF). 

We should then say that the predicate
domain R is a subset of the domain I of individual constants. But
how exactly do we say that in some particular concrete syntax?

Perhaps the seqvars have to be used to get the App/Pred
semantics?

If we could get the nontraditional semantics without seqvars,
then the question remains:

It seems that we could define different concrete languages with
concrete syntaxes on top of SCL. One language, say, "traditional"
would have a traditional semantics, while another language,
say, "RDFSplus" would have the I=R semantics. 

Did you have something like this in mind?

Alternatively, one could imagine that we assume that
an implementation looks at the actual formulas it gets.
It can easily detect whether some lexical entity is
used both in a predicate position and as argument
to some predicate/function, or a quantified variable
is used in the predicate/function position.

If it notices this nonstandard use of the lexicon, it
will use either I=R (or a partial overlap between I and R),
otherwise it will assume that I is distinct from R.

Let me bring some examples to make my question
about the implementation-detected semantics option clearer:

Given
(***)  (forall x. P(x) & -Q(x)) & (forall x,y. x=y)
the implementation would determine that traditional semantics
is used and (***) is satisfiable.

Given
(****)  R(P) & R(Q) & (forall x. P(x) & -Q(x)) & (forall x,y. x=y)
it will detect that nontraditional semantics is used
and (****) is NOT satisfiable.

Again, which approach did you have in mind?

Regards,
        Tanel Tammet




-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20030526/0d4d8ba5/attachment.htm