# Tom_Breton comments on The Quotation is not the Referent

• In clas­si­cal logic, the op­er­a­tional defi­ni­tion of iden­tity is that when­ever ‘A=B’ is a the­o­rem, you can sub­sti­tute ‘A’ for ‘B’ [but it doesn’t fol­low that] I be­lieve 2 + 2 = 4 ⇒ I be­lieve TRUE ⇒ I be­lieve Fer­mat’s Last The­o­rem.

The prob­lem is that iden­tity has been treated as if it were ab­solute, as if when two things are iden­ti­cal in one sys­tem, they are iden­ti­cal for all pur­poses.

The way I see it, iden­tity is rel­a­tive to a given sys­tem. I’d define it thus: A=B in sys­tem S just if for ev­ery equiv­alence re­la­tion R that can be con­structed in S, R(A,B) is true. “Equiv­alence re­la­tion” is defined in the usual way: re­flex­ive, sym­met­ri­cal, tran­si­tive.

My for­mu­la­tion quan­tifies over equiv­alence re­la­tions, so it’s not prop­erly a re­la­tion in the sys­tem it­self. It “lives” in any meta-logic about S that sup­ports the defi­ni­tion’s mod­est com­po­nents: Abil­ity to dis­t­in­guish equiv­alence re­la­tions from other types, quan­tifi­ca­tion over equiv­alence re­la­tions in S, abil­ity to ap­ply a vari­able that’s known to be an equiv­alence re­la­tion, and abil­ity to con­join an ar­bi­trary num­ber of con­juncts. The fact that it’s not in the sys­tem also avoids the po­ten­tially para­dox­i­cal situ­a­tion of in­clud­ing ‘=’ among its own con­juncts.

Given my for­mu­la­tion, it’s eas­ily seen that iden­tity needs to be rel­a­tive to some sys­tem. If we were to quan­tify over all equiv­alence re­la­tions ev­ery­where, we would have to in­clude re­la­tions like “Be­gins with the same let­ter”, “Has the same ASCII rep­re­sen­ta­tion”, or “Is printed at the same lo­ca­tion on the page”. Th­ese re­la­tions would fail on A=B and on other equiv­alences that we cer­tainly should al­low at least some­times. In fact, the `=′ test would fail on ev­ery two ar­gu­ments, since the re­la­tion “is passed to the NNNNth call to`=′ as the same ar­gu­ment in­dex” must fail for those ar­gu­ments. It could only suc­ceed in a purely Pla­tonic sense. So iden­tity needs to be rel­a­tive to some sys­tem.

How can sys­tems differ in what equiv­alence re­la­tions they al­low, in ways that are rele­vant here? For in­stance, sup­pose you write a the­o­rem prover in Lisp. In the Lisp code, you definitely want to dis­t­in­guish sym­bols that have differ­ent names. Their names might even have de­com­pos­able mean­ing, eg in a field ac­ces­sor like `my-struct-my-field’. So im­plic­itly there is an equiv­alence re­la­tion­`has-same-name’ about the Lisp. In the the­o­rem prover it­self, there is no such re­la­tion as has-same-Lisp-name or even has-same-sym­bol-in-the­o­rem-prover. (You can of course feed the prover ax­ioms which model this situ­a­tion. That’s differ­ent, and doesn’t give you real ac­cess to these dis­tinc­tions)

Your text ed­i­tor in which you write the Lisp code has yet an­other differ­ent cat­a­log of equiv­alence re­la­tions. It in­cludes many dis­tinc­tions that are sen­si­tive to spel­ling or lo­ca­tion. They don’t trip us up here, they are just the sort of things that a text ed­i­tor should dis­t­in­guish and a the­o­rem prover shouldn’t.

The code in which your text ed­i­tor is writ­ten makes yet other dis­tinc­tions.

So what about the cases at hand? They are both about logic of be­lief (dox­as­tic logic). Dox­as­tic logic can con­tain equiv­alence re­la­tions that fail even on de re equiv­a­lent ob­jects. For in­stance, dox­as­tic logic should be able to say “Alice be­lieves A but not B” even when A and B are both true. Given that sort of ex­pres­sive ca­pa­bil­ity, one can con­struct the re­la­tion “Alice be­lieves ei­ther both A and B or nei­ther”, which is re­flex­ive, sym­met­ri­cal, tran­si­tive; it’s an equiv­alence re­la­tion and it treats A and B differ­ently.

So A and B are not iden­ti­cal here even though de re they are the same.