In classical logic, the operational definition of identity is that whenever ‘A=B’ is a theorem, you can substitute ‘A’ for ‘B’ [but it doesn’t follow that]
I believe 2 + 2 = 4 ⇒ I believe TRUE ⇒ I believe Fermat’s Last Theorem.
The problem is that identity has been treated as if it were absolute, as if when two things are identical in one system, they are identical for all purposes.
The way I see it, identity is relative to a given system. I’d define it thus: A=B in system S just if for every equivalence relation R that can be constructed in S, R(A,B) is true. “Equivalence relation” is defined in the usual way: reflexive, symmetrical, transitive.
My formulation quantifies over equivalence relations, so it’s not properly a relation in the system itself. It “lives” in any meta-logic about S that supports the definition’s modest components: Ability to distinguish equivalence relations from other types, quantification over equivalence relations in S, ability to apply a variable that’s known to be an equivalence relation, and ability to
conjoin an arbitrary number of conjuncts. The fact that it’s not in the system also avoids the potentially paradoxical situation of including ‘=’ among its own conjuncts.
Given my formulation, it’s easily seen that identity needs to be relative to some system. If we were to quantify over all equivalence relations everywhere, we would have to include relations like “Begins with the same letter”, “Has the same ASCII representation”, or “Is printed at the same location on the page”. These relations would fail on A=B and on other equivalences that we certainly should allow at least sometimes. In fact, the =′ test would fail on every two arguments, since the relation “is passed to the NNNNth call to=′ as the same argument index” must fail for those arguments. It could only succeed in a purely Platonic sense. So identity needs to be relative to some system.
=′ test would fail on every two arguments, since the relation “is passed to the NNNNth call to
How can systems differ in what equivalence relations they allow, in ways that are relevant here? For instance, suppose you write a theorem prover in Lisp. In the Lisp code, you definitely want to distinguish symbols that have different names. Their names might even have decomposable meaning, eg in a field accessor like my-struct-my-field’. So implicitly there is an equivalence relationhas-same-name’ about the Lisp. In the theorem prover itself, there is no such relation as has-same-Lisp-name or even has-same-symbol-in-theorem-prover. (You can of course feed the prover axioms which model this situation. That’s different, and doesn’t give you real access to these distinctions)
my-struct-my-field’. So implicitly there is an equivalence relation
Your text editor in which you write the Lisp code has yet another different catalog of equivalence relations. It includes many distinctions that are sensitive to spelling or location. They don’t trip us up here, they are just the sort of things that a text editor should distinguish and a theorem prover shouldn’t.
The code in which your text editor is written makes yet other distinctions.
So what about the cases at hand? They are both about logic of belief (doxastic logic). Doxastic logic can contain equivalence relations that fail even on de re equivalent objects. For instance, doxastic logic should be able to say “Alice believes A but not B” even when A and B are both true. Given that sort of expressive capability, one can construct the relation “Alice believes either both A
and B or neither”, which is reflexive, symmetrical, transitive; it’s an equivalence relation and it treats A and B differently.
So A and B are not identical here even though de re they are the same.