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* &equiv *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.
[Here is a proof.]
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 since (i) *P* and *T* necessarily
imply the same properties, (ii) *b* encodes all and only the
properties necessarily implied by *P*, and (iii) *c*
encodes all and only the properties necessarily implied by *T*,
then *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.