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

Theorem empty-surprise 42337
Description: Demonstrate that when using restricted "for all" over a class the expression can be both always true and always false if the class is empty.

Those inexperienced with formal notations of classical logic can be surprised with what restricted "for all" does over an empty set. It is important to note that 𝑥𝐴𝜑 is simply an abbreviation for 𝑥(𝑥𝐴𝜑) (per df-ral 2901). Thus, if 𝐴 is the empty set, this expression is always true regardless of the value of 𝜑 (see alimp-surprise 42335).

If you want the expression 𝑥𝐴𝜑 to not be vacuously true, you need to ensure that set 𝐴 is inhabited (e.g., 𝑥𝐴). (Technical note: You can also assert that 𝐴 ≠ ∅; this is an equivalent claim in classical logic as proven in n0 3890, but in intuitionistic logic the statement 𝐴 ≠ ∅ is a weaker claim than 𝑥𝐴.)

Some materials on logic (particularly those that discuss "syllogisms") are based on the much older work by Aristotle, but Aristotle expressly excluded empty sets from his system. Aristotle had a specific goal; he was trying to develop a "companion-logic" for science. He relegates fictions like fairy godmothers and mermaids and unicorns to the realms of poetry and literature... This is why he leaves no room for such non-existent entities in his logic." (Groarke, "Aristotle: Logic", section 7. (Existential Assumptions), Internet Encyclopedia of Philosophy, While this made sense for his purposes, it is less flexible than modern (classical) logic which does permit empty sets. If you wish to make claims that require a nonempty set, you must expressly include that requirement, e.g., by stating 𝑥𝜑. Examples of proofs that do this include barbari 2555, celaront 2556, and cesaro 2561.

For another "surprise" for new users of classical logic, see alimp-surprise 42335 and eximp-surprise 42339. (Contributed by David A. Wheeler, 20-Oct-2018.)

Ref Expression
empty-surprise.1 ¬ ∃𝑥 𝑥𝐴
Ref Expression
empty-surprise 𝑥𝐴 𝜑

Proof of Theorem empty-surprise
StepHypRef Expression
1 empty-surprise.1 . . . 4 ¬ ∃𝑥 𝑥𝐴
21alimp-surprise 42335 . . 3 (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
32simpli 473 . 2 𝑥(𝑥𝐴𝜑)
4 df-ral 2901 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
53, 4mpbir 220 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1473  wex 1695  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-ral 2901
This theorem is referenced by:  empty-surprise2  42338
  Copyright terms: Public domain W3C validator