[SCL] Re: Observation

[Chris Menzel]

On Fri, May 30, 2003 at 10:54:32AM -0500, Pat Hayes wrote:
> [Menzel wrote:]
> >The point Ian seemed to be making against SCL was that there are 
> >sentences in HIS familiar first-order language that suddenly change 
> >their logical properties when you interpret THAT VERY LANGUAGE via 
> >SCL model theory. Not so on our latest SCL model theory in which the 
> >relation between R and I is unspecified.  The logical properties of 
> >a traditional first-order SCL language are identical whether 
> >interpreted a la Tarski or a la SCL.  What you *can't* do is start 
> >with a gonzo type-free SCL language and expect that a superficially 
> >traditional first-order sentence ripped from that context will have 
> >the same logical properties when interpreted a la Tarski.
> 
> Ah, but that is what Ian WOULD expect. The point is that all 
> sentences one comes across are 'ripped' from their context in this 
> way: there are no contexts on the Web. There are only sentences. Or, 
> to put the same point differently, if it looks like first-order, then 
> it IS first-order. Or to put the point differently again: it must be 
> possible to recognize the intended context simply by parsing the 
> sentences. A file of sentences must be interpretable in one definite 
> way without any other information being made available that is not 
> somehow encoded in the form of the expressions in that file.  

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.  One could then only get a Horrocks
sentence in an inconsistent set (I think).  Thus, if you receive, say,
"(x)(Px <-> ~Qx) & (x,y)x=y", then you assume "P" and "Q" aren't also
individual constants and hence don't denote individuals.  No Horrocks
problem.  The only way to force them to denote would be add sentences to
the file in which "P" and "Q" occur as arguments.  But then the
resulting file would be provably inconsistent for pretty much standard
first-order reasons:  you'd be able to prove "P=Q" from "(x,y)x=y" and
"~P=Q" from "(x)(Px <-> ~Qx)" and the usual rules of identity.  (Suppose
"P=Q".  then by the substitutivity of identicals we have "(x)(Px <->
~Px)", which is easily shown to be contradictory in FOL.)

I think you were saying something like this on the phone the other day,
but I didn't grok it at the time.

> If this requires that the sublanguage in fact be a small subontology,
> as with the suggested use of Rel, then I reckon we ought to as far as
> possible absorb these little extensions in to the core language, so
> this ought to be scl:Rel and be given its semantic burden as part of
> the core model theory. That way, SCL has all the tools it requires to
> present its sublangauges to the world. I am pretty sure that we can do
> all the cases we are interested in with just a few of these: we
> decided a while back that Rel or something like it was going to be
> needed for GOFOL expressivity in any case, right?
> 
> 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.

> Maybe it would be better - I think we had this idea a while back - to
> use its complement as the primitive, so that scl:Ind is true of items
> in I that are NOT in R. 

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.

> This has the merit that one can take any expression written in
> GOFOL-SCL (we need a less insulting name for this subcase, btw) and
> map its content back into the full language by restricting its
> quantifiers with scl:Ind, providing a nice interoperability mapping
> between SCL and GOFOL. 

That might be an advantage for Ind -- though this will require some
terminology tweaking, as individuals in the model theory are all the
things in the domain of quantification, relations (the ones in both R
and I) included.

I'm working on the options here.

-chris