Draft:Substitution (mathematics)

History

Possible? Early mathematics

Babylonian and Egyptian mathematics solving quadratic equations

Greek geomety

Euclid

Indian mathematics

Aryabhata

Brahmagupta

Early algebra

Al-Kitab al-Mukhtasar fi Hisab al-Jabr wal-Muqabala

François Viète

Explicit

La Géométrie - change coordinate systems or simplify equations in Analytic geometry

Leibniz and Newton, in calculus, and especially Integration by substitution

Substitution property of equality

In mathematics, there are two common uses of substitution: substitution of variables for constants (also called assignment for that variable), and the substitution property of equality, also called Leibniz's Law.

Considering mathematics as a formal language, a variable is a symbol from an alphabet, usually a letter like Template:Mvar, Template:Mvar, and Template:Mvar, which denotes a range of possible values. If a variable is free in a given expression or formula, then it can be replaced with any of the values in its range. Certain kinds of bound variables can be substituted too. For instance, parameters of an expression (like the coefficients of a polynomial), or the argument of a function. Moreover, variables being univerally quantified can be replaced with any of the values in its range, and the result will a true statement. (This is called Universal instantiation)

For a non-formalized language, that is, in most mathematical texts outside of mathematical logic, for an individual expression it is not always possible to identify which variables are free and bound. For example, in $\sum _{i<k}{a}_{ik}$, depending on the context, the variable $i$ can be free and $k$ bound, or vice-versa, but they cannot both be free. Determining which value is assumed to be free depends on context and semantics.

The substitution property of equality, or Leibniz's Law (though the latter term is usually reserved for philosophical contexts), generally states that, if two things are equal, then any property of one, must be a property of the other. It can be formally stated in logical notation as:$$(a=b)⟹[\varphi (a)\Rightarrow \varphi (b)]$$For every $a$ and $b$, and any well-formed formula $\varphi (x)$ (with a free variable x). For example: For all real numbers Template:Math and Template:Math, if Template:Math, then Template:Math implies Template:Math (here, $\varphi (x)$ is Template:Math). This is a property which is most often used in algebra, especially in solving systems of equations, but is apllied in nearly every area of math that uses equality. This, taken together with the reflexive property of equality, forms the axioms of equality in first-order logic.

In mathematical logic and mathematical philosophy, equality is often described through the following properties:

$\mathrm{\forall }a(a=a)$

• Law of identity: Stating that each thing is identical with itself, without restriction. That is, for every $a$, $a=a$. It is the first of the historical three laws of thought.

$(a=b)⟹[\varphi (a)\Rightarrow \varphi (b)]$Template:Efn

• Substitution property: Sometimes referred to as Leibniz's law, generally states that if two things are equal, then any property of one must be a property of the other. It can be stated formally as: for every Template:Mvar and Template:Mvar, and any formula $\varphi (x),$ (with a free variable Template:Mvar), if $a=b$, then $\varphi (a)$ implies $\varphi (b)$.

For example: For all real numbers Template:Math and Template:Math, if Template:Math, then Template:Math implies Template:Math (here, $\varphi (x)$ is Template:Math)

These properties offer a formal reinterpretation of equality from how it is defined in standard Zermelo–Fraenkel set theory (ZFC) or other formal foundations. In ZFC, equality only means that two sets have the same elements. However, outside of set theory, mathematicians don't tend to view their objects of interest as sets. For instance, many mathematicians would say that the expression "$1\cup 2$" (see union) is an abuse of notation or meaningless. This is a more abstracted framework which can be grounded in ZFC (that is, both axioms can be proved within ZFC as well as most other formal foundations), but is closer to how most mathematicians use equality.

Note that this says "Equality implies these two properties" not that "These properties define equality"; this is intentional. This makes it an incomplete axiomatization of equality. That is, it does not say what equality is, only what "equality" must satify. However, the two axioms as stated are still generally useful, even as an incomplete axiomatization of equality, as they are usually sufficient for deducing most properties of equality that mathematicians care about. (See Template:Section link)

