IsTheFormOf(b,P) & ParticipatesPH(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) ParticipatesPH(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) ParticipatesPH(d,b). To establish (ii), note that by definition, d encodes only a single property, namely, T. Since P ≠ T, it follows that ¬dP.
So we've identified objects b and d and property P such that:IsTheFormOf(b,P) & ParticipatesPH(d,b) & ¬dP
Q.E.D.