1. There is a thing, x, such that it is a contingent proposition.

∃xCx

2. For any thing, x, if x is a contingent proposition then there is a possible world, w, where x is true, and there exists a possible world, w’, where x is false.

∃xCx→∃x∃w∃w’Pxaw∧Pxbw’

3. Thus, there is a thing, x, and there is a possible world, w, and there is a possible world, w’, such that x has the property true in world w and x has the property false in w’.

⊢ ∃x∃w∃w’Pxaw∧Pxbw’ [1, 2, MP]

4. For any thing, x, and for any possible world, w, if x has the property true or has the property false in w, then x exists in w.

∃x∃wPxaw→∃x∃wExw

5. Thus, there is a thing, x, and there is a possible world, w, and there is a possible world, w’, such that x exists in w and x exists in w’ and

⊢∃x∃w∃w’Exw∧Exw’∧Pxaw∧Pxbw’ [3, 4, MP]

6. For any thing, x, for any possible world, w, x has the property true iff x does not hasve the property false.

∀x∀w(Pxaw↔¬Pxbw)

7. For any thing, x, and for any thing, y, for any possible world, w, and for any possible world, w’, if x exists in w and y exists in w’, then (x and y are identical iff for any property, z, if x has it in w, then y has it in w’).

∀x∀y∀w∀w'(Exw∧Eyw’)→(x=y↔(∀zPxzw↔Pyzw’))

This set is inconsistent (5∧6→¬7)^{1}. But it seems clear to me that we ought to give up 7.

### Notes

1I thought about giving the proof tree but it would be awfully long. Until I have an automatic way of doing this, I won’t prove such complex argument beyond formalizing them.