![]() |
Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > empty-surprise2 | Structured version Visualization version GIF version |
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 48795. Here we prove an extreme example: we "prove" that false is true. Of course, we actually do no such thing (see notfal 1565); 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 48802. (Contributed by David A. Wheeler, 20-Oct-2018.) |
Ref | Expression |
---|---|
empty-surprise2.1 | ⊢ ¬ ∃𝑥 𝑥 ∈ 𝐴 |
Ref | Expression |
---|---|
empty-surprise2 | ⊢ ∀𝑥 ∈ 𝐴 ⊥ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | empty-surprise2.1 | . 2 ⊢ ¬ ∃𝑥 𝑥 ∈ 𝐴 | |
2 | 1 | empty-surprise 48795 | 1 ⊢ ∀𝑥 ∈ 𝐴 ⊥ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ⊥wfal 1549 ∃wex 1777 ∈ wcel 2103 ∀wral 3063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-12 2173 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-ex 1778 df-ral 3064 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |