[SCL] Horrock formulas: simple solution candidates

[Tanel Tammet]

Hi,

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

This can be easily proved (unless I am horribly
mistaken) by transforming the derivations of
a contradiction from F to the similar derivations
in enc(F), and vice versa (in the latter case
assuming the condition from the lemma).

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"

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,
  only one needed:
  forall x,y. (x=y => (P(x) <=> Q(x))).

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


Obviously, in the latter we have variables occurring
as a first argument of Pred, hence violating the
condition in the lemma.

Now we have two simple options to amend the situation:

Option A: axiomatise "=" before the encoding to App/Pred,
and THEN encode to App/Pred:

   We would get the following set (***) of axioms for "=":

   - equivalence axioms:

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

   - substitution axioms (only one):

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

   Observe that these axioms DO NOT violate the condition of
   not having variables as a first argument of Pred, hence
   everything will be fine with the Horrock formulas.

Option B: drop some of the substitution axioms from
the set (**) created by axiomatising "=" AFTER encoding to
App/Pred:

  In the axiomatisation (**) above we would drop
  the first substitution axiom.

  The limited axiomatisation we get still violates the
  condition of not having a variable in the first argument
  of App/Pred, but I am positive that we can prove that
  the addition of the limited set of equality substitution
  axioms to the enc(F) in the lemma above still preservers
  the property
  satisfiable(F) <=> satisfiable(enc(F)).


To summarise: we could use the App/Pred encoding of traditional
FOL and still avoid the problems from Horrock
formulas. We have at least two options for doing this
(A and B above). Both lead to having two different equality
predicates: one being a (limited) equality used in traditional
FOL, one being the full, typeless equality.


Observe that in SCL where one can explicitly write formulas
like
(forall x,y. x(y))
it is always possible for users to introduce the axioms like
the problematic substitution axiom in (**),
hence creating Horrock-kind of formulas themselves.

However, doing this requires adding
non-traditional axioms (variable occurring at the place of
a predicate) to a "traditional FOL" formula, like this:

(forall x. P(x) & -Q(x)) & (forall x,y. E(x,y)) &
(forall x,y,z. (E(x,y) => (x(z) <=> y(z)))).

Such a combination could be IMHO rightly be expected to be
non-satisfiable even if the traditional FOL part
is satisfiable: predicate "E" above is very clearly
NOT axiomatised in traditional FOL.

Hence, we could probably avoid the problems stemming from
the Horrock formulas even without using typed quantifiers
or type predicates: IMHO it would suffice to have two different
equality predicates, one a "traditional FOL" equality, one a
"free" equality.
Personally, I'd prefer option (A) as simpler and clearer.

I do not know if this whole approach would be any
better or any worse than others, and certainly it
is not a really new idea.

The goal of this letter was to remind that (unless I
have missed something really crucial) there seem to
be simple equality-based options for tackling
the Horrock problem.


Regards,
          Tanel Tammet