What is the difference between a definition and an equivalence class?

Question

In what way is 'the definition of $x$ is $y$' ($x:=y$) not the same as '$x$ is equivalent to $y$' ($x=y$)? I can find no justification for making the distinction aside from 'it feels right'. It seems that every property of $:=$ is also a property of $=$ and that neither possesses a property that the other does not.

Furthermore, trying to casually force a distinction either renders one relation meaningless, with the other assuming the meaning of 'equality', or leads to glaringly obvious contradictions (ex $1:=S(0)\land S(0):\neq1\implies 1\in\Bbb{N}\land 1\notin\Bbb{N}$ using the Peano axioms).

Is there any objective distinction between a term and its definition (without explicit typing)?

I know its a bit (okay, extremely) pedantic to insist on a formal distinction between the definition of an object and the equivalence class to which that object belongs, but making this distinction effectively sets the limits on the definability of objects within a theory.

---

Note: the definition of an object is an equivalence class in the sense that a definition is specified via the conjunction of a sequence of formulae $(\Phi_i)_{i\in I}$, and the collection of objects $X=\{x\mid\bigwedge_{i\in I}\Phi_i(x)\}$ is an equivalence class since the relation $x\sim y\iff \left(\bigwedge_{i\in I}\Phi_i(x)\right)\land\left(\bigwedge_{i\in I}\Phi_i(y)\right) \iff x\in X\land y\in X$ is an equivalence relation. There are more technical details regarding the nature of this relation depending on whether or not a universe of discourse has been specified, but that's another thing entirely.

Answer 1

Equality, in many system and particularly for first-order logic with equality, is a relation of the logic. Most logical systems don't have a mechanism for making a definition. It simply makes no sense to say $(1:=S(0))\land P$ in these systems. A definition isn't a claim. It's not a statement that has a truth value.

So, not only are equality and definition not the same, they aren't even the same sort of thing. The most common way to handle definitions is meta-logically and informally. A definition like $1:=S(0)$ is an instruction to you, as the reader, to mentally replace $1$ with $S(0)$ everywhere you see it. You then trivially get $1=S(0)$ be reflexivity, because this really means $S(0)=S(0)$.

There are several ways of formalizing the notion of definitions. The typical way would be an extension by definition. For this perspective, a (meta-logical) definition like $1:=S(0)$ means: "Add the constant $1$ and the axiom $1=S(0)$ to the current theory, then continue with this new theory." Note how operational this is. It's instruction to create a new theory. "Add the constant $1$ and the axiom $1=S(0)$ to the current theory, then continue with this new theory," is not a statement that is true or false.

Some logical systems have an internal mechanism for making definitions. One example is the system used by Coq. The $\delta$-reductions do a formal version of the "mental replacement" described earlier. To over-simplify, it basically states that when you are in a context with a definition like $1:=S(0)$, then $1$ reduces to $S(0)$. The typing judgment is (supposed to be) sensitive only to normal forms of the reduction relation. There are constraints on the rules that introduce definitions to avoid (or clearly define the behavior of) multiple, potentially inconsistent definitions.

Answer 2

The notion of equality in mathematics that you've touched upon is something very deep.

Every axiomatic system in mathematics (that I am aware of) has some way of imbuing the canonical $=$ sign (if there even is a canonical notion of equality, which there sometimes is not) with some definitional value that is distinguished from just-any-other equivalence class defined over a structure.

In most (all?) versions of set theory, two sets are equal in the purest sense if they contain the same elements, and the elements of a set themselves are also just composed out of smaller sets (where axiomatically we only assume the existence of the empty set and a few ways of constructing new sets out of that) so all of the equality follows this same definition (in some sense, it reduces to being able to compare the empty set to any other set), whereas the same cannot be said of just any arbitrary equivalence relation over a set (although sometimes the equivalence of cosets under a quotient can confuse this).

If you're partial to constructive mathematics, then in certain forms of the calculus of inductive constructions, equality is just another inductive data type with nothing particularly special about it. Depending on the exact implementation of your type system though, you could end up with a definition of equality that basically boils down to two things having the same data representation on the computer. Or you could just as well come up with a very different kind of equality.

The real answer is that there are many different takes on this topic under many different systems, and to understand some of the variety involved I can only recommend checking out some type theory, axiomatic set theory, and category theory. This is a very good question, though, and one I wish I had a better answer for.