# Well-formed formula a theorem in first-order system K

I'm trying to show that the following well formed formula is a theorem of K:

$(\forall{x_i})\sim(A \to B) \to ((\forall{x_i})A \to (\forall{x_i})\sim B)$

Before going any further, I've rewritten it:

$(\forall{x_i})\sim(A \to B) \to (\forall{x_i})(A \to \sim B)$

which is equivalent to:

$(\forall{x_i})(\sim(A \to B) \to (A \to \sim B))$

which is a tautology and as such the wff is a theorem in K. Is this considered a complete proof that the wff is a theorem of K? I could go ahead and use the deduction theorem and the axioms of K but this seems like a faster way, assuming all the formulas above are in fact logically equivalent.

Thanks

• I don't think you can rewrite $(\forall x\, A) \to (\forall x \,B)$ like in the first step. You should first rewrite it to $(\forall x \,A) \to (\forall y \,\tilde{B})$ and then to $(\exists x \forall y)\, (A\to \tilde{B}$) where $\tilde{B}$ is $B$ with each occurance of $x$ replaced by $y$, etc Dec 20, 2015 at 23:32
• Please make sure to say what "K" is. I am used to seeing that term in the context of modal logic, rather than first-order logic. At the risk of exposing my ignorance, I don't know what "K" is supposed to mean here. Dec 20, 2015 at 23:33

Note that $((\forall{x_i})A \to (\forall{x_i})\sim B)$ is not equivalent to $(\forall{x_i})(A \to \sim B)$ If you have one of the $x_i$ for which $A$ is false, the first statement is true because the antecedent is false. For the second, you must have $A$ true for all the $x_i$ and $B$ false for all the $x_i$