[SCL] Identity and Horrocks sentences

[Christopher Menzel]

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.

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

It still looks exactly right to me.

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

Right, but still unconvinced eqscl is the way to represent identity.

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

Correct, and it requires a schema in FOL, right?

> 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",

Both instances of the more general identity schema:

forall x,y (x=y -> (A -> A[x/y])),

where A[x/y] is the result of replacing all free occurrences of x with 
y (y assumed to be free for x in A).  I'm not quite sure what you mean 
by the above being "susbtitution" axioms for Pred; they are just 
instances of axioms for identity.

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

Since I'm not clear about what a substitution axiom is, I'm not sure 
how to evaluate this.

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

I have to admit that I am pretty set in my ways, and that makes it 
difficult for me sometimes to see things that others, with different 
perspectives, find obvious.  Perhaps that is why I do not find what you 
are saying obvious or intuitive, Tanel.

-chris