Consider the following premises. ~R(a_4). forall z: P(z) <-> R(z). Can we infer ~P(a_4) from them?
 From forall z: P(z) <-> R(z) we can infer forall z: P(z) -> R(z). From forall z: P(z) -> R(z) we can infer P(a_4) -> R(a_4). Finally, from P(a_4) -> R(a_4), ~R(a_4) we can infer ~P(a_4). Therefore, the answer is yes.