[SCL] Re: Observation

[pat hayes]

>Chris Menzel wrote:
>
>>Well, how about then that parsers default to the least amount of
>>type-freedom?  That is, reasoners/parsers/etc receiving a file should
>>assume that a predicate is NOT an individual constant unless it is used
>>explicitly as such in that file.
>...
>>>BTW, yet another tweak occurs to me. Having Rel in GOFOL as a
>>>predicate is illegal of course since there isnt anything there for it
>>>to be predicated of.
>>
>>
>>Oh but there is -- it is true of exactly those individuals that are
>>relations.
>...
>>Can do it either way, but Rel strikes me as perhaps conceptually
>>preferable, since the fact that relations are relations is what
>>distinguishes them from other individuals.
>
>I must say that I am slightly confused about the discussion
>you and Pat are having here.

Fair enough. There are several agendas being pursued here, I confess, 
and they havnt been stated clearly and explicitly.

Let me try to sketch the 'vision' I am trying to achieve.

As we all know, SCL generalizes GOFOL in some ways.  There are at 
least two relationships between SCL and GOFOL:

(inclusion) GOFOL is simply a subset of SCL syntax: every GOFOL 
sentence is an SCL sentence

(embedded) There is a mapping from SCL into a GOFOL sublanguage 
(using App/Holds).

Obviously we can go back and forth between GOFOL and SCL in several 
ways using these, eg one can start with a GOFOL sentence, think of it 
as SCL, then embed it back into GOFOL using App/Holds. And as your 
debate with Chris illustrates, you tend to get different results for 
GOFOL and GOFOL+=, but let me leave that aside for now.  The issue 
that I am concerned with is essentially a political one. IN the past 
I claimed, rather strenuously, in some quarters that SCL was 
essentially FOL semantically, in that the GOFOL subcase of SCL 
actually *was* FOL and that the semantics generalized naturally - 
this was the 'inclusion' idea; and that the embedding using App/Holds 
made a slightly different point, which was that the standard 
inferential machinery used for all FOL thoeremprovers was adequate 
for SCL also, since one could simply use the FOL embedding inside the 
implementation. These are two rather different claims, however: the 
second was essentially an existence proof that SCL introduced no new 
(and ill-understood) *computational* problems; it was not intended to 
be a serious proposal to be a normative way of using SCL. In many 
ways, the entire CL/SCL effort has been motivated by the desire to 
*avoid* forcing users to write formulae in this ugly and unnatural 
form, and to instead give them the ability to write sentences in 
conventional FOL form but with greater syntactic freedom, ie to 
preserve the intuitive form of the usual FOL sentences while also 
being able to quantify over relations. The point being that this 
doesn't invoke any dreadful higher-order demons or paradoxical 
consequences, as many people  - notably Horrocks - have claimed (and 
are still claiming).

The form this debate has taken in the semantic web effort is what I 
can only describe as an organized campaign orchestrated by Horrocks 
and Peter Patel-Schneider to resist  any extension to what might be 
called 'conventional FOL' in any SW standard.  Since I based the RDF 
semantics on the CL work, this has taken the form of an extended 
resistance to any influence of RDF on the design of OWL, which has 
been seriously disruptive to the OWL effort and is likely to continue 
to be so. I confess to having been surprised by both the energy and 
passion which has been devoted to this campaign: it has found its way 
even into the choice of wording in the OWL documentation, which is 
riddled with phrases which seem to be directly motivated by this need 
to preserve OWL from any taint of the RDF 'nonstandardness'. I 
mention this only to convey some of the reasons why this matter is 
seen as worthy of taking seriously: they are more political than 
technical. In the context of this debate, Ian Horrocks' example, 
which was indeed a counterexample to my claim that the inclusion was 
*semantically* transparent, was rather shocking; since he first 
mentioned it, it has been repeatedly used by Horrocks and 
Patel-Schneider as an example (in a published paper, many email 
discussions, and I gather was mentioned by Horrocks in the recent 
Budapest meeting) to justify the reiterated claim that SCL is not 
'fully understood' or is 'nonstandard'. (The intensity of this debate 
can perhaps be judged from the fact that no mention has been made of 
any of the archived email discussion of the example, even though it 
pre-dates the writing of the Budapest paper by several months.)

