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.

Advertisements