[SCL] Re: Observation

[Chris Menzel]

On Sun, Jun 01, 2003 at 11:47:08AM +0300, Tanel Tammet wrote:
> 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.
> 
> 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. 

Yes, of course, we've known that from the beginning, but the problem is
that the meaning of a sentence might change.  My impression from Pat's
comments and from his discussions with Ian is that there would be some
stiff resistance in the semantic web community to the idea that familiar
formulas of TFOL don't *really* express what folks think they do, but
rather need to be run through the App/Pred transmogrifier before their
True Logical Form is made manifest.  That might look so some folks as if
we've hijacked TFOL without their consent.  On the current SCL semantics
the meanings of TFOL sentences are undisturbed.  An App/Pred translation
is necessary only in contexts where one is knowingly taking advantage of
features of SCL, in which case the App/Pred translation will be
meaning-preserving.

> Horrock formulas are a strawman (Chris was not convinced, but neither
> had he any serious objections).

No serious objections to your proposal?  I don't know what could be more
serious than that distinct things could end up being "identical".
(Granted, I have not had time to look in detail at your latest response
on this issue yet.)

> Most importantly, there seems to be NO difference between TFOL
> formulas (out of context or not) and core SCL formulas 

There is if identity is part of the core.  And it should be if it isn't.

> Core SCL is a subset of TFOL: a restricted signature
> for predicate and function symbols. 

The *language* is; but logical properties can differ depending on the
semantics.

> Not anything stronger.  Paradoxically, weaker: every core SCL formula
> is a TFOL formula...

TFOL predicates have fixed arity; SCL predicates don't, so we can't say
that an SCL formula is a TFOL formula without some qualification.

> 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.

Sure, but this doesn't address the concern above, if is is a concern.

-chris