Introduction

In MATHS equality has properties that are different to those made by logicians like Whitehead and Russell(1920s) or Kleene 1967. The logician's equality is a given property of given objects which is true when and only when the objects are identical. In MATHS identity is used in a meta-linguistic way. Equality is more useful and looser relationship between expressions.

In logics where expressions can be evaluated to expressions are equal when they have the same value. One can also argue that the natural values in a logic with equality are essentially the sets of equivalent elements under equality.

In MATHS, as in an algebra, we get different types by assuming different forms of equality. Items are equal, not when they are identical but when we wish to confuse them! We are permitted to create new types of object by ignoring differences. For example the strings "1+2" and "2+1" are different but 1+2 and 2+1 are expressions of an numeric type and so will be assumed equal.

When an axiom of the form

1. for all x,y: T, if W(x,y) then x=y

   is added to the other axioms and variables that define a type, a new type is generated. The new type is called a quotient type and can be thought of as being a collection of sets of elements of the original type. The elements in the new set are treated as single objects however.

   Example

   ---

   An example of this is the construction of the rational numbers by
   1. Pairs::=$ following.
      Net
      1. numerator::Integer,
      2. denominator::Natural.

      
      (End of Net)
      
      
   2. Rational_Numbers::=Pairs / cross_ratio. [ logic_41_HomogenRelations#Equivalence Relations ]
   3. cross_ratio::=rel[x,y:Pairs](numerator(x)*denominator(y)=numerator(y)*denominator(x)).

      In MATHS we can write

   4. RATIONAL::=
      Net{

      1. Rational::=Pairs.
      2. For all x,y:Pairs, if (numerator(x)*denominator(y)=numerator(y)*denominator(x)) then x=y.
      3. ...

      
      }=::RATIONAL.
   5. Rational::= $ RATIONAL

   ---

   For each type of object a rule needs to be given specifying when two objects are to be assumed equal. In many ways the conditions under which two expressions are considered to be equal define the mathematical properties of a type. In may ways algebra is the study of the effect of various equalities - commutativity, associativity, cancellation and so on. In practice there are three distinct ways an equality is asserted: (1) By a simple definition of a new term,(2) As an axiom making certain simple expressions equal, and (3) By a recursive definition. Take these in turn:

   ---

   [1] A simple definition of a new term:

   	t ::= e

   or

   	t::T=e

   where e does not contain t and t is free prior to the definition.

   These definitions declare the term t and also add the axiom

   	t=e.

   Such a definition does not change the logic of the type very much because such terms can always be removed from any expression by substituting their expression. This does not constrain the type: if there were objects of the type without the definition then there will be similar objects existing afterward. These are essentially notational conveniences.

   Compare with [Jackson95c] where terms are attached to real world designations. The syntax of a definition is used in MATHS also to designate a term:

    	t::T=`string in some other language`.

   is semantically equivalent to

    	t::T.

   This is therefore a declaration of a new term and can not constrain the type.

   [2] An axiom making certain simple expressions equal:

    	For all .....  , e1=e2.

   The result is a different type of object called a quotient type because the the original objects are now divided up into class of equivalent objects that are treated as equal. [ logic_41_HomogenRelations#Equivalence Relations ]

   [3] By a recursive definition:

    		t ::= e

   or

    	t::T=e

   where e does contain t, or t has been used in an earlier definition. These add a new axiom:

    	t=e,

   These may or may not invalidate the type. It is wise to demonstrate that there is a set of objects that satisfy the axioms when there is a recursive definition in the axiom system.

   ---

   Mathematically such formulas look very like equations: Such equations can often be solved.

   ---

   1. For example:
   2. x = 2*x

      This equality is satisfied by exactly one value of x, x=0. So sometimes an axiom like this leads to defining a term.

      However consider this equation:

   3. x = x^2+2*x

      This is satisfied by x=0 or x=-2, for example. This shows that a recursive definition may not define a unique value. We have an under-defined term.

      Considering:

   4. x = 2^x

      we are forced to realize that there is no value of x that satisfies some definitions. Here x is over-defined.

   ---

   Equality has attracted the attention of both computer scientists and software engineers. Here are some notes:

   Substituting one expression for an equal one is the heart of Gries approach to logic and programming[Gries 91, Gries & Schnieder 93). From this rules of symmetry, transitivity, ... can be deduced [Kalish & Montague 64].

   Substitution of equals does not always work inside character strings and quotations. It can also fail in statements involving beliefs, desires, and knowledge. The MATHS assumption (as in Cyc [Lenat et al 90]) is that such statements can be handled by placing the beliefs, knowledge, etc in a string. Just because two expressions have the same informal description we can not conclude that they are equal.

   Parnas has pointed out that when expressions in an equality contain partial functions then it is simplest to assume that the equality is false whenever either or both expressions are undefined[Parnas 93].

   Syntax

   For any two expressions x and y of the same type x=y and x<>y are predicates. Thus x=y and x<>y have type @ if and only if x and y have the same type.
2. For T:Type, x,y:T, (x=y) ::@=x and y are defined and are identical.
3. For T:Type, x,y:T, (x!=y) ::@= not(x=y).
4. For T:Type, x,y:T, (x<>y) ::@= (x!=y).

   The "!=" notation comes from the C family of languages and has infected just about evry programmer by now. The abbreviation representing inequality (<>), comes from BASIC and Pascal, but this should be shown (if possible) as the conventional mathematical symbol when a document is typeset or displayed.

   Equality and inequality are both serial operators so expressions of form x = y = z, w = x = y = z, and so on are valid when x, y, and z are expressions of the same type.

   Semantics of equality

5. For x,y:T, (x=y) ::= y can be substituted for x in all logical contexts.

   The exceptional non-logical contexts are: character strings, quotations, and statements involving beliefs, desires, and knowledge. These will not in general keep the same value when equals replace equals.

   Note that if x or y are expressions with free variables then one needs to be careful to not substitute one for the other in a context where the free variables are bound. The bound variables need to be changed to other variables. Similarly, if x is a variable then only free occurrences of it can be replaced in an expression by y.

   Equality is used via Euclid's Axiom - Equals can be substituted for equals:
   

6. |- (euclid1): For expressions x and y of type T, x=y iff for all e(x):expression_containing_x, e(x) = e(y)

   and
   

7. |- (euclid2): For expressions x and y of type T, x=y iff for all W(x):predicate_containing_x, W(x) iff W(y).

   Liebnitz's Axiom is similar: Two expressions are equal if and only if they remain equal when any and/all values of variables they are equal:
   

8. |- (liebnitz): For variables x with type T1 and e1(x), e2(x):expression_containing_x of type T2, e1(x)=e2(x) iff for all x:T ( e1(x)=e2(x) ).

   So x+1 = 1+x in any traditional numeric type because 0+1=1=1+0, 1+1=1+1, 2+1=1+2, 3+1=1+3, ....

   Similarly for predicates, two predicates are equal exactly when they have the same truth value when the same values are substituted for the same variables in each predicate. The iff is the same as = between predicates.

   Uniqueness and Definite Descriptions

   Expressing Uniqueness

   Use the quantifier one: (uniqueness): (for one x:X(W(x))) ::= for some x:X( W(x) and for all y:X(if W(y) then x=y)).

   Definite descriptions and articles

   If we know that there is only one object satisfying a property, then we can define the object that satisfies that property. We borrow the definite article or the from English:

    	the (object:Type || Property).

   Alternate syntax

   A more writable alternative is:

    		the(object:Type . Property).

   The standard binding form is:

    		the[object:Type] (Property).

   which suggests using the with a subscript when type set.

   Note. Later we can also define,

   1. the [ x:T1, y:T2, ...] (W(x, y,...) = the [v:T1><T2><T3...] (W(v.1st, v.2nd,...)) and
   2. for all S:Sets, the S = the [x:S](true).

   3. For N:structure, S:@$ N, P:proposition(variables(N)), the N(P)::=the unique $(N) in S and satisfying P.

      Syntax of definite descriptions

      The above is a definite description:
   4. definite_description::= "the" variable ":" type "(" predicate ")" | "the" "(" variable ":" type "||" proposition")" | "the" "[" loose_bindings"]" "(" predicate")" | "the" set_expression | "the" structure "(" proposition")".

      Rules for definite descriptions

      
      
   5. |- (the1): if for one x:X (W(x)) then the(x:X||W(x)) exists and is in X
      
   6. |- (the2): if for one x:X (W(x)) then the(x:X||W(x) ) in X and W( the(x:X||W(x) )).

      If-then-else

      
      

   7. (above)|- (ite1): For all p:@, x:T, y:T, one z:T, (if p then z=x else z=y).
   8. For p:@, x:T, y:T, if(p,x,y)::= the(z:T||if p then z=x else z=y).
      
   9. (above)|- (ite2): For p:@, x:T, y:T, if p then if(p,x,y)= x.
      
   10. (above)|- (ite3): For p:@, x:T, y:T, if p then if(p,x,y)= y.

       Undefined Definite Descriptions

       Occasionally we need the idea of `the x satisfying P, iff its unique, else some other value`
   11. For W:@^T, a:T, the(z:T||W(z)||a)=if(for one (z:T||W(z)),the(z:T||W(z)),a).

       Kalish and Montague go further and effectively introduce the idea that all non-unique description defines the same value the(x:X || false). This is reminiscent of the null pointer in many languages and the Smalltalk Class of Undefined Object. This lets them derive three useful inference rules:

   12. You can change all occurrence of a bound variable to a different (unused) one.
   13. If two predicates are equivalent then one can be substituted for the other.
   14. If two expressions are equal then one can be substituted for the other.

       However MATHS takes these inferences for granted. Now we can show that, if no object of the relevant set(X say) fits the definition then, the description formula is equal to the(x:X || x<>x):
       

   15. |-if for no x:X(W(x)) then the(x:X|| W(x) ) = the(x:X || false).
       Let
       
       
       1. |- (1): for no x:X(W(x)),
          
       2. (1)|- (2): for all x:X(not W(x)),
          
       3. (2)|- (3): for all x (W(x) iff false),
          
       4. (subs iff):|-(4) the(x:X|| W(x) ) = the(x:X || x<>x).
       
       (Close Let )
       However if two or more objects can fit a property W then it is not obvious that the(x:X||W(x))=the(x:X||W(x)).

       Indeed Dana Scott's Domains are sets of objects which are more or less defined and contain both an undefined object (⊥) and the overdefined object(→p) - one that can not exist because its specification is contradictory [ACM87]. So we do not assume this as an axiom but name the proposition encoding the inference as "Improper descriptions".

   16. Improper_descriptions::@. Improper_descriptions iff if for no x:X, some y:X (W(x) iff x=y ) then the(x:X|| W(x) ) = the(x:X || false).

       Top and Bottom

       Taking this a step further, we can associate with each type a domain - this has, in addition to the usual values, two extra ones - the undefined value(bottom) and the over-defined value(top) with the following properties
   17. DOMAIN::=following,
       Net
       1. ⊥::T.
       2. →p::T.
       3. For all W:predicate, if for 0 x(W(x)) then the(x:X||W(x))=→p.
       4. For all W:predicate, if for 1 x(W(x)) then W(the(x:X||W(x)).
       5. For all W:predicate, if for 1 x(W(x)) then for all y(if W(y) then y=the(x:X||W(x)).
       6. For all W:predicate, if for (2..) x(W(x)) then the(x:X||W(x))=⊥.

       
       (End of Net)
       
       

   . . . . . . . . . ( end of section Uniqueness and Definite Descriptions) <<Contents | End>>

   Cans of Worms

   Adding definite descriptions into a logic opens a can of worms. We have the problem of handling expressions that have no valid value or no defined value. For example: mathematicians regularly solve equations under the assumption that a solution exists. But the value they find is only a solution if there is a solution - see section 7 below. Kalish and Montague assume that if there is no unique x that satisfies W(x) then
9. the(x:T||W(x)) = the(x:T|| x<>x). Parnas argues out that this is not just a theoretical problem but one that arises in software specifications:
10. For all Real x, sqrt(abs(x))=if(x>=0, sqrt(x), sqrt(-x)),

    but y'=sqrt(x) or y'=sqrt(-x) in normal logic is undefined because one part is undefined.

    This question has also been debated on Usenet: comp.specification.z

    Mathematicians assumed that there was an "imaginary" sqrt(-1) and developed complex numbers. LISP, Algol 60, C, Smalltalk, etc all delay the evaluation of all the arguments in condition expressions until after the condition is evaluated. Dijkstra introduces a special operator cand that is the logical equivalent of Ada's short circuited "and then" or UNIX's "&&".

    Parnas notes that in software engineering it is simpler to assume that certain primitive predicates (like equality) are false when their parts are undefined[Parnas93]. In MATHS the predicate e1=e2 is assumed false if either e1 or e2 are undefined. This is quite different to Kalish and Montague's assumption, but is, apparently consistent[Parnas 93]. We can say that '=' is Parnasian predicate. It follows that e1<>e2 must be true if either e1 or e2 are undefined. We might call this an anti-Parnasian predicate.
    Net

    Parnas gives the general rules but does not specify what the primitive predicates would be in practice. So if "=" and "<>" are taken as primitive then both are true if they applied to an undefined term. Thus we could no longer assume that for all terms x and y:
    1. x=y iff not(x<>y).

       Parnas does not discuss the question of whether a recursive definition of a predicate creates a primitive or non-primitive predicate. This may be because recursion opens the question of predicates being undefined -- something that Parnas is trying to avoid.

    
    (End of Net)
    
    

    Adding '=' to a logic opens another can of theoretical worms if we then ask which universes of discourse fit the logic - the different semantic models of the logic. The work on Universal Algebra and Category Theory shows that there are several ways to define these models[Wechler 92, Cramer et al 94]. In the strictest of these (initial semantics) all the models are similar except for relabeling the objects systematically - here two objects in the universe are taken to be equal if and only if they can be proved equal in the logic. The loosest form - final or terminal semantics - two objects can be the same(confused) unless they can be proved different. In practice these distinctions don't seem to be particularly important.

. . . . . . . . . ( end of section Equality, Uniqueness, etc) <<Contents | End>>

Numerical quantifiers