Vacuous Truth

I briefly saw this in SE212. a vacuous truth is a conditional or universal statement that is true because the antecedent cannot be satisfied.

SE212: “Vacuously true” is a justification that can be used for a universally quantified implication when there are no values that can satisfy the antecedent of the implication.

Example

1. ∀i • 0 ≤ i ∧ i < n ⇒ B[i] = B0[i] premise
2. ∀i • 0 ≤ i ∧ i < 0 ⇒ B[i] = B0[i + 1] by arith /* vacuously true*/
3. (∀i • 0 ≤ i ∧ i < 0 ⇒ B[i] = B0[i + 1]) ∧ (∀i • 0 ≤ i ∧ i < n ⇒ B[i] = B0[i]) by and_i on 1,2