[SCL] Identity and Horrocks sentences

Sat May 31 02:46:38 CDT 2003

Hi,

Christopher Menzel wrote:

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

Ha, we have different views on honesty :-)

I have understood that your default reasoning mode is model theory,
whereas my default reasoning mode is proof theory. Fortunately,
since proof theory reflects model theory, there are no
important differences in the end results of these two modes.

Now, the formula (* honest) above is the correct TFOL
representation of a "shorthand":

(*) (x)(Px <-> ~Qx) & (x,y)x=y.

Just look in any good handbook (just kidding, of course
you do know it is correct).

It is a well-known fact for ages that in plain TFOL
without equality one can axiomatise equality for each
concrete TFOL sentence. That is exactly what we do here,
exactly in the way it is traditionally done.

The axiomatisation, when added to a formula F in TFOL
(our example: *) gives a new formula, in our case
(* honest).

Then, "in TFOL with built-in equality F is satisfiable" iff
"(F + equality-axioms) is satisfiable in TFOL without equality".

Of course, almost all the other important properties are preserved
as well (for example, the question "what is the size of a minimal
domain on which F (resp (F + equality-axioms)) has a model" gives
the same number).

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

It is the way, at least according to the decades-old agreement of
people working with TFOL.

IF you want your identity to be something non-traditional, then of
course you may claim what you did. But then we start slowly moving
away from classical logic. I could take the next step, say, an
intuitionistic view and claim that all your classical model theory is
plain wrong. Since I worked at Chalmers, I do personally know
serious people who believe that the classical model will lead
to contradictions in fancy situations (ie parts of classical
mathematics are contradictory).

Now, I have understood that we do NOT take a non-traditional
view in SCL and will NOT start to discuss whether we should perhaps
base it on intuitionistic logic (or better still, linear logic :-).
Hence I'd like to also keep the traditional equality predicate.

More seriously: moving away from the traditional equality would
probably mean that the TFOL provers with all the fancy apparatus
for efficient equality handling will not be capable of
handling SCL formulas correctly - at least without major
reimplementation efforts. This would be real bad.

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

A schema, yes, which cannot be be axiomatised in TFOL itself.
Equality, as we know, cannot be finitely axiomatised in TFOL. It
can be finitely axiomatised (easily) for any particular TFOL
sentence.

>> 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 would not use this schema. It may lead to too many axioms
if applied non-intelligently. Take A(f(x,g(y,x))).
A large number of instances will be created.

Rather, I use a different schema which axiomatises that
for any i-arguments of any function/predicate symbol in
the signature of your formula the replacement of A for B
gives an equal term (equivalent atom).

In order words, the "standard" schema I am using works
on the signature of a particula formula. The other details
of a formula are not relevant: only the signature is.

 > I'm not quite sure what you mean by
> the above being "susbtitution" axioms for Pred; they are just instances 
> of axioms for identity.

Right. I used the phrase "substitution axioms" for these equality axioms
which are NOT in the set of three standard equivalence axioms.
I agree that the "substitution axioms" might be a not too successful
name for these - but it is an often-used terminology.

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

Said above.

Just to "prove" that what I wrote is a standard way to understand
equality, used by other people, I will cite  a part of Geoff's
course on automated theorem proving. See
http://www.cs.miami.edu/~geoff/Courses/CSC648-F02/Content/1stOrder.shtml
------------------------------------------------------
....
Although the conjecture may seem like a logical consequence to humans, 
that's because humans "know" what equal means (even without knowing what 
the "maths" means). However, there are many models of the axioms that 
are not a models of the conjecture, e.g., simply by making 
even(sum(four,b)) be FALSE. Such models are possible because the axioms 
are missing definitions for equal/2. These definitions are the axioms of 
equality, and must be included to force equal/2 is to have its usual 
meaning. They are:

     * Reflexivity - everything equals itself
     * Symmetry - If X equals Y then Y equals X
     * Transitivity - If X equals Y and Y equals Z, then X equals Z

"X equal(X,X)
"X "Y (equal(X,Y) => equal(Y,X))
"X "Y "Z ((equal(X,Y) /\ equal(Y,Z)) => equal(X,Z))

     * Function substitution - If X equals Y then f(X) equals f(Y). For 
every argument position of every functor.
     * Predicate substitution - If X equals Y and p(X) is TRUE, then 
p(Y) is TRUE For every argument position of every predicate.

"X "Y "Z (equal(X,Y) => equal(sum(X,Z),sum(Y,Z)))
"X "Y "Z (equal(X,Y) => equal(sum(Z,X),sum(Z,Y)))
"X "Y "Z (equal(X,Y) => equal(difference(X,Z),difference(Y,Z)))
"X "Y "Z (equal(X,Y) => equal(difference(Z,X),difference(Z,Y)))
"X "Y ((equal(X,Y) /\ even(X)) => even(Y))
"X "Y ((equal(X,Y) /\ zero(X)) => zero(Y))
------------------------

Regards,
         Tanel Tammet