> In case it wasn't clear, I'm hoping someone can explain how this notion of equivalence differs from what we've traditionally called equality since middle school, given that the latter doesn't appear to mean exactly the same either.
The point is that what's called "equality" in current foundations of mathematics is not equality in the middle-school math sense, but something far more restrictive. There are older, property-based notions of "equivalence relation" that broaden this a bit, but not nearly enough for many uses. OP describes a logical formalism that might enable us to make rigorous, watertight inferences about something really, really close to what a middle-schooler would call "equality". It gets rid of a pervasive abuse of mathematical language and notation, a worrying "gap" in previous attempts to make mathematical reasoning rigorous.
The point is that what's called "equality" in current foundations of mathematics is not equality in the middle-school math sense, but something far more restrictive. There are older, property-based notions of "equivalence relation" that broaden this a bit, but not nearly enough for many uses. OP describes a logical formalism that might enable us to make rigorous, watertight inferences about something really, really close to what a middle-schooler would call "equality". It gets rid of a pervasive abuse of mathematical language and notation, a worrying "gap" in previous attempts to make mathematical reasoning rigorous.