Definition of equality

Question

I wondered what the exact definition of equality would be and came across this question: Should this "definition" of set equality be an axiom?. I then proceeded to read the corresponding appendix of Tao's book in which he mentions the following:

Equality is a relation linking two objects $x,y$ of the same type $T$ (e.g. two integers or two matrices, or two vectors, etc.). Given two such objects $x$ and $y$, the statement $x=y$ may be true or may not be true; it depends on the value of $x$ and $y$ and also on how equality is defined for the class of objects under consideration. [...] How equality is defined depends on the class of objects $T$ under consideration, and to some extent is just a matter of definition. However, for the purpose of logic we require that equality obeys the following four axioms of equality: $(1)$ Given any object $x$, we have $x=x$. $(2)$ Given any two objects $x,y$ of the same type, if $x=y$ then $y=x$. $(3)$ Given any three objects of the same type, $x,y$ and $z$, if $x=y$ and $y=z$ then $x=z$. $(4)$ Given any two objects of the same type $x,y$, if $x=y$, then $f(x)=f(y)$ for all functions or operations $f$.

I now wonder, how is this used in practice? If I understand it correctly, equality is not defined explicitly but rather what properties equality should have. However in practice one usually is not given an explicit definition of equality. As far as I understand, one does not define equality explicitly which is justified since only the properties that come from the axioms $(1)-(4)$ are used, meaning no matter what explicit equality is used in practice, I obtain the same results. Further questions I have are the following:

Q$1$: Given a group $G$, what does it mean that for two objects, $g_1,g_2 \in G$, $g_1=g_2$? Are they literally the same object of the underlying set, since a set can only contain an element once? I am really unsure what equality should be here, since $G$ can be any group. (This question should work analogously for sets)

Q$2$: Is there an underlying equality for all classes $T$? If one does not define equality explicitly, one has to ensure that there is at least one notion of equality for all "situations", right? Why is that the case?

Q$3$: Given a function $f:A \to B$ and $a \in A$. Why is it possible to write: Let $b=f(a)$? Is this the case due to axiom $(1)$? Meaning that I could at least write $f(a)=f(a)$ or in other words choose $z$ to be $f(a)$?

Q$4$: Isn't axiom $(4)$ already satisfied due to functions being well defined, meaning in particular that for $a=b$ we have that $f(a)=f(b)$?

Answer 1

In most (maybe all) instances, equality is always taken to be at the set level.

But often in different areas of math, we often want take a more abstract view of objects so you define some kind of equivalence relation (e.g. group isomorphism, homeomorphism between topological spaces, etc) where even when two sets are not identical in the set-theoretic sense, they are equivalent in this new sense we are interested in.

Terrence Tao is being a bit loose with the word 'equality' there. I think 'equivalence' would have been a more precise term to use, but it's not uncommon to hear.

Also, equivalence relations satisfy (1)-(3) so they act like equality (equality is an equivalence relation).

Answer 2

My hope of a mathematics career ended thirty-five years ago because of the nature of your question. I have studied uses of the sign of equality during those years and have written both foundational axiomatizations and a geometric metamathematics to go along with them. As an amateur autodidact, my work will never see publication.

With respect to a logical calculus, the sign of equality can have only a substitutivity interpretation. The problem arises with the fact that substitutions require a warrant (a reason, a justification). In so far as "formalism" can be traced to Augustus de Morgan's work on symbolic algebra, he had observed that the sign of equality can never be purely formal for this reason.

Within the Peano axioms the treatment of succession provides for both well-formedness and substitutivity. The first is generally obfuscated by extra-mathematical stipulations about terms (inherited from universal algebra). The second is obfuscated by the linguistic analysis that declares mathematics to be reducible to signatures of constants, function symbols, and relation symbols. The axiom asserting that succession is well-defined would fall under the idea of an "identity criterion" for the theory.

Associating induction axioms with the structure of a system conflates logic with mathematics for anyone who is not a "logicist." The interest in weakenings of induction axioms to explain Hilbert's finitary mathematics would explain why I have brought up Peano arithmetic first. What Skolem had referred to as "the inductive mode of thought" is not explained by stipulating that mathematics reduces to stipulations, whereby induction becomes mathematics by stipulation.

The introduction of Moschovakis' "Elementary Induction over Abstract Structures" describes how a relatively standard mathematical statement that appears to be "second order" can be understood "more constructively" by iteration with respect to "given" individuals. Because this work is couched in the first-order paradigm, this term generation is understood as occurring within an ontology. Arguably, ontologies are the business of philosophers and logicians. That should give you a hint of why the necessary truth of reflexive equality statements is a stipulated truth of the first-order inference rules.

The necessary truth of reflexive equality statements is not an essential feature of Tarski's semantic conception of truth.

A curious aspect of recursion theory is the introduction of a special form of equality that allows one to distinguish between "defined" and "not defined." Authors sometimes use the sign for the empty set as a distinguished symbol representing an undefined expression. Then, all undefined expressions are set "equal" to this symbol. As a logical principle, this is called the indiscernibility of non-existents and is associated with negative free logic.

A finitist could be understood as someone who uses the sign of infinity for this same purpose in an arithmetical theory. The notion of "givenness" mentioned above may then be compared with Markov's discussion of "strengthened implication" in his theory of algorithms. All one needs to do is to use reflexive equality statements as part of a restricted quantification implementation. From the language of recursion theory, a universal quantifier restricted in this way would read, "If x is defined...."

Relative to negative free logic, one might notice that Tarski's work on cylindric algebra contains a transitivity axiom which would convey existential import to reflexive equality statements. Thus, one may formulate a logic whose universal quantifier reads, "If x exists...."

The first-order paradigm has its origins in logicism. So, ontologies are assumed and stipulated to exist as extra-mathematical presupposition. The necessary truth of reflexive equality statements arises either from this or from the metaphysical character of "the law of identity." A modern formalist might deny the metaphysics, where a logicist cannot. But, for example, the result is largely the same when reflexive equality statements are the basis for interpreting the universal quantifier.

An important historical aspect of the sign of equality involves the debate over the principle of the identity of indiscernibles. It is denied in the first-order paradigm. A modern justification for this denial is Wittgenstein's use of a geometric analogy in which names be treated as points. So, this yields a geometric basis for numerical identity.

In his book "Individuals," Strawson shows that this introduces an essential circularity between "parts" of space that separate points and "points" of space that separate parts. Consequently, one reads that "set theory" unfolds. For what it is worth, Strawson also highlights the problem with the qualitative identity which corresponds with the use of equivalence relations as proxies for equality.

An alternative criticism for the principle of the identity of indiscernibles had been Kant's use of geometry for numerical difference. Relative to the circularity identified by Strawson, a finitary geometric metamathematics would recognize a reduction to graph theory in which the circularity expresses itself between vertices and edges (and dual graphs).

Time to go to work for pay...

Continuing...

The finitary nature of ,Hilbert's metamathematics does not address the problems of proper mathematics. But, it yields a clue. Characterizing proper mathematics in terms of a dichotomy between syntax and semantics fails to account for the relationship of mathematics to language users. This third leg of mathematical foundations falls under "pragmatics" and is simply ignored by logicists. Hilbert's metamathematics had invoked the "sensible impressions of symbols" as the concrete basis for his proof theory.

Now consider the fact that logic is often introduced using Venn diagrams or Euler diagrams. These illustrations rely upon naive geometric coincidence to differentiate between individuals and classes of individuals, pictorially.And, this, of course may be with topological notions ubiquitous across ordinary mathematics. This is why deliberations about numerical identity or numerical difference involving geometric analogies apply to any foundational claims made by any foundational paradigm.

My initial axiomatic work had been motivated by Cantor's nested set theorem for closed sets of vanishing diameter. It treated "proper subset" and " membership" as primitive relations with membership having a syntactic dependency on proper subset. This is what one has with Venn diagrams and it fails.

Eventually, I would write separate axiomatizations differentiating between the logical atomism arising from Russell's atheism (yes, Cantor had not been the only one tying "mathematics" to religious opinions) and Czarsar' study of syntopogenous orders. Relative to the latter, my original "proper subset" became an intensional "proper part" with "proper subset" defined extensionally with respect to membership.

People who see the expression "proper part" often wish to invoke "mereology." People who see the expression "topology" often wish to invoke "intuitionism." Neither applies here. Understanding the use of syntopogenous orders algebraically is better approached from the standpoint of biordered sets as described by Easdown. And the intuitionism is addressed by the reference to Markov's classical logic.

In his book on analysis Eric Schecter speaks of gauge spaces as a set with a class of pseudometrics. The homotopy type theory advocate, Mike Schulman has an entry on gauge spaces at ncatlab.

Every topology carries an implicit class of guages with its open sets. The pseudometrics are based upon numerical difference between points with respect to a given open set. It would be this which corresponds to my "proper part" and the use of naive geometric incidence in the teaching of logic.

It is certainly true that self-substitution is needed in logical calculi. That does not justify the necessary truth of reflexive equality statements.

Question 1:

There is ambiguity with respect to whether equality is a relation between language terms or the underlying objects. Logical atomism in the sense of early Russell simply stipulates that terms are the objects. Driving this analogy to its reasonable conclusion, one will obtain Herbrand logic rather than first-order logic. Tarski's semantics, as applied for first-order logic, allows one to speak in a way that does not reduce mathematics to the terms of formal systems. So, one has issues related to discernibility with respect to what may be expressed by the well-formed formulas of a language. Set theorists often study cardinals that can be described with the logic if uncountable languages.

The demand that what works for groups ought to work for sets is where things get problematic. Strawson's analysis comes into play.

Question 2:

That is what logical atomism attempts to enforce by stipulation. That the "received view" of first-order logic has so many detractors (in a minority) suggests that it is often unsatisfactory for those who do due diligence with respect to the question.

Type theory differs in that identity is presumed to be meaningful only with respect to a type specification.

Question 3:

If you work with the idea of an underlying set theory similar to ZFC, it rests with how well definition for functions is represented un the set theory.

Category theory is different. Much of what is said above is related to the idea that categorical logic intentionally approaches logic "more geometrically."

Question 4:

That is addressed in the initial remarks about recursion theory.

Time for a real job again...