IsTheFormOf(b,P) &Participates_{PH}(d,b) & ¬dP

Consider the necessarily empty property
being-*Q*-and-not-*Q* (for some arbitrarily chosen
property *Q*). Call this property *P*. I.e.,
*P* = [λz *Qz* & ¬*Qz*].
Consider a distinct necessarily empty property, say, the property of
being-round-and-square, and call this property *T*. I.e.,
*T* = [λz *Rz* &
*Sz*]. Note that in object theory one can
consistently assert that *P* ≠ *T* even though
□∀*x*(*Px* ≡ *Tx*). The
reason is that identity for properties (‘*F* =
*G*’) is defined as □∀*x*(*xF*
≡ *xG*). So properties may be distinct even though
necessarily equivalent.

Now the following two facts are theorems of quantified modal logic:

[□∀y¬Fy& □∀y¬Gy] → □∀x(Fx≡Gx)□∀

x(Fx≡Gx) → ∀H(F⇒H≡G⇒H)

The first asserts that necessarily empty properties are
necessarily equivalent. (Clearly, if neither *F* nor
*G* are exemplified by any objects at any possible world, then
*F* and *G* are exemplified by all and only the same
objects at every possible world.) The second asserts that necessarily
equivalent properties necessarily imply the same properties. Clearly,
both of these theorems apply to *P* and *T* as we have
defined them; so from the fact that *P* and *T* are
necessarily empty, it follows that they necessarily imply the same
properties.

Now choose *b* to be the abstract object that encodes all and
only the properties implied by *P*. Then, it is straighforward
to verify that *IsTheFormOf*(*b*,*P*). And
choose *c* to be the abstract object that encodes all and only
the properties implied by *T*. So we also know that
*IsTheFormOf*(*c*,*T*). Now even though
*P* ≠ *T*, it follows that *b* = *c*.
To see this, note that from the facts:

*b*encodes all and only the properties necessarily implied by*P*,*c*encodes all and only the properties necessarily implied by*T*, and*P*and*T*necessarily imply the same properties,

it follows that *b* and *c* encode the same properties.
Thus *b* = *c*, by the definition of identity for
abstract objects.

We can complete the countermodel by considering the abstract object
*d* which encodes just one property, namely, *T*. We
can now establish (i)
*Participates*_{PH}(*d*,*b*),
and (ii) ¬*dP*. To establish (i), we have to show:

(A) ∃F(IsTheFormOf(b,F) &dF)

So, if we can show
*IsTheFormOf*(*b*,*T*) & *dT*, we can
generalize to get (A). To show
*IsTheFormOf*(*b*,*T*), we simply note that we've
already established both *IsTheFormOf*(*c*,*T*)
and *b*=*c*. So
*IsTheFormOf*(*b*,*T*). And clearly, by
definition of *d*, we know *dT*. So, by existential
generalization, we have established (i)
*Participates*_{PH}(*d*,*b*).
To establish (ii), note that by definition, *d* encodes only a
single property, namely, *T*. Since *P* ≠ *T*,
it follows that ¬*dP*.

IsTheFormOf(b,P) &Participates_{PH}(d,b) & ¬dP

Q.E.D.