Monday, November 06, 2006

When is identity not identity?

In Kripke model semantics for intuitionistic first-order logic, it turns out that you can't interpret '=' as the identity relation between objects in the domains. You can interpret it as a mapping from domains to domains.
[Edit: as Aidan pointed out, leaving open the possibility of ~(x=y OR ~x=y), what I said previously, doesn't make sense. The following is what I meant to say.]
The reason is that you need to leave open the possibility that for some x and y, at node a x=y is not true (a doesn't force x=y) but at some node b>=a, x=y is true at b (b forces x=y), which means that a doesn't force ~x=y.
If you want decidable equality you don't have to worry about this. If you're dealing with classical logic, you get excluded middle, so I think you can use the identity relation and get all the puzzles about trans-world identity. However, for Kripke models of classical logic, there is only one world, so only one domain. I'm not sure how the puzzles creep in exactly.


Aidan said...

I'm afraid I'm a little confused. Isn't ~~(x=y OR ~x=y) going to be a theorem of intuitionist logic for all x and y? If so, in what way do we need to 'leave open' the possibility you mention?

(I should say I'm not really that familiar with intuitionist FOL, so I might just be missing something obvious here).

Shawn said...

I checked my notes, and you are right. I wrote the wrong thing. I will post a correction.