[SCL] Re: Update to SCL-related work

[Pat Hayes]

Tanel, a quick amplification of a point in the last email:

>>- Equality confusion solved.
>
>I really don't think there is any equality confusion. Equality means 
>what it usually means, i.e. I('x=y') = true when I(x)=I(y). The 
>issue you have always raised is not two kinds of equality, but two 
>notions of what is in the universe (GOFOL individuals only, or also 
>including relations). This can be expressed in terms of equality 
>since (x exists) is the same as (x=x) , but that is misleading. 
>Equality is the same on both universes: there aren't two notions of 
>equality.
>
>>As it stands
>>   now, many of the complexities in the
>>   semantics seem to be motivated by the
>>   desire to fight the Horrocks sentences,
>>   which is purely a problem with equality
>>   axiomatisation.
>
>It runs deeper than this. Its a problem with the size of the 
>universe. Its true that without equality there is no way to 
>axiomatically enforce a finite universe, so the examples all use 
>equality, but the meta-theoretic point they illustrate holds true 
>even for the logic without equality. What we want is that if some 
>SCL text is GOFOL, then its FO models are among its SCL models. The 
>Horrocks sentences illustrate the objection that with the former SCL 
>semantics, this is not the case (because the relations had to be in 
>the universe).  It would still be a valid objection in the logic 
>without equality. That is what was unacceptable (and is now fixed), 
>not a specific equality issue.

To illustrate, consider the single FO sentence in SCL notation

(P a)

and its embedding into FOL using the ECL format:

Atom_2(P, a)

and consider the FO-valid inference rule of existential 
generalization (in an ND system), which applies to the latter to 
produce the valid FO consequence

(exists (x) Atom_2(x, a) )

which is NOT a correct translation of any FO consequence of the 
original sentence. So the translation fails to accurately capture FO 
logic.

This exhibits the issue without using equality, and illustrates why 
it is essentially a matter of what is in the universe. By using the 
relation names as true FO names in a classical FO framework, we have 
required them to denote something in the universe of quantification.

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