Consider the following premises. T_1(g) -> w_1. forall y_4: S(y_4) -> T_1(y_4). w_1 -> S(g). Can we infer ~(T_1(g) <-> S(g)) from them?
 From forall y_4: S(y_4) -> T_1(y_4) we can infer S(g) -> T_1(g). From T_1(g) -> w_1, w_1 -> S(g) we can infer T_1(g) -> S(g). Finally, from T_1(g) -> S(g), S(g) -> T_1(g) we can infer T_1(g) <-> S(g), which contradicts ~(T_1(g) <-> S(g)). Therefore, the answer is no.