Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  empty-surprise2 Structured version   Visualization version   GIF version

Theorem empty-surprise2 43053
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 43052. Here we prove an extreme example: we "prove" that false is true. Of course, we actually do no such thing (see notfal 1667); 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 43059. (Contributed by David A. Wheeler, 20-Oct-2018.)

Hypothesis
Ref Expression
empty-surprise2.1 ¬ ∃𝑥 𝑥𝐴
Assertion
Ref Expression
empty-surprise2 𝑥𝐴

Proof of Theorem empty-surprise2
StepHypRef Expression
1 empty-surprise2.1 . 2 ¬ ∃𝑥 𝑥𝐴
21empty-surprise 43052 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wfal 1636  wex 1852  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ex 1853  df-ral 3066
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator