Equality
Two mathematical objects are equal if and only if they are precisely the same in every way. This defines a binary relation, equality, denoted by the sign of equality = in such a way that the statement "x = y" means that x and y are equal.
Some properties:
"all a,b . a = b -> b = a"""all a,b . a = b -> b = a"" cannot be used as a page name in this wiki. "symmetry"
"all a,b,c . a = b /\ b = c -> a = c""transitivity"
Where "/\" is logical (ML -style ) "and", "->" is implication
and "all" is the Universal Quantifier
S-expressions for <ask>Equality*</ask> for example is "(all (a) (= a a))"; for <ask>Equality*</ask> "(all (a b) (-> (= a b)(= b a)))"""(all (a b) (-> (= a b)(= b a)))"" cannot be used as a page name in this wiki.; etc
The substitution property states:
For any quantities a and b and any expression F(x), if a = b, then F(a) = F(b)
Some specific examples of this are:
"all a,b,c . a = b -> a / c = b / c)" (here F(x) is x / c); "substitution /"
"all a,b,c . a = b -> a * c = b * c)" "all a,b,c . a = b -> a + c = b + c)" "all a,b,c . a = b -> a - c = b - c)"
