[SCL] CORRECTION to the previous Horrock and equality message

[Chris Menzel]

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.

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

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.)  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.  But, of course, on the web, where
formulas don't wear their concomitant semantic rules on their sleeve,
this represents a genuine problem.  Do we scrap SCL syntax and just
start writing App/Pred sentences?  Do we tell everyone to rewrite their
automated reasoners?  Do we call for a revolution in logic?   It seems
to me that a little required header information at the top of any logic
file -- something analagous to an HTML <!DOCTYPE> tag -- could go a long
way here, but what do I know.

BTW, Pat and I discussed the App/Pred encoding in a sketchy paper on an
early KIF'ish version of SCL that we presented at IJCAI 2001:

http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI01.pdf

I think I'm not clear on exactly what you think the problem is to
which your proposal is a solution, Tanel.  (This is quite possibly my
fault.)  But let me just ask a couple of questions about a few things in
your msg.

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

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

That's what we get on the App/Pred translation scheme I'm suggesting.

-chris