So the issue of the Horrocks sentences isn't really to do with the 
embedding, but the inclusion.  I thought that the best we could do 
was to adapt the embedding claim by restricting the FOL quantifiers 
in SCL-GOFOL; but the great merit of Chris' suggested MT modification 
is that it removes even that snag, and makes the embedding claim 
strictly and exactly correct: with this MT, the GOFOL subset of SCL 
is *exactly* the same logic as FOL, with exactly the same 
satisfaction and entailment properties.  The cost, and I think it is 
very small, is that one cannot be sure that a relational quantifier 
in non-GOFOL SCL ranges over all mentioned properties, eg the 
following would be consistent:
P(a) and not (exists (?r)(?r(a))
but it would not be if one were to add
Q(P)
and one can assert that any relation which holds between any number 
of individuals is an individual as follows:
  ?r(@x) implies Thing(?r)
This provides an inference path from any term R(t1...tn) to Thing(R), 
thereby ensuring that any relation named in a positive assertion is 
in the domain of discourse.

BTW, re. my recent message: the above holds for FOL and FOL+=; but if 
we interpret equality axiomatically, then we can state the 
correspondence even more tightly, since there is a 1:1 mapping 
between the actual models of SCL-GOFOL  and the conventional textbook 
MT models. It makes no difference for the entailments, of course.

Hope this helps explain some of the background/context.

>
>It sounds like the Rel/Ind predicates, quantifier types,
>Horrock stuff etc are highly important and we have to find
>a clever way out of the mess they potentially create.
>
>IMHO these things WOULD be complex in case
>(a) we hadn't decided on the kind of App/Pred encoding
>    as we seem to have decided upon, or
>(b) it were true that Horrock sentences pose
>     a fundamental problem (appears not to be true).
>As we stand now the things appear to be rather simple.
>
>Take a formula F and convert it using App/Pred. Nothing
>bad will happen. Satisfiability is preserved. Horrock
>formulas are a strawman (Chris was not convinced, but
>neither had he any serious objections).
>
>Most importantly, there seems to be NO difference
>between TFOL formulas (out of context or not) and
>core SCL formulas ("core" meaning that various
>extensions like arithmetic are not present in the
>formula). Quite recently Pat claimed just that.
>
>Core SCL is a subset of TFOL: a restricted signature
>for predicate and function symbols. Not anything stronger.
>Paradoxically, weaker: every core SCL formula is a TFOL
>formula, but not vice versa.
>
>A parser sees a formula like "forall x. P(f(x))"
>and ALWAYS converts it to "forall x. Pred(P,App(f,x))."
>No need whatsoever to guess if the "forall x. P(f(x))"
>was in TFOL or SCL: there is no difference.
>"forall x. x(x)" is converted in the same way.

Right; that is the implementation inside traditional TFOL (GOFOL) 
mapping, using the embedding. I want to have it both ways, though :-) 
And surely, even on purely pragmatic grounds, it might be nice to 
know that you don't need to map it in this way? Eg suppose you have 
something already written in TFOL, do you need to re-render it into 
this form in order to use SCL? I would prefer not (though it is 
always an option, of course, as it always has been.)

>
>The parser does not have to wonder that in one case
>we had no variables in the predicate positon and
>in the other case we had. No need for special
>declarations either.
>
>Wrote this up (despite that we all know this),
>simply because I do not really understand the motivation
>for Ind and Rel predicates and questions
>about "the least amount of type freedom"
>in the current SCL context.
>
>Suppose we put Rel/Ind into the SCL signature
>and give them a specific meaning.

Well, we will need several such things, so why not? Although I guess 
there is some utility in having a core-core which is completely free 
of all signatures, Im worried about the specification getting to be 
too 'multi-layered' if we try to keep things too logically pure. I 
ask myself: is there any justification for making this distinction in 
an actual use case, or is being done just for aesthetic reasons?

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