.Open Equality, Uniqueness, etc . 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 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 .Box An example of this is the construction of the rational numbers by Pairs::=$ following. .Net numerator::Integer, denominator::Natural. .Close.Net Rational_Numbers::=Pairs / cross_ratio. .See http://www/dick/maths/logic_41_HomogenRelations#Equivalence Relations cross_ratio::=rel[x,y:Pairs](numerator(x)*denominator(y)=numerator(y)*denominator(x)). In MATHS we can write RATIONAL::=Net{ Rational::=Pairs. For all x,y:Pairs, if (numerator(x)*denominator(y)=numerator(y)*denominator(x)) then x=y. ... }=::RATIONAL. Rational::= $ RATIONAL .Close.Box 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: .Box [1] A simple definition of a new term: .As_is t ::= e or .As_is 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 .As_is 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 .See [Jackson95c] where terms are attached to real world `designations`. The syntax of a definition is used in MATHS also to designate a term: .As_is t::T=`string in some other language`. is semantically equivalent to .As_is 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: .As_is 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. .See http://www/dick/maths/logic_41_HomogenRelations#Equivalence Relations [3] By a recursive definition: .As_is t ::= e or .As_is t::T=e where `e` does contain `t`, or `t` has been used in an earlier definition. These add a new axiom: .As_is 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. .Close.Box Mathematically such formulas look very like equations: Such equations can often be `solved`. .Box For example: 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: 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: x = 2^x we are forced to realize that there is no value of x that satisfies some definitions. Here x is over-defined. .Close.Box Equality has attracted the attention of both computer scientists and software engineers. Here are some notes: .Set 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]. .Close.Set . 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. For T:Type, x,y:T, (x=y) ::@=`x and y are defined and are identical`. For T:Type, x,y:T, (x!=y) ::@= not(x=y). 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 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: |- (euclid1): For expressions x and y of type T, x=y iff for all e(x):`expression_containing_x`, e(x) = e(y) and |- (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: |- (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. .Open 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: .As_is the (object:Type || Property). . Alternate syntax A more writable alternative is: .As_is the(object:Type . Property). The standard binding form is: .As_is the[object:Type] (Property). which suggests using `the` with a subscript when type set. Note. Later we can also define, the [ x:T1, y:T2, ...] (W(x, y,...) = the [v:T1>x)`: |- if for no x:X(W(x)) then the(x:X|| W(x) ) = the(x:X || false). .Let |-(1): for no x:X(W(x)), (1)|-(2): for all x:X(not W(x)), (2)|-(3): for all x (W(x) iff false), (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 (\bot) and the overdefined object(\top) - 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". 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 DOMAIN::=following, .Net \bot::T. \top::T. For all W:predicate, if for 0 x(W(x)) then the(x:X||W(x))=\top. For all W:predicate, if for 1 x(W(x)) then W(the(x:X||W(x)). For all W:predicate, if for 1 x(W(x)) then for all y(if W(y) then y=the(x:X||W(x)). For all W:predicate, if for (2..) x(W(x)) then the(x:X||W(x))=\bot. .Close.Net .Close Uniqueness and Definite Descriptions . 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 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: 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: .See news: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: 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. .Close.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. .Close Equality, Uniqueness, etc . Numerical quantifiers An example is `for all x, 2 y(y^2=x)`. To define these completely we have to use both set and number theory - which comes later - Maths.Numbers. For n:Nat0, for n x:X(W(x)) ::= if n=0 then for no x:X(W(x)) else if n=1 then for one x:X(W(x)) else for some x:X( W(x) and for (n-1) y:T( W(y) and not x=y) ). |- for 1 x:X(W(x)) iff for some x:X(W(x)) and for 0..1 x:X(W(x)). For N:@Nat0,x,X,W, (for N x:X(W)) ::= (|{x:X||W}| in N). For n:Nat0, (..n) ::= { i:Nat0 || i<=n}, For n:Nat0, n..::= { i || i >=n} For n,m:Nat0, n..m::= n.. & ..m. any::quantifiers= Nat0. This is used mainly in quantifying relationships - for example X(any)-(1)Y says that for each X there is one Y but there can be any number of X's (including none) for a given y. |- for 0..1 x:X(W(x)) iff for all x,y(if W(x) and W(y) then x=y). |- not for 0..1 x:X(W(x)) iff for all x,y (W(x) and W(y) not x=y). |- for ..n-1 x:X(W) = not for n.. x:X(W). |- for n+1.. x:X(W) = not for ..n x:X(W). For A: Finite(T),..., (for most a:A(W(a)) ) ::= |{ a:A||W(a)}| > 0.5 * |A|, For A, (for (p%) a:A(W(a)) ) ::= |{ a:A||W(a)}|*100=|A|*p. . Advanced Quantifiers abf::= `all but a finite number of`. finite::=`only a finite number of`, well defined on natural numbers. infinite::=`infinite number of`, well defined on netural numbers. For a:variables, W:integer_proposition, for abf a(W(a))=for some n:Nat0, all m:Nat0( if m>n then W(m)). For a:variables, W:integer_proposition, for finite a(W(a))=for some n:Nat0, all m:Nat0( if m>n then not W(m)). For a:variables, W:integer_proposition, for infinite a(W(a))=for all n:Nat0, ssome m:Nat0( m>n and W(m)). In general, For T:Types,... (for abf x:T(W(x)) ) ::= {x:T||not W(x)} in finite(T). generic::=`in the general case excluding a highly unlikely class of special cases`. This is rather an advanced idea and only has meaning when the type of the variable is some kind of continuum or space, and the excluded cases form a continuum or space of lower dimension or of measure zero. Do not confuse this the idea of generic properties that apply to any type of objects. For T:Type, m:measure(T), W:predicate(T), (for generic x:T(W(x)) ) ::= m({x:T||not W(x)} = 0. For T:Type, dim:@T->Nat0, if `T in space(dim=>dim(T))` then W:predicate(T), (for generic x:T(W(x)) ) ::= dim{x:T|| not W(x)} < dim(T). For example, in normal 3D space, two 2D objects generically intersect in a 1D object. The chances of the just touching is mathematically 0. Or, generically two lines are never parallel, ... . Either_or The following are useful abbreviations for documenting systems that have internal classifications: PET1::=Net{ ... Either cat, dog, gopher, or peculiar. ... }. For A,B:identifier, Either A or B::=Net{ A,B:@. one(A,B). }, For A,B,C:identifier, Either A, B, or C::=Net{ A,B,C:@. one(A, B, C). }, For A:L(identifier), B:identifier, Either A, or B::=Net{ A,B:@. one(A,B). }. For P, Q:@, one(P,Q) ::@=P iff not Q, For P, Q, R:@, one(P,Q,R) ::@=if not P then one(Q,R) else not P and not Q, For P:#@, one(P) ::=if not 1st(P) then one(rest(P)) else no(rest(P)), For P:#@, no(P) ::=not 1st(P) and no(rest(P)), no() ::=true, For p:#@, two(p) ::=if 1st(p) then one(rest(p) else two(rest(p)). For p:#@, n:Nat0, (n)(p) ::= if 1st(p) then (n-1)(rest(p)) else (n)(rest(p)). . Existence Dependency Partly Baked Idea! Here is an abbreviation that may be useful for discovering databases and class hierarchies and ontologies. Suppose that we have a predicate F on type X and predicate G on objects of type Y then define: F >-> G ::@=for all x:X(if F(x) then for 1 y:Y( G(y))). The idea is that a good data base design can be based on the predicates describing the situation/state of the world and connected by the existence dependencies. These lead to the functional dependencies used in data base normalization etc.