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.

2 comments:

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...

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