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.

### Like this:

Like Loading...

*Related*

## 2 comments

Comments feed for this article

November 20, 2006 at 1:17 am

AidanI’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).

November 20, 2006 at 3:33 am

ShawnAidan,

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