[SCL] Re: Observation

[pat hayes]

>>Right.  Slightly odd suggestion: make Rel be true of all sequences 
>>of things in the intersection of I and R, and make it be false 
>>(even of the empty sequence) if there aren't any.  That way, one 
>>could write Rel(P Q R ...) to 'declare' a lot of them at once, and 
>>more pointedly, (not Rel( ) ) is true inside GOFOL, not otherwise. 
>>so it can be used to say that one is inside the GOFOL sublanguage.
>
>Can do that.

But read on before you do :-)

>
>>>I think we were a little unclear on the following point yesterday.  So
>>>long as "P" has been designated a constant in our particular SCL
>>>language, we get all theorems of the form:
>>>
>>>...P... -> (EF)...F...
>>>
>>>e.g.,
>>>
>>>Px -> (EF)Fx
>>>
>>>regardless of whether or not "P" occurs as an argument to another
>>>predicate in our axioms somewhere.
>>
>>Seems to me that this brings back the Horrocks sentences.
>
>No, not for "traditional" first-order SCL languages, i.e., SCL 
>languages in which no predicate constants are simultaneously 
>individual constants (and in which one does not allow variables in 
>pred position).

We really have to stop talking in this way. There really is only one 
SCL language, which can be used with various vocabularies. If some 
property of a sublanguage is different from that property of the full 
language in a way which is semantically visible, then the sublanguage 
needs to be clearly recognizable in some way.

>  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.  To make 
that possible is the minimal task of a web-logic syntax and model 
theory. Now, in addition, there are  strong engineering reasons why 
this should not be done by having 'headers', since that requires 
information to be conveyed only in large file-size units, which is 
anathematic to the basic design assumptions of the semantic web. So 
we are winning when we can provide a single model theory that works 
for all SCL expressions without any further stipulations; SCL 
sublanguages can be recognized simply by parsers, ie are defined 
purely by local syntactic constraints, and moreover those 
sublanguages have a semantics which is (isomorphic to) the SCL 
semantics restricted to the syntactic subcase (ie if the syntactic 
restriction automatically encodes any . 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.  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. Then the GOFOL axiom 
is (forall (?x)(scl:Ind(?x)) and the quantifier is GOF-ok; and 
outside GOFOL we can define Rel by
Rel(?x) iff not scl:Ind(?x)
(and then for sequences by the usual induction, if required.)
That avoids the need for that odd empty-case hack and the potentially 
problematic use of a nullary relation, which might break many 
conventional FOL parsers. In the GOFOL model theory that axiom is 
vacuously true, but in SCL it serves to restrict the satisfying 
interpretations to those which are  isomorphic to GOFOL 
interpretations.

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. (The reverse mapping makes the restrictions 
vacuous because of the GOFOL axiom.) This is actually one case of a 
more general phenomenon, which is to map between SCL ontologies A and 
B by restricting the quantifiers in A  to the universe of A described 
in B.

>  But I can't see that THAT is any more problematic than the fact 
>that you can't rip an arbitrary sentence out of a context in which 
>it is interpreted according to the model theory for, say, free logic 
>and complain that its logical properties are different interpreted a 
>la Tarski.

You could complain if one of these was already an accepted standard 
and the other came along with an identical syntax but a divergent 
semantics. That would be an engineering/interoperability disaster and 
one of them (probably the later arriviste) would almost certainly be 
changed to avoid this situation. There are high-level engineering 
coordinating committee structures in place to look out for such 
disasters and to prevent them happening, eg the W3C TAG group.

>  If you want to pull a sentence from an arbitrary SCL language into 
>a traditional first-order framework, you'll have to use an App/Pred 
>translator or restricted quantifiers.
>
>>>Being a possible argument is not a
>>>property conferred upon an expression in real time, so to say, but ahead
>>>of time in virtue, before we write anything down, in virtue of
>>>stipulating that the given expression is a constant.
>>
>>Well, Im not sure what this stipulating amounts to.
>
>Same as with any language.  This is the standard way in which a 
>language is defined.  Granted, we're thinking about the web where 
>these matters aren't always so neat...

Yes. You and I constantly get into trouble over this point. I know 
this is the 'standard' way in logic textbooks that this is done, but 
those textbook uses of logic just assume it is being used by some guy 
with a pencil somewhere.  The world has changed. To hell with it 
being a "standard" way: the question is, does it make sense in our 
context? And the answer is no, and moreover it hasnt made sense ever 
since formal logics were first put into computers, but it hasnt 
really mattered until the Web arrived, so nobody made much of a fuss 
about it. The textbook writers don't know computation from a hole in 
the ground and the computational logicians just quietly ignored this 
way of talking. But the idea that a particular vocabulary defines a 
unique 'language' is silly when one is writing parsers and inference 
engines which work for all such 'languages' (its like saying that 
every set of Java identifiers defines a new programming language) and 
it becomes downright mistaken when one is writing code which is 
expected to deal with syntactically correct SCL arriving from 
anywhere on the planet. Vocabularies are just not part of what can be 
built-in: we cannot POSSIBLY have each  vocabulary is considered to 
be a distinct language with potentially its own semantics. We are 
trying to define a format in which logics can be used as a basis for 
*communication*, right?

(BTW, this logician's use of the word 'language' is a local 
aberration in any case; it doesnt fit with the way that 'language' is 
used in linguistics, for example, and it doesnt fit with the way that 
formal logic is used to model and describe mathematics; we don't 
usually consider that a mathematician who says, 'let S be a set' is 
defining a new 'language'. )

>>Like, here I am, a softbot somewhere, and I come across a piece of 
>>SCL: how do I know which of the relation symbols have been 
>>designated a constant? Designated where, and by who? I think we 
>>have to have some way of recognizing from the syntax how to 
>>interpret the language. If that requires knowing what has been 
>>stipulated, then the syntax has to have a way to indicate 
>>stipulation.
>
>I think that is exactly what we will have to say, else there will be 
>no way out to avoid Horrocks sentences.

I really think we can do better than that. In fact, I think you 
already DID do it better :-)

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 ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam