What is the correct way to apply contrapositive law in a proposition using universal quantifiers? Its possible to eliminate the quantifier?

Question

I reach the following conclusion during a proof: $(\forall x)(\forall y)([y < x \Rightarrow H(y) < H(x)])$, the contrapositive of this statment is $(\forall x)(\forall y)([H(x) \leq H(y) \Rightarrow x \leq y])$ or should I modify something in the universal quantifiers too? and what about the quantifiers elimination, its possible to do this in a simple case like this one?

Answer 1

Your contraposition is correct.

If you form the contraposition of an implicative subformula, then the resulting formula will be logically equivalent after substituting the implication for the contraposition, and the rest of the formula remains unchanged, so you don't tinker with the quantifiers around the implication.

As for quantifier eliminiation: This formula has two universal quantifiers in front, which can be directly eliminated, yielding again just

$$H(x) \leq H(y) \Rightarrow x \leq y$$