[SCL] CORRECTION to the previous Horrock and equality message

[Tanel Tammet]

Hi Chris,

Chris Menzel wrote:
> Hi Tanel,
> 
> On Fri, May 30, 2003 at 03:18:08PM +0300, Tanel Tammet wrote:
> 
>>It occurred to me that perhaps we have all been over-excited by the
>>Horrock formulas a la (forall x. P(x) & -Q(x)) & (forall x,y. x=y).
>>
>>Maybe the problems these create are strawman problems, after all. I'll
>>elaborate in the rest of the email.
>>
>>I do not know if this is of any help, but at this point of discussion
>>I'd like to stress (has been done before on SCL list) that the core of
>>the problem seems to be the definition of the equality predicate, not
>>the App/Pred encoding in itself.
>>
>>First, the following lemma appears to be true:
>>
>>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.

> Also, I'm not quite sure how your lemma relates to Horrocks sentences,
> since the problem there has to do with SCL satisfiability vs "Tarski"
> satisfiability, and you appear only to be talking about Tarski
> satisfiability in the lemma. 

The lemma is a triviality. I wrote it up to avoid misunderstandings
in the latter part of email.

> 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.

Well - some minor properties differ  - but it appears that the important
properties we care about - like satisfiability and validity - do NOT
differ.

The seemingly different properties (satisfiability of our examples)
actually stem from the way equality is defined, not the SCL vs Tarski 
semantics.

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.

Let us use "eq" instead of "=" in the following, simply to avoid the
usual connotations of the "=" predicate.

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)))

The right translation of (* honest) to SCL is:

(***)  (x)(Pred(P,x) <-> ~Pred(Q,x)) & (x,y)Pred(eq,x,y) &
        (x)  Pred(eq,x,x) &
        (x,y) Pred(eq,x,y) => Pred(eq,y,x) &
        (x,y,z) (Pred(eq,x,y) & Pred(eq,y,z)) => Pred(eq,x,z) &
        (x,y) (Pred(eq,x,y) => (Pred(P,x) <=> Pred(P,y))) &
        (x,y) (Pred(eq,x,y) => (Pred(Q,x) <=> Pred(Q,y)))

The translation (**) simply translates "=" incorrectly,
ie it is not the "right thing".

The axiomatised version of (**) follows (named (****)):
(I use "eqscl" instead of "eq" in the following to avoid confusion):

(****) (x)(Pred(P,x) <-> ~Pred(Q,x)) & (x,y)eqscl(x,y) &
        (x)  eqscl(x,x) &
        (x,y) eqscl(x,y) => eqscl(y,x) &
        (x,y,z) (eqscl(x,y) & eqscl(y,z)) => eqscl(x,z) &
        (x,y,z) eqscl(x,y) => (Pred(x,z) <=> Pred(y,z))) &
        (x,y,z) eqscl(x,y) => (Pred(z,x) <=> Pred(z,y)))

Observe that the incorrect translation (****) is different
from (***) and violates the condition of the lemma.

> What we can then prove is that if A is any sentence in any
> instance of SCL, then A is SCL-satisfiable iff enc(A) is Tarski
> satisifiable.  Actually, we can prove something a lot stronger: we can
> take any SCL-interpretation in which A is true and transform it in a
> natural way into a Tarski interpretation that satisfies enc(A), and vice
> versa.
> 
> For my part, I'm still not clear on the practical upshot of this for
> Horrocks sentences.  Theoretically,  you want to say that a Horrocks
> sentence is just a pun: you pull a sentence out of one context where it
> is interpretated by one set of rules, and put it in another in which it
> is interpreted by another set.  

The observation made above is that the "context" is not the culprit:
the incorrect translation of the equality predicate is. With the
correct translation of the equality predicate the satisfiability
properties ARE preserved when the Horrocks formula is taken from a FOL
context and put into the SCL context.

Hence the App/Pred conversion seems to be perfectly OK.

>>Any formula F in FOL, when transformed to enc(F), will obviously yield
>>a form satisfying the conditions of the lemma: except that the "="
>>predicate, if present in F, will lead to problems.
>>
>>Depending on how we read "=" in the Horrock example, the example
>>violates either the condition: - being without equality, or - assuming
>>that "=" is just axiomatised and not a "built-in" predicate in
>>signature: "any first argument of App and Pred in enc(F) is a
>>constant"
> 
> 
> How does it violate the second condition?  Wouldn't the translation of
> x=y, if = is just another predicate, be Pred(=,x,y)?  (I *don't* think
> = should be translated, as indicated above.)

Pred(=,x,y) is IMHO the correct translation of a TFOL equality.

The second condition is violated if you translate the TFOL equality
to SCL equality: the substitution axioms of the SCL equality violate the
condition, see (****) above.

>>Let us assume that "=" means a suitably axiomatised predicate in FOL,
>>not a special built-in predicate.
>>
>>Ie, we add the following axioms to the example F, called (*): -
>>reflexivity, symmetry, transitivity - 
>>substitution axioms for the particular example, two needed:
> 
> 
>>forall x,y. (x=y => (P(x) <=> P(y)).
>>forall x,y. (x=y => (Q(x) <=> Q(y)).
>>
>>If we do the same for enc(F) we get the following axioms called 
>>(**) instead: - same reflexivity, symmetry, transitivity - 
>>different substitution axioms: 
>>forall x,y,z. (x=y => (Pred(x,z) <=> Pred(y,z))).
>>forall x,y,z. (x=y => (Pred(z,x) <=> Pred(z,y))).
> 
> 
> I don't get it.  How does this general substitution principle arise out
> of the axioms above?  Why aren't the corresponding axioms:
> 
> forall x,y. (x=y => (Pred(P,x) <=> Pred(P,y)).
> forall x,y. (x=y => (Pred(Q,x) <=> Pred(Q,y)).

I am not inventing anything here. The obvious explanation follows:

When you take a TFOL formula F and encode it using App/Pred to
enc(F), then you get a TFOL formula again: just a different
TFOL formula, this time containing App and Pred.

The equality predicate in TFOL has a standard axiomatisation,
and one important part of this is the set of substitution axioms.
As you know, we have to axiomatise substitution of equals for
equals into ALL argument positions of any predicate and function
symbol (we have just App and Pred in enc(F)). This is THE
way to axiomatise equality.

The axioms

forall x,y,z. (x=y => (Pred(x,z) <=> Pred(y,z))).
orall x,y,z. (x=y => (Pred(z,x) <=> Pred(z,y))).

are the correct substitution axioms in TFOL for an arity-two
predicate "Pred", while

forall x,y. (x=y => (Pred(P,x) <=> Pred(P,y)).
forall x,y. (x=y => (Pred(Q,x) <=> Pred(Q,y)).

obviously are not the correct substitution axioms for "Pred".

Think about equality as an ordinary predicate axiomatised
(not predefined in semantics at all) in a traditional way,
and no confusions arise.

To summarise: the "equality" predicate in a TFOL sentence F
has a different axiomatisation than the equality predicate
in its SCL encoding enc(F). Most importantly, the substitution
axioms are different. These are simply two different "equality"
predicates!

The "pun" of the Horrocks formula is a mistaken
translation of one "equality" predicate to another.


Regards,
         Tanel Tammet