Why is forall true on an empty list?

This is a specific instance of a vacuous truth. The example given on Wikipedia is that the statement "all cellphones in the room are turned off" is vacuously true if there is no cellphone in the room. Interestingly, the statement "all cellphones in the room are turned on" is vacuously true, as is the statement "all cellphones in the room are turned off and turned on".

The basic intuition is that every element which is there satisfies the predicate.

To add to the previous answers and comments: this is more consistent and leads to fewer surprises down the road.

For example, to check if a predicate holds for all elements of a big collection, you could employ a divide-and-conquer strategy: split the collection into smaller parts, run forall on each sub-collection, and combine the results with &&:

List(1, 2, 3, 4).forall(_ > 0)
// is equivalent to:
List(1, 2).forall(_ > 0) && List(3, 4).forall(_ > 0)

Now you could imagine "splitting" a collection into a collection containing exactly the same elements, and an empty one:

List(1, 2).forall(_ > 0)
// should be equivalent to:
List(1, 2).forall(_ > 0) && List[Int]().forall(_ > 0)

You wouldn't like the result of running forall on an empty collection to change the overall result, so it's convenient to treat it as true.

Logic dictates that an implication can only be false if the antecedent is satisfied, but the consequent isn't. That is, P => Q (P implies Q, or "if P then Q") is false only if P but !Q. In any other cases, even in the case where P is false, P => Q is true.

And forall relies on an implication (i.e "if x satisfies P, include x in the resulting set"). If forall is applied to an empty set/list, no x will satisfy P

This answer derives the fact from basically just two things:

• empty set is subset of the empty set
• definition of implication

Unlike all those handwavy excluded-middle-answers in the linked MathOverflow answers, it doesn't even use negation anywhere.

Since list.forall(p) should behave the same as list.toSet.forall(p), I'll speak only about sets.

Assuming that you accept the definition of "for all" in some more basic terms, you can prove that Set.empty[A].forall(p) must be true, regardless of what the condition p is.

One way to express such fundamental notions as "for all" in terms of something even more basic is given in the last paragraph of this section on Lawvere Quantifiers.

If one boils down the definition, it basically says:

• Given a set X

• and a predicate p: X -> Boolean

• consider the subset S = { s in X | p(s) = true } defined by the predicate

• and the preimage of the constant true-function:

  tPreimg(b: Boolean) = if b then X else emptySet
  

then forall is defined by the property

tPreimg(b) subset S  <=>  b implies X.forall(p)

Now, if one takes X as the empty set, then

• tPreimg(b) is always the empty set, regardless of the boolean value b
• S, as a subset of empty X, must also be the empty set
• Left hand side becomes emptySet subset emptySet, which is always true, because every set must be subset of itself.
• Thus, the right hand side must also be always true, regardless of the choice of Boolean b
• Thus, X.forall(p) must be true, because otherwise the right hand side would be false for b = true.

Hence, we obtain that for empty X, X.forall(p) must be true, regardless of how the predicate p is expressed.