Consider the following premises. U(f_3) <-> q_4. forall y: U(y) <-> P_4(y). forall y: ~P_4(y). Can we infer q_4 from them?
 From forall y: U(y) <-> P_4(y), forall y: ~P_4(y) we can infer forall y: ~U(y). From forall y: ~U(y) we can infer ~U(f_3). From U(f_3) <-> q_4 we can infer q_4 -> U(f_3). Finally, from q_4 -> U(f_3), ~U(f_3) we can infer ~q_4, which contradicts q_4. Therefore, the answer is no.