Consider the following premises. t_2 -> w. T(i) -> t_2. ~w. forall x: T(x) <-> T_4(x). Can we infer T_4(i) from them? If possible, name the inference rules being used at each step.
 From t_2 -> w, ~w we can infer ~t_2 via modus tollens. From forall x: T(x) <-> T_4(x) we can infer T(i) <-> T_4(i) via universal instantiation. From T(i) -> t_2, ~t_2 we can infer ~T(i) via modus tollens. Finally, from T(i) <-> T_4(i), ~T(i) we can infer ~T_4(i) via biconditional elimination, which contradicts T_4(i). Therefore, the answer is no.