Still struggling to understand vacuous truths

I've never been satisfied with the definition of the material implication in the context of propositional logic alone. The only really important things in the context of propositional logic are that $T \Rightarrow T$ is true and $T \Rightarrow F$ is false. It feels like the truth values of $F \Rightarrow T$ and $F \Rightarrow F$ are just not specified by our intuition about implication. After all, why should "if the sky is green, then clouds are red" be true?

But in predicate logic, things are different. In predicate logic, we'd like to be able to say $\forall x (P(x) \Rightarrow Q(x))$ and have the $x$'s for which $P(x)$ is false not interfere with the truth of the statement.

For example, consider "among all integers, all multiples of $4$ are even". That statement is true even though $1$ is not even. It's also true even though $2$ is even despite not being a multiple of $4$.

But now in classical logic, every proposition has a single truth value. Thus the only way to define $\forall x R(x)$ is "for every $x$, $R(x)$ is true". We can't define it in some other way, like "for every $x$, either $R(x)$ is true or $R(x)$ is too nonsensical to have a truth value". Thus we are stuck defining $F \Rightarrow T$ and $F \Rightarrow F$ to both be true, if $\forall x (P(x) \Rightarrow Q(x))$ is going to behave the way we want.

In a different system of logic, we might do things differently. But in classical logic, "every proposition has a truth value" is basically an axiom.

Given that we want the $\rightarrow$ to capture the idea of an 'if .. then ..' statement, it seems reasonable to insist that $P \rightarrow P$ is a True statement, no matter what $P$ is, and thus no matter what truth-value $P$ has.

So, if $P$ is False, then we get $\boxed{F \rightarrow F = T}$

It is likewise reasonable to insist that $(P \land Q) \rightarrow P = T$, again no matter what $P$ and $Q$ are.

So, if $P$ is True, and $Q$ is False, we get: $(T \land F) \rightarrow T = \boxed{F \rightarrow T = T}$

Other times I see "Well it's just defined that way because it's useful"... with no examples of how it's indeed useful

OK, then let's give an example of a real-world use case. I'm a computer programmer by trade, but I also am concerned with the meta-problem of how we know when a program is correct. That is, I use static analysis to understand programs; "implies" as it is defined is extremely useful in this analysis.

Let's suppose I have a list of orders and a reference to a customer, and I happen to know that if the reference is valid, then the list contains at least one order:

if (customer != null)
{
  Assert(orders.Count() > 0);
  Print(orders.First());
}

"Assert" crashes the program if the condition is false.

Let us call a computer program which crashes an "F" program and one which runs without crashing a "T" program.

Now let's look at the truth table of this little program fragment.

cust != null  orders.Count() > 0  Program classification
-----------------------------------------------------
True          True                 T -- because the assertion succeeds
True          False                F -- because the assertion crashes
False         True                 T -- because the assertion never runs at all
False         False                T -- because the assertion never runs at all

Now suppose we had an implies operator in this language. We would want to be able to rewrite our program as

Assert(customer != null  implies  orders.Count() > 0);
if (customer != null)
{
  Print(orders.First());
}

without changing the categorization of the program. In order to maintain the meaning of the program, the truth table of binary operator A implies B must be the same as (NOT A) OR B.

That's why "implies" as defined is useful. It lets us reason accurately and concisely about the correctness of computer programs that contain conditional statements.

Now, you might argue that "implies" is the wrong word to use, because "implies" is imbued with some meaning that you think does not match this truth table. But that's a fact about your intuition; it doesn't change the fact that this operator is useful as defined for reasoning logically about the correctness of programs.