Being vacuously true is a definition? 'If $p$ is false, then $p\rightarrow q$ is vacuously true.' Do we have to prove this or is this statement a definition? I have seen a lot of examples explaining this statement but I feel like those examples only explain why it makes sense to say that the statement is true.
 A: Here is a proof of the fact from http://proofs.openlogicproject.org/

Alternatively, if you define $P\to Q$ as a shorthand for $\neg P \vee Q$ (as many logical systems do), then again it is readily apparent that $P$ being false makes the statement true.
A: This is arguably a definition of what "vacuously true" means, namely that it is an implication that holds because its antecedent doesn't.  Of course, that $p\to q$ actually does hold when $p$ doesn't is a fact that can be proven in several ways, and which is appropriate depends on how you're defining the logic. Given your semantics-oriented terminology, you are presumably specifying the logic by giving it a semantics in terms of truth tables. Here the interpretation you've been given for $\to$ immediately says that $p\to q$ interprets as "true" when $p$ is interpreted as "false" regardless of the interpretation of $q$.
To reiterate, that $p\to q$ interprets as "true" when $p$ interprets as "false" is most likely true by definition of the interpretation of $\to$ you were given. That we call this particular situation "vacuous truth" is a different definition of some terminology, and the only reason we need to check anything is to verify that "truth" in "vacuous truth" is justified (otherwise this would be some very confusing terminology).
