Consider the following premises. forall z: P(z) -> T_2(z). forall z: T_2(z) -> P(z). p -> T_2(f). Can we infer ~(p -> P(f)) from them? If possible, name the inference rules being used at each step.
That contradicts the premises. Therefore the answer is no.