If these properties were to define a complete axiomatization of equality, meaning, if they were to define equality, then the converse of the second statement must be true. The converse of the Substitution property is the identity of indiscernibles, which states that two distinct things cannot have all their properties in common. In mathematics, the identity of indiscernibles is usually rejected since indiscernibles in mathematical logic are not necessarily forbidden. Set equality in ZFC is capable of declairing these indiscernibles as not equal, but an equality solely defined by these properties is not. Thus these properties form a strictly weaker notion of equality than set equality in ZFC. Outside of pure math, the identity of indiscernibles has attracted much controversy and criticism, especially from corpuscular philosophy and quantum mechanics. This is why the properties are said to not form a complete axiomatization.

However, apart from cases dealing with indiscernibles, these properties taken as axioms of equality are equivalent to equality as defined in ZFC.

These are sometimes taken as the definition of equality, such as in some areas of first-order logic.

Proof of property in ZFC

See Template:Section link for the definition of formulas in ZFC. The definition is recursive, so a proof by induction will be used. For simplicity, this proof simplifies the recursive definition to only have three possible recursive steps: $\mathrm{\exists }x(\psi ),\mathrm{\neg }(\psi ),\text{and}\psi \wedge \varphi$, which can be shown to be equivalent.

In ZFC without equality, "$x=y$" is usually defined as "$x$ and $y$ have the same elements and belong to the same sets", or written symbolically:$$(x=y):=\mathrm{\forall }z[z\in x\iff z\in y]\wedge \mathrm{\forall }w[x\in w\iff y\in w].$$Then, the Axiom of Extensionality asserts that if two sets have the same elements, then they are equal, or symbolically: $$\mathrm{\forall }z(z\in x\iff z\in y)\Rightarrow (x=y).$$Base formulas

Let $X,Y,Z$, be metavariables for any variables or sets, such that $X=Y$ then $(Z\in X)\iff (Z\in Y)$, and $(X\in Z)\iff (Y\in Z)$.

Case 1:

$\varphi (X):(Z\in X)$

Assume

$Z\in X$

, then

$Z\in Y$

, thus

$(X=Y)⟹[Z\in X\Rightarrow Z\in Y]$

Case 2:

$\varphi (X):(X\in Z)$

Assume

$X\in Z$

, then

$Y\in Z$

, thus

$(X=Y)⟹[X\in Z\Rightarrow Y\in Z]$

Recursive formulas

Let $\psi ,\phi$ be meta variables for any formulas with the property that $(a=b)⟹[\varphi (a)\Rightarrow \varphi (b)]$. Let $X,Y$, be metavariables for any variables or sets, such such that $X=Y$, and let $z$ be a metavariable for any variable.

Case 1:

$\mathrm{\neg }(\psi )$

Since

$X=Y$

, then

$Y=X$

by symmetry of equality, therefore

$[\psi (Y)\Rightarrow \psi (X)]$

, by the induction hypothesis, therefore

$[\mathrm{\neg }\psi (X)\Rightarrow \mathrm{\neg }\psi (Y)]$

, thus

$(X=Y)⟹[\mathrm{\neg }\psi (X)\Rightarrow \mathrm{\neg }\psi (Y)]$

Case 2:

$\psi \wedge \phi$

Since

$X=Y$

, then

$[\psi (X)\Rightarrow \psi (Y)]$

and

$[\phi (X)\Rightarrow \phi (Y)]$

, which implies

$\left[\right(\psi (X)\wedge \phi (X))\Rightarrow \psi (Y)\wedge \phi (Y))]$

, thus

$(X=Y)⟹\left[\right(\psi (X)\wedge \phi (X))\Rightarrow \psi (Y)\wedge \phi (Y))]$

Case 3:

$\mathrm{\exists }z(\psi )$

Since

$X=Y$

,

$\psi (X,z)\Rightarrow \psi (Y,z)$

assume by way of contradiction that the result is false, that is

$\mathrm{\exists }z(\psi (X,z))$

is true but

$\mathrm{\exists }z(\psi (Y,z))$

is false. By existential instantiation, let

$z_0$

denote the value such that

$\psi (X,z_0)$

is true. Then

$\psi (Y,z_0)$

is false by asumption, and therefore

$\psi (X,z_0)\Rightarrow \psi (Y,z_0)$

is false, which contradicts our induction hypothesis, and the result follows.

Computer science

• Computer algebra

References

https://edisciplinas.usp.br/pluginfile.php/8029434/mod_resource/content/2/Stephen%20Cole%20Kleene-Introduction%20to%20Metamathematics-Wolters-Noordhoff%20Publishing%20%281971%29.pdf - Page 78

https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf - Page 5