Theory of proveit.logic.equality¶
This theory deals with equals, not equals, and various forms of substitution. The basic idea is that all well-defined expressions evaluate to mathemetical objects and any two mathematical objects are either exactly equal to each other or not. Expressions are said to be equal when they evaluate to the same mathematical object. Any expression is equal to itself even if it is ill-defined. It is, however, not general possible to prove equality relations involving an ill-defined expression; there is generally no way to know whether or not an ill-defined expression is ill-defined (versus requiring an axiom that has not yet been invoked).
Equality is transitive (if $x=y$ and $y=z$ then $x=z$) and symmetric (if $x=y$ then $y=x$), as inherent properties of sameness. Furthermore, substitution is fundamental to the concept of equality. If two expressions are equal, then one may be substituted for the other in any theory without changing the meaning of the original expression.
