Editing Equality (mathematics) (section)

== In logic ==

=== History ===
[[File:Aristotle Altemps Inv8575.jpg|thumb|upright=1.2|Roman copy in marble of a Greek bronze bust of [[Aristotle]] by [[Lysippos]], c.&nbsp;330&nbsp;BC, with modern alabaster mantle]]
Equality is often considered a [[primitive notion]], informally said to be "a relation each thing bears to itself and to no other thing".<ref>{{Cite book |last=Zalabardo |first=Jose L. |title=Introduction To The Theory Of Logic |date=2000 |publisher=[[Routledge]] |isbn=978-0-429-49967-8 |location=New York |doi=10.4324/9780429499678}}</ref> This tradition can be traced back to at least 350&nbsp;BC by [[Aristotle]]: in [[Categories (Aristotle)|his ''Categories'']], he defines the notion of ''quantity'' in terms of a more primitive ''equality'' (distinct from [[Identity (philosophy)|identity]] or similarity), stating:<ref>{{Cite web |translator-last=Edghill |translator-first=E. M. |author-link=E. M. Edghill |publisher=The Internet Classics Archive, MIT |title=Categories |author=Aristotle |url=https://classics.mit.edu/Aristotle/categories.1.1.html |access-date=2025-01-23}}</ref>
<blockquote>The most distinctive mark of quantity is that equality and inequality are predicated of it. Each of the aforesaid quantities is said to be equal or unequal. For instance, one solid is said to be equal or unequal to another; number, too, and time can have these terms applied to them, indeed can all those kinds of quantity that have been mentioned.{{pb}}That which is not a quantity can by no means, it would seem, be termed equal or unequal to anything else. One particular disposition or one particular quality, such as whiteness, is by no means compared with another in terms of equality and inequality but rather in terms of similarity. Thus it is the distinctive mark of quantity that it can be called equal and unequal. ―&thinsp;(translated by [[E. M. Edghill]])</blockquote>
Aristotle had separate categories for [[quantities]] (number, length, volume) and [[quality (philosophy)|qualities]] (temperature, density, pressure), now called [[intensive and extensive properties]]. The [[Scholastics]], particularly [[Richard Swineshead]] and other [[Oxford Calculators]] in the 14th century, began seriously thinking about [[kinematics]] and quantitative treatment of qualities. For example, two flames have the same heat-intensity if they produce the same effect on water (e.g, warming vs [[boiling]]). Since two intensities could be shown to be equal, and equality was considered the defining feature of quantities, it meant those intensities were quantifiable.<ref>{{Cite journal |last=Clagett |first=Marshall |author-link=Marshall Clagett |date=1950 |title=Richard Swineshead and Late Medieval Physics: I. The Intension and Remission of Qualities (1) |journal=Osiris |volume=9 |pages=131–161 |doi=10.1086/368527 |jstor=301847 |issn=0369-7827}}</ref><ref>{{Cite journal |last=Grant |first=Edward |date=1972-08-01 |title=Nicole Oresme and the medieval geometry of qualities and motions. A treatise on the uniformity and difformity of intensities known as 'tractatus de configurationibus qualitatum et motuum' |translator-first=Marshall |translator-last=Clagett |publisher=University of Wisconsin Press |location=Madison/Milwaukee |url=https://www.sciencedirect.com/science/article/abs/pii/0039368172900222?fr=RR-2&ref=pdf_download&rr=90fe00ac2def6dd9 |journal=Studies in History and Philosophy of Science Part A |volume=3 |issue=2 |pages=167–182 |doi=10.1016/0039-3681(72)90022-2 |bibcode=1972SHPSA...3..167G |issn=0039-3681}}</ref>

Around the 19th century, with the growth of modern logic, it became necessary to have a more concrete description of equality. With the rise of [[predicate logic]] due to the work of [[Gottlob Frege]], logic shifted from being focused on classes of objects to being property-based. This was followed by a movement for describing mathematics in logical foundations, called [[logicism]]. This trend lead to the axiomatization of equality through the [[law of identity]] and the [[Substitution (logic)#Mathematics|substitution property]] especially in [[mathematical logic]]<ref name="Suppes1957" /><ref name="Mendelson1964">{{harvnb|Mendelson|1964|page=75}}</ref> and [[analytic philosophy]].<ref>{{Cite encyclopedia |last1=Noonan |first1=Harold |title=Identity |date=2022 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/entries/identity/#LogiIden |access-date=2025-01-11 |edition=Fall 2022 |publisher=Metaphysics Research Lab, Stanford University |last2=Curtis |first2=Ben |editor2-last=Nodelman |editor2-first=Uri}}</ref>

The precursor to the substitution property of equality was first formulated by [[Gottfried Leibniz]] in his ''[[Discourse on Metaphysics]]'' (1686), stating, roughly, that "No two distinct things can have all properties in common." This has since broken into two principles, the substitution property (if <math>x=y,</math> then any property of <math>x</math> is a property of <math>y</math>), and its [[Converse (logic)|converse]], the [[identity of indiscernibles]] (if <math>x</math> and <math>y</math> have all properties in common, then <math>x=y</math>).<ref>Forrest, Peter, "[https://plato.stanford.edu/entries/identity-indiscernible/#Form The Identity of Indiscernibles]", The Stanford Encyclopedia of Philosophy (Winter 2020 Edition), Edward N. Zalta (ed.)</ref> Its introduction to logic, and first symbolic formulation is due to [[Bertrand Russell]] and [[Alfred North Whitehead|Alfred Whitehead]] in their ''{{lang|la|[[Principia Mathematica]]}}'' (1910), who claim it follows from their [[axiom of reducibility]], but credit Leibniz for the idea.<ref name="Russell1910">{{Cite book |last1=Russell |first1=Bertrand |author-link1=Bertrand Russell |title=Principia Mathematica |volume=1 |last2=Whitehead |first2=Alfred |author-link2=Alfred North Whitehead |url=https://archive.org/details/dli.ernet.247278/ |publisher=[[Cambridge University Press]] |year=1910 |page=57 |oclc=729017529}}</ref>

=== Axioms ===
[[File:Gottfried Wilhelm Leibniz, Bernhard Christoph Francke.jpg|thumb|[[Gottfried Wilhelm Leibniz|Gottfried Leibniz]], a major contributor to [[17th-century mathematics]] and [[philosophy of mathematics]], and whom the ''Substitution property of equality'' is named after.|upright=1.2]]
''[[Law of identity]]'': Stating that each thing is identical with itself, without restriction. That is, [[Universal quantification|for every]] <math>a,</math> <math>a = a.</math> It is the first of the traditional [[Law of thought#The three traditional laws|three laws of thought]].<ref>"Laws of thought".  ''[[The Cambridge Dictionary of Philosophy]]''.  [[Robert Audi]], Editor,  Cambridge University Press. p. 489.</ref> Stated symbolically as:

<math display="block">\forall a(a = a)</math>

''[[Substitution (logic)#Mathematics|Substitution property]]'': Sometimes referred to as ''[[Gottfried Wilhelm Leibniz|Leibniz's]] law'',<ref>{{Cite encyclopedia |title=Identity of indiscernibles |url=https://www.britannica.com/science/identity-of-indiscernibles |access-date=2025-01-12 |encyclopedia=Encyclopædia Britannica}}</ref> 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 {{mvar|a}} and {{mvar|b}}, and any [[Well-formed formula|formula]] <math>\phi(x),</math> (with a [[free variable]] {{mvar|x}}), if <math>a=b,</math> then <math>\phi(a)</math> [[Material conditional#Definitions|implies]] <math>\phi(b).</math> Stated symbolically as:

<math display="block">(a=b) \implies \bigl[ \phi(a) \Rightarrow \phi(b) \bigr]</math>

Function application is also sometimes included in the axioms of equality,<ref name="Grishin" /> but isn't necessary as it can be deduced from the other two axioms, and similarly for symmetry and transitivity. (See {{Section link||Derivations of basic properties}}) In [[first-order logic]], these are [[axiom schema]]s (usually, see below), each of which specify an infinite set of axioms.<ref name="Hodges1983">{{Cite book |last=Hodges |first=Wilfrid |date=1983 |editor-last=Gabbay |editor-first=D. |editor2-last=Guenthner |editor2-first=F. |title=Handbook of Philosophical Logic |publisher=Springer |location=Dordrecht |pages=68–72 |doi=10.1007/978-94-009-7066-3 |isbn=978-94-009-7068-7}}</ref> If a theory has a predicate that satisfies the Law of Identity and Substitution property, it is common to say that it "has equality", or is "a theory with equality".{{Sfn|Mendelson|1964|pp=82–83}}

The use of "equality" here somewhat of a [[misnomer]] in that any system with equality can be modeled by a theory without standard identity, and with [[indiscernibles]].<ref>{{Cite encyclopedia |last1=Deutsch |first1=Harry |title=Relative Identity |date=2024 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/entries/identity-relative/ |access-date=2025-01-20 |edition=Fall 2024 |publisher=Metaphysics Research Lab, Stanford University |last2=Garbacz |first2=Pawel |editor2-last=Nodelman |editor2-first=Uri}}</ref><ref name="Hodges1983" /> Those two axioms are strong enough, however, to be isomorphic to a model with idenitity; that is, if a system has a predicate staisfying those axioms {{Em|without}} standard equality, there is a model of that system {{Em|with}} standard equality.<ref name="Hodges1983" /> This can be done by defining a new [[Domain of discourse|domain]] whose objects are the [[equivalence class]]es of the original "equality".{{Sfn|Kleene|1967|pp=158-161}} If the relation is interpreted as equality, then those properties are enough, since if <math>x</math> has all the same properties as <math>y,</math> and <math>x</math> has the property of being equal to <math>x,</math> then <math>y</math> has the property of being equal to <math>x.</math><ref name="Russell1910" /><ref>{{Cite book |last=Suppes |first=Patrick |url=https://web.mit.edu/gleitz/www/Introduction%20to%20Logic%20-%20P.%20Suppes%20(1957)%20WW.pdf#page=120 |title=Introduction to Logic |date=1957 |publisher=[[Van Nostrand Reinhold]] |location=New York |page=103 |lccn=57-8153}}</ref>

As axioms, one can [[Logical consequence|deduce]] from the first using [[universal instantiation]], and the from second, given <math>a = b</math> and <math>\phi (a),</math> by using [[modus ponens]] twice. Alternatively, each of these may be included in logic as [[Rule of inference|rules of inference]].<ref name="Hodges1983" /> The first called "equality introduction", and the second "equality elimination"<ref>{{Cite web |title=Introduction to Logic – Equality |url=http://logic.stanford.edu/intrologic/extras/equality.html |access-date=2025-03-01 |website=logic.stanford.edu}}</ref> (also called [[paramodulation]]), used by some [[Theoretical computer science|theoretical computer scientists]] like [[John Alan Robinson]] in their work on [[Resolution (logic)|resolution]] and [[automated theorem proving]].<ref>{{cite book |last1=Nieuwenhuis |first1=Robert |url={{GBurl|HxaWA4lep_kC |pg=PR9}} |title=Handbook of Automated Reasoning |last2=Rubio |first2=Alberto |date=2001 |publisher=Elsevier |isbn=978-0-08-053279-0 |editor1-last=Robinson |editor1-first=Alan J. A. |pages=371–444 |chapter=7. Paramodulation-Based Theorem Proving |editor2-last=Voronkov |editor2-first=Andrei |chapter-url=http://www.cmi.ac.in/~madhavan/courses/theorem-proving-2014/reading/Nieuwenhuis-Rubio.pdf}}</ref>

=== Derivations of basic properties ===
* '''Reflexivity:''' Given any expression <math>a,</math> by the Law of Identity, <math>a = a.</math>{{Snf|Mendelson|1964|pp=93-95}}
* '''Symmetry:''' Given <math>a = b,</math> take the formula <math>\phi(x) : x = a.</math> So we have <math>(a=b) \implies ((a=a) \Rightarrow (b=a))  .</math> Since <math>a=b</math> by assumption, and <math>a=a</math> by Reflexivity, we have that <math>b=a.</math>{{Snf|Mendelson|1964|pp=93-95}}<!--
-->
* '''Transitivity:''' Given <math>a = b</math> and <math>b = c,</math> take the formula <math>\phi(x): x=c.</math> So we have <math>(b=a) \implies ((b=c) \Rightarrow (a=c)).</math> Since <math>b=a</math> by symmetry, and <math>b=c</math> by assumption, we have that <math>a=c.</math>{{Snf|Mendelson|1964|pp=93-95}}<!--
-->
* '''Function application:''' Given some [[Function (mathematics)|function]] <math>f(x)</math> and expressions {{math|''a''}} and {{math|''b''}}, such that {{math|1=''a'' = ''b''}}, then take the formula <math>\phi(x): f(a) = f(x).</math>{{Snf|Mendelson|1964|pp=93-95}} So we have:<br /><math>(a=b) \implies [(f(a) = f(a)) \Rightarrow (f(a) = f(b))]</math> <br />Since <math>a=b</math> by assumption, and <math>f(a) = f(a)</math> by reflexivity, we have that <math>f(a) = f(b).</math>