Consider the following premises. P(g_2) or w_4. w_4 -> W_3(g_2). forall z: W_3(z) -> P(z). forall z: P(z) -> W_3(z). Can we infer ~W_3(g_2) from them? If possible, name the inference rules being used at each step.
 From forall z: P(z) -> W_3(z), forall z: W_3(z) -> P(z) we can infer forall z: P(z) <-> W_3(z) via universal biconditional introduction. From forall z: P(z) <-> W_3(z) we can infer P(g_2) <-> W_3(g_2) via universal instantiation. From P(g_2) <-> W_3(g_2) we can infer P(g_2) -> W_3(g_2) via biconditional elimination. Finally, from P(g_2) -> W_3(g_2), w_4 -> W_3(g_2), P(g_2) or w_4 we can infer W_3(g_2) via disjunction elimination, which contradicts ~W_3(g_2). Therefore, the answer is no.