[SCL] Re: SCL 1.02: more reasons to avoid ind pred separation

[pat hayes]

>Hi Chris and Pat,
>
>After sending the previous letter a few hours ago
>about why ind/pred separation in IMHO bad,
>I thought a bit about other aspects than were
>described in the previous letter (please read
>the previous one first: the main reasons are
>outlined there).
>
>Wanted to mention the usefulness aspect
>of ind/pred separation: what could it BUY
>us what we cannot get without this separation
>(on the non-political, real-user level)?
>
>As far as I understand, if the user wants
>to keep clear separation of ind/pred constants,
>then there are several obvious, intuitive ways
>to do that.
>
>First, one can simply NEVER USE a non-constant
>term in the first position of the triple.
>
>No axioms of the kind
>
>(forall x. reflective(x) <=> forall y. z. x(y) <=> z(y)).
>
>and no terms in the first position, ie no f(x)(y).

But, but.  Consider this *syntactic* case simply as a grammatical 
restriction on the SCL language - case A - and as a standard FOL in 
its own right - case B.  Are these the same case? We used to think 
so, but that was exactly Horrock's point with his example: they are 
not the same, if we use the 'simple' version of SCL in which all 
symbols - even those in relation position - denote something in the 
universe. Even if they don't occur in the 'name' position, they still 
*denote*, so saying P(x) makes there be a P-thing in the universe. 
So just refraining from using the extended SCL syntax does not - with 
our old, simple, version of SCL - automatically buy you a genuine 
conventional FO= language. It looks like GOFOL=, but it isn't quite 
the same (the Horrocks sentence case).  So, one is led to consider 
how to arrange things in SCL so that simply by refraining from using 
any syntactic case other than GOFOL, an SCL user automatically gets 
the conventional FO interpretations, in which the universe of 
quantification is restricted (as it seems from an SCL perspective) to 
the non-relational things which are denoted by expressions in the 
'conventional first-order position' in the syntax. The only change 
that is needed is to say that the universe of discourse is not 
*required* to contain all relations: in the abstract SCL core that is 
a remarkably small change.

Other options we did briefly consider were:
(1) just basically saying, tough: SCL restricted to GOFOL syntax 
isn't quite exactly traditional FOL: put up with it and get used to 
case A. Obvious snag: unacceptable to users. (I think this is what 
your suggestion amounts to. I agree it is more elegant and easier for 
us, but it sends the Jeff Pans and Ian Horrockses of this world into 
a terrible tizzy.)
(2) saying that the FOL syntactic subset was a distinct language with 
a FOL-restriced model theory, ie if it looks like case B, it is case 
B. Obvious snag: having two model theories nullifies main design aims 
of SCL.
Neither of these is anywhere as nearly attractive as the one we are 
pursuing, seems to me.

For practical users of many persuasions, I think case A is in fact 
quite acceptable, and we can present it as a useable alternative 
which allows the simplicity of a single-sorted FOL embedding and 
perhaps the cost of using two equalities, as you have suggested. I 
think it works in the no-equality case, so we only need the 
two-sorted SFOL embedding for the logic with equality and even then 
only if you care about Horrocks sentences. This needs to be checked 
carefully but I think it works out OK.

>Second, if one sometimes wants to use variables
>in the first position and STILL be able to separate
>ind/pred constants, then one can easily axiomatise
>it oneself, simply taking axioms like:
>
>ind(pat).
>ind(chris).
>pred(father).
>etc
>
>and then use these axioms explicitly.

Yes, but all the art is in providing a way so that just doing this in 
the language automatically makes the model theory come out as 
required. If you can see how to do this, please don't keep it to 
yourself :-)

In haste

Pat


>
>One can obviously restrict quantification
>explicitly, like this:
>
>forall x. pred(x) => ....
>
>We even have a special syntax for restricted
>quantification, so that the last example can be
>more conveniently written as
>
>forall x:pred. =>
>
>One can also give explicit rules for deriving information
>about what is predicate, for example, like this:
>
>forall x, y. x(y) => pred(x).
>
>Now, in case you build in the separation into
>the language and MT, you FORCE a specific scheme
>of separating ind/pred on the user, but you give
>the user nothing really sensible she could not
>do herself. And, if by any chance there is something
>which she cannot (at least easily) do herself,
>she WILL NOT UNDERSTAND the scheme
>you impose. Rhetorically: either your scheme is simple
>and understandable (in which case it can be done
>explicitly) or it is ununderstandable for an
>ordinary user (in which case it brings down
>the whole MT and SCL along with it).
>
>All this again points to that the formal
>ind/pred separation should either:
>
>- be abolished from the SCL spec altogether

It isnt in the central SCL spec. It arises only when we consider how 
to embed SCL into GOFOL syntax. That is the only place we need to 
consider any of these issues.

>
>- or brought in a special module (like we bring
>    in annotations and equality (at least the
>   SFOL-translation equality) as special ind
>   and  pred and fun predicates, just explicitly
>  axiomatised.
>
>- or described in a later special notes appendix
>
>As you see, I am very much against putting ind/pred
>separation (constants of different types in general)
>into scl core semantics or syntax.

The issue arises more when one asks what set the variables range over.

>
>If you really want them, please put them into somewhere
>non-core only, with explicit axioms or usage suggestions,
>where they do no harm.
>
>We can still speak about predicates, of course,
>in a non-formal way in the SCL spec, just like
>we speak about "predicates" or "properties"
>in the RDF context, typically meaning "something
>which is located in the first element of the atom tuple",
>but this is a convention, not a rule.
>
>Regards,
>            Tanel Tammet


-- 
---------------------------------------------------------------------
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 ihmc.us       http://www.ihmc.us/users/phayes