Does the sentence "prove that two things are equal" has a sense?

Question

"In modern first-order logic equality is primitive. We don't define it, we just know that two things are equal if and only if they are the same thing. So two numbers are equal if and only if they are the same number."-Asaf Karagila

This sentence is extracted from the following question How do we define equality in real numbers?.

I'm writing an article that is not strictly pure logic, but i would like to give a definition of equality (in no particular space) , or at least give something more than "these are equal if they are."

Has someone a track to give me ? Maybe a reference or an advice ?

Also, is it possible to give a sense to the sentence "prove that two things are equal" ?

I've read about the Leibniz identity of indiscernibles , but it seems like a consequence of the equality of two objects. why is the latter can not be given as an equivalence ? that seems very interesting

Answer 1

Set theoretically: Equality on a set $I$ is any fixed equivalence relation that we choose and decide to treat as defining equality.

Category theoretically: Equality in the fiber over $I$ of a fibration $E\to B$ is a left adjoint to the re-indexing functor induced by the diagonal $I\to I\times I$ (assuming that $B$ is products), evaluated at the terminal object of the fiber. To see why this makes sense, consider the predicate fibration, where the fiber over a set $I$ is precisely the power set $\mathcal P(I)$. It is then a straightforward verification that the left adjoint to the evident functor $\mathcal P(I\times I)\to \mathcal P (I)$, evaluated at $I$, is the identity relation on $I$.

Answer 2

One way to understand equality in mathematics is via Type Theory.

See e.g. Ansten Klev, The Justification of Identity Elimination in Martin‑Löf’s Type Theory (Topoi, 2017).

The basic notion is that of evaluation:

In the explanation of the forms of categorical judgement the notion of evaluation plays an important role. The following examples suggest what one should understand by evaluation.

$(3 + 2)! \times 4$ evaluates to $480$

$x.(\text {Prime}(x) ∧ x > (3 + 2)! \times 4)$ evaluates to $487$.

Thus, ordinary arithmetical computation are instances of evaluation.

Ordinary mathematical equations can thus be interpreted as computations, using the usual formal definitions of the arithmetical operations of sum and product

Making the definitions $1 = s(0) ∶ \mathbb N$ and $2 = s(1) ∶ \mathbb N$, one can then see that $2 + 2$ is an element of $\mathbb N$, since [this expression] evaluates to $s(2 + 1)$ [which in turn evaluates to $s(s(2+0))$ and then to $s(s(2))$] .

Thus, making the definition $3 = s(2) ∶ \mathbb N$, we have $2 + 2 = 3 + 1 ∶ \mathbb N$, since the left hand side evaluates to $s(2 + 1)$ [i.e. to $s(s(2))$] and the right hand side to $s(3 + 0)$ [i.e. to $s(s(2))$].

Answer 3

The other answers have covered category theory and type theory, but I'd like to add a few words about set theory. Zermelo-Frankel set theory is often presented using a language with a single non-logical symbol $\in$ for the membership relation and without equality. Equality is then defined by:

$$x = y \equiv \forall z(z \in x \iff z \in y)$$

If you agree to work in a world of "pure" sets whose essence is defined by the membership relation, then this is a very satisfactory explication of equality. In practice, this point of view doesn't accord so well with traditional mathematical thinking: I don't show that $\pi \neq 2\pi$ by examining the "members" of $\pi$ and $2\pi$. See Benecereaf's celebrated paper What numbers could not be.