Draft of explicit axiomatization of equality for RuleML / DAML Rules 

by Benjamin Grosof

version V1 of 7/1/03

% (file housekeeping memo to Benjamin:  this file is axiomatization-1.txt, 
%  excerpted from file equality/thoughts-1.txt)

Background:  see Joint Committee telecon discussion of 7/1/03, including 
- Mike Dean's test cases
- Benj's notes from the telecon

Here's a pass at defining an axiomatization, within a declarative 
(definite Horn) LP language itself, 
of explicit equality.  Here, equality is 
treated as essentially an ordinary predicate (rather than specially
within the model theory).  
Let ee stand for the explicit equality predicate.   

1. symmetry:  

  ee(?y,?x) <- ee(?x,?y);

2. transitivity:

  ee(?x,?z) <- ee(?x,?y) and ee(?y,?z);

3. substitutivity for predicates:

Let P1,...,Pm be the predicates of the LP language.
Let the arity of Pi be ni, where ni >= 0.

For each Pi, i=1,...,m, and for each j=1,...,ni:    

  Pi(?X1,...,?W,...,?Xni) <- ee(?Xj,?W) and Pi(?X1,...,?Xj,...,?Xni);

Actually, one can equivalently omit this if ni=0.  

4. substitutivity for logical functions, i.e., constructors:

Let F1,...,Fk be the logical functions of the LP language.
Let the arity of Fi be ni, where ni >= 0.

For each Fi, i=1,...,k, and for each j=1,...,ni:    

  ee(?Y,Fi(?X1,...,?W,...,?Xni)) 
         <- ee(?Xj,?W) and ee(?Y,Fi(?X1,...,?Xj,...,?Xni));

Actually, one can equivalently omit this if ni=0.  


Issue/Q todo:  do we need to say anything else about equality other
than the above (1.)-(4.)?  
- E.g., is there anything different about skolem functions?  
- E.g., is there something that needs to be said about how unification
treats equality in corresponding proof theory (since the usual
definition of unification ignores equality other than syntactic
identicality)?

todo: Look at how FOL with equality has been formalized, including
unification in it.