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.


  • 1
    $\begingroup$ 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 $\endgroup$ Dec 20, 2015 at 23:32
  • $\begingroup$ 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. $\endgroup$ Dec 20, 2015 at 23:33

1 Answer 1


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$


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .