[SCL] Identity and Horrocks sentences

[pat hayes]

>Greetings, Tanel.
>
>On Friday, May 30, 2003, at 05:14  PM, Tanel Tammet wrote:
>>>>Lemma:
>>>>
>>>>"Given a formula F in traditional FOL without equality and its
>>>>encoding enc(F) using App/Pred then: F is satisfiable in traditional
>>>>FOL iff enc(F) is satisfiable in traditional FOL, provided that the
>>>>following CONDITION holds: any first argument of App and Pred in
>>>>enc(F) is a constant."
>>>
>>>The condition here seems vacuous.  By hypothesis F is a formula of
>>>traditional FOL ("TFOL") w/o equality.  Hence, all expressions occurring
>>>in predicate position in F are constants.  Hence, the App/Pred
>>>translation of F can't possibly have a variable occurring as first
>>>argument to App or Pred.
>>
>>In one sense, yes. In another sense, the "encoding to App/Pred" is
>>not fixed: we may do it in slightly different ways. The encoding
>>might involve the addition of axioms, type conditions, etc.
>
>Not competely sure I understand, but ok.
>
>>>And the problem (as I understand it) is
>>>that the logical properties of a TFOL sentence can differ depending on
>>>whether it is interpreted via SCL or Tarski.  So it's not clear to me
>>>how a theorem about the equivalence of a TOFL sentence with its App/Pred
>>>encoding relates to this.
>>
>>This was the point of the letter: it suddenly seemed to me (and seems
>>still), that the logical properties of a TFOL sentence actually
>>DO NOT differ depending on whether is interpreted via SCL or Tarski.
>
>Ok, let's see.
>
>>If you axiomatise equality, instead of giving direct semantic conditions
>>for it, the differences in equality in TFOL and SCL become very clear.
>>See the following elaborations.
>>
>>>The connection between SCL and App/Pred encodings seems to me to be
>>>this.  In a full, unconstrained instance of SCL all predicates are also
>>>individual constants.  For such an instance, a sentence like
>>>(*)   (x)(Px <-> ~Qx) & (x,y)x=y
>>>is SCL-unsatisfiable but clearly Tarski-satisfiable.   However, the
>>>right thing to compare the above with (in some sense of "the right
>>>thing"!) is its App/Pred encoding:
>>>(**)  (x)(Pred(P,x) <-> ~Pred(Q,x)) & (x,y)x=y
>>>which is also unsatisfiable.  (I do not think identities should be
>>>encoded.)
>>
>>This is what I objected to: that the identities are not encoded.
>>Why aren't they? The identity is a predicate like any other, just
>>that it has to be axiomatised for each formula separately, using a
>>general schema.
>>
>>It occurred to me that (**) is NOT the right translation of a TFOL 
>>sentence (*)
>>at all.
>
>A bold claim!  The reason I am dubious, is that we want = to express 
>honest to goodness identity.  If it's translation doesn't express 
>honest to goodness identity, then it is not the right translation.
>
>>Let us use "eq" instead of "=" in the following, simply to avoid the
>>usual connotations of the "=" predicate.
>
>I'm already worried! :-)
>
>>When we write (*) HONESTLY in TFOL, it looks like this:
>>
>>(* honest)
>>
>>     (x)(Px <-> ~Qx) & (x,y)eq(x,y) &
>>     (x)  eq(x,x) &
>>     (x,y) eq(x,y) => eq(y,x) &
>>     (x,y,z) (eq(x,y) & eq(y,z)) => eq(x,z) &
>>     (x,y) (eq(x,y) => (P(x) <=> P(y))) &
>>     (x,y) (eq(x,y) => (Q(x) <=> Q(y)))
>
>I guess I don't see how this can be an HONEST rendering of (*) in 
>TFOL.  There is a model of this sentence on which there are many 
>things, as long as eq is an equivalence relation on the domain and 
>either everything is P and not Q, or vice versa.  That is a 
>DISHONEST rendering of (*)!  In particular, eq is simply an 
>untenable rendering of "=".  Things that are not identical can be 
>eq, and so any translation of (*) that renders identity as eq is 
>just plain wrong.  There is no wiggle room on this point, IMO.

Hey, guys, this is a textbook example of a classical clash of 
intuitions. You are both right :-) Chris is right if '=' is a logical 
symbol with a fixed semantics; Tamel is right if "=" is simply a 
binary predicate defined axiomatically (relative to a vocabulary). 
Seems to me that either intuition is OK, in fact, and that there is 
already a terminology to distinguish them: Tamel is talking about 
FOL, Chris is talking about FOL with equality.  We ought not to be 
surprised that these languages don't behave exactly similarly in 
matters like this, since they also don't behave exactly the same for 
such classical results as the upward Sk-L theorem, right?

In fact, I bet that this is an exact correspondence: a language has 
Horrocks sentences iff it does not satisfy the upward Sk-L theorem.

I wonder, do we have strong reasons for insisting that SCL is a 
language with equality? Logical equality (ie equality defined 
semantically to be true identity in all models) does provide us with 
some problems, in fact, apart from this issue. For example, our 
somewhat 'nonstandard' use of an extension mapping gives us an 
intensional view of relations. If equality were only required to be a 
substitutive equivalence (i.e. defined axiomatically) then we could 
allow models of our GOFOL sublanguage in which equality was 
interpreted over relations extensionally, and these would be 
perfectly correct SCL interpretations of the sublanguage.

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