[SCL] two comments

[pat hayes]

Rather than drafting yet another version, let me put on record some 
of the changes Id like to see.  I'd be happy to attempt a rewrite 
when the text settles down.

First, as currently phrased the AS describes a lexicon as a 
collection of sets. I would prefer that we treat the AS as a purely 
abstract algebraic structure, in which the 'basic' items are 
considered to be grammatical categories - categories of expressions - 
rather than sets of syntactic entities. The makes no difference to 
the formal stuff but simplifies the AS and makes it more uniform, and 
avoids what is otherwise a potentially awkward set of issues 
concerning the 'status' of lexical items in some concrete SCL 
languages.

A concrete SCL language is then obtained by providing a 
'lexicalization' which provides for a set of wf expressions and a way 
to parse any such expression into an SCL AS structure.  Now we can 
distinguish two kinds of lexicalization: those in which the primitive 
syntactic elements (the things in the 'lexicon') can be recognized in 
isolation, and the others. Call the first 'local' for now. For 
example, a local lexicalization might write variables using a prefix 
?, relation names using initial uppercase, individuals using initial 
lowercase and no punctuation, and function symbols using the prefix 
'fun-', so that elements of each lexical category can be recognized 
in isolation, permitting easy parsing.  But a non-local 
lexicalization might not make any distinction between the lexical 
forms for individuals, functions and relation names, and rely 
entirely on the SCL grammatical context to assign these roles. In 
such a language, the Horrocks sentences are self-correcting, in a 
sense: if one writes

(x y) x=y & P(x) & not Q(x)

then x and y must be individual names, and P and Q must be relation 
names, but whether or not they are individual names is open. They 
might be, but there are no satisfying interpretations in which they 
are. But they also might not be, and so this is satisfiable by an 
interpretation which makes P and Q into relation names but not 
individual names.  But if we add

(x y) x=y & P(x) & not Q(y) & R(P,Q)

then it is no longer satisfiable, since this sentence only admits 
interpretations in which P and Q are classed as individual constants 
as well as relation names. But note, this is the *same* language, in 
this account: the language does not change when the extra conjunct is 
added, it just has fewer satisfying interpretations (as one would 
expect, of course).  P and Q are still in the category 'predicate 
constant'  as they were before, but they are now also required to be 
in the category 'individual constant'.

Chris, I know this is unconventional, but I think it is important to 
allow this flexible case without breaking the underlying SCL model , 
and in fact I think that it is actually easier to state things in 
this way (and it is more in the spirit of McCarthy's original AS 
proposal). It has the nice feature that when you use it everything 
gets simpler and nagging problems just go away, with no real cost, 
which is always the sign of having got something right :-).  Just 
forget the doctrine that a language *is* a set of strings. For us, a 
language *is* anything that can  be made to fit our AS structure. A 
concrete language defines how to parse things by SCL rules. If you 
can parse it, its legal; and if you can construct a satisfying 
interpretation on that parsing, its satisfiable. That is all we need.

Now, SFOL is a locally lexicalized syntax, of course, so these 
subtleties don't arise there. Tanel's worries about needing two 
versions of equality then appear in the following form. Consider the 
holds/app translation of SCL into SFOL: this maps everything into 
individual constants, thereby ruling out the SCL interpretations in 
which the relations aren't in the universe. In order to recapture the 
SCL flexibility, therefore, we need to modify the translation so that 
quantifiers are restricted to that part of the SFOL universe that 
corresponds to the FO part of the SCL universe, if you see what I 
mean.  On this view, then, the holds/app embedding needs to be 
extended to a holds/app/ind embedding, illustrated as follows:

(x y) x=y & P(x) & not Q(x)  -->  (x y)((ind(x) & ind(y)) implies 
x=y) & holds1(P,x) & not holds1(Q,y) & ind(x) & ind(y)

where it is left open whether or not ind(P) or ind(Q).  The extension 
of  'ind' then is the set of things that are in the SCL universe of 
discourse. The translation of the second example would have in 
addition

...  & holds2(R, P ,Q) & ind(P)  & ind(Q)

illustrating the inconsistency.

The same effect could be achieved by axioms of the form
holdsn(x y1 ... yn) implies ind(yi)
i.e. by embedding SCL into a FO theory rather than into SFOL itself, 
with a suitable modification to the statement of correspondence 
between full SCL and the holds/app translation.

However, contra Tanel, it seems to me that this is not really an 
issue requiring any changes to equality: rather, it is to do with the 
range of quantification. What it boils down to is that in the 
holds/app embedding, all quantifiers should be understood as 
restricted to a class which is not obliged to contain entities which 
occur only in the first argument position of any holds or app 
assertion. How this is best implemented in a conventional FOTP is a 
matter I will leave to Tanel to decide, but I do not think that we 
should describe it as a requirement for SCL to have two notions of 
equality.

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