LESSWRONGLW

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.

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 relation`has-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)

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.

36

In classical logic, the operational definition of identity is that whenever 'A=B' is a theorem, you can substitute 'A' for 'B' in any theorem where B appears.  For example, if (2 + 2) = 4 is a theorem, and ((2 + 2) + 3) = 7 is a theorem, then (4 + 3) = 7 is a theorem.

This leads to a problem which is usually phrased in the following terms:  The morning star and the evening star happen to be the same object, the planet Venus.  Suppose John knows that the morning star and evening star are the same object.  Mary, however, believes that the morning star is the god Lucifer, but the evening star is the god Venus.  John believes Mary believes that the morning star is Lucifer. Must John therefore (by substitution) believe that Mary believes that the evening star is Lucifer?

Or here's an even simpler version of the problem.  2 + 2 = 4 is true; it is a theorem that (((2 + 2) = 4) = TRUE).  Fermat's Last Theorem is also true.  So:  I believe 2 + 2 = 4 => I believe TRUE => I believe Fermat's Last Theorem.

Yes, I know this seems obviously wrong.  But imagine someone writing a logical reasoning program using the principle "equal terms can always be substituted", and this happening to them.  Now imagine them writing a paper about how to prevent it from happening.  Now imagine someone else disagreeing with their solution.  The argument is still going on.

P'rsnally, I would say that John is committing a type error, like trying to subtract 5 grams from 20 meters.  "The morning star" is not the same type as the morning star, let alone the same thing.  Beliefs are not planets.

morning star = evening star
"morning star" ≠ "evening star"

The problem, in my view, stems from the failure to enforce the type distinction between beliefs and things.  The original error was writing an AI that stores its beliefs about Mary's beliefs about "the morning star" using the same representation as in its beliefs about the morning star.

If Mary believes the "morning star" is Lucifer, that doesn't mean Mary believes the "evening star" is Lucifer, because "morning star" ≠ "evening star".  The whole paradox stems from the failure to use quote marks in appropriate places.

You may recall that this is not the first time I've talked about enforcing type discipline—the last time was when I spoke about the error of confusing expected utilities with utilities. It is immensely helpful, when one is first learning physics, to learn to keep track of one's units—it may seem like a bother to keep writing down 'cm' and 'kg' and so on, until you notice that (a) your answer seems to be the wrong order of magnitude and (b) it is expressed in seconds per square gram.

Similarly, beliefs are different things than planets.  If we're talking about human beliefs, at least, then:  Beliefs live in brains, planets live in space.  Beliefs weigh a few micrograms, planets weigh a lot more.  Planets are larger than beliefs... but you get the idea.

Merely putting quote marks around "morning star" seems insufficient to prevent people from confusing it with the morning star, due to the visual similarity of the text.  So perhaps a better way to enforce type discipline would be with a visibly different encoding:

morning star = evening star
13.15.18.14.9.14.7.0.19.20.1.18 ≠ 5.22.5.14.9.14.7.0.19.20.1.18

Studying mathematical logic may also help you learn to distinguish the quote and the referent.  In mathematical logic, |- P (P is a theorem) and |- []'P' (it is provable that there exists an encoded proof of the encoded sentence P in some encoded proof system) are very distinct propositions.  If you drop a level of quotation in mathematical logic, it's like dropping a metric unit in physics—you can derive visibly ridiculous results, like "The speed of light is 299,792,458 meters long."

Alfred Tarski once tried to define the meaning of 'true' using an infinite family of sentences:

("Snow is white" is true) if and only (snow is white)
("Weasels are green" is true) if and only if (weasels are green)
...

When sentences like these start seeming meaningful, you'll know that you've started to distinguish between encoded sentences and states of the outside world.

Similarly, the notion of truth is quite different from the notion of reality.  Saying "true" compares a belief to reality.  Reality itself does not need to be compared to any beliefs in order to be real.  Remember this the next time someone claims that nothing is true.