[SCL] Re: Observation

[Tanel Tammet]

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

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. Then, how are
people supposed to use these predicates? Also,
how are the systems going to decide Rel and Ind?

Regards,
          Tanel Tammet