What precisely is a vacuous truth? Is there a proper and precise definition that goes something like this?
Definition. A statement $S$ is a vacuous truth if ... ...

An implication is said to be vacuously true if its antecedent is false.
$$\neg A \implies (A\implies B)$$
This logical principle is a tautology, and can be used to introduce an arbitrary consequent in an implication.
Example 1: If pigs can fly, then the President is a genius.
Proof: The antecedent, "pigs can fly," is false. Therefore the above implication is true, whether or not the consequent, "the President is a genius," is true. Note: We cannot infer from this that the President is not a genius. Nor can we infer the contrary that he is a genius.
Example 2: $\forall x: (x\in \emptyset \implies 0=1)$
Proof: $y\in \emptyset$ is always false. Then the implication $y\in \emptyset \implies 0=1 $ is true (vacuously so). Generalizing, we obtain as required: $$\forall x: (x\in \emptyset \implies 0=1)$$
