Theorem empty-surprise2

Description: "Prove" that false is true when using a restricted "for all" over the empty set, to demonstrate that the expression is always true if the value ranges over the empty set.

Those inexperienced with formal notations of classical logic can be surprised with what restricted "for all" does over an empty set. We proved the general case in empty-surprise . Here we prove an extreme example: we "prove" that false is true. Of course, we actually do no such thing (see notfal ); the problem is that restricted "for all" works in ways that might seem counterintuitive to the inexperienced when given an empty set. Solutions to this can include requiring that the set not be empty or by using the allsome quantifier df-alsc . (Contributed by David A. Wheeler, 20-Oct-2018)

	Ref	Expression
Hypothesis	empty-surprise2.1	$$⊢\neg \exists xx\in A$$
Assertion	empty-surprise2	$$⊢\forall x\in A\perp$$

Proof

Step	Hyp	Ref	Expression
1		empty-surprise2.1	$$⊢\neg \exists xx\in A$$
2	1	empty-surprise	$$⊢\forall x\in A\perp$$