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 A. x e. A ph is simply an abbreviation for A. x ( x e. A -> ph ) (per df-ral ). Thus, if A is the empty set, this expression isalways true regardless of the value of ph (see alimp-surprise ).
If you want the expression A. x e. A ph to not be vacuously true, you need to ensure that set A is inhabited (e.g., E. x e. A ). (Technical note: You can also assert that A =/= (/) ; this is an equivalent claim in classical logic as proven in n0 , but in intuitionistic logic the statement A =/= (/) is a weaker claim than E. x e. A .)
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 nonexistent entities in his logic." (Groarke, "Aristotle: Logic", section 7. (Existential Assumptions),Internet Encyclopedia of Philosophy, http://www.iep.utm.edu/aris-log/ ). While this made sense for his purposes, it is less flexible than modern (classical) logic whichdoes permit empty sets. If you wish to make claims that require a nonempty set, you must expressly include that requirement, e.g., by stating E. x ph . Examples of proofs that do this include barbari , celaront , and cesaro .
For another "surprise" for new users of classical logic, see alimp-surprise and eximp-surprise . (Contributed by David A. Wheeler, 20-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | empty-surprise.1 | ⊢ ¬ ∃ 𝑥 𝑥 ∈ 𝐴 | |
| Assertion | empty-surprise | ⊢ ∀ 𝑥 ∈ 𝐴 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | empty-surprise.1 | ⊢ ¬ ∃ 𝑥 𝑥 ∈ 𝐴 | |
| 2 | 1 | alimp-surprise | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝜑 ) ) |
| 3 | 2 | simpli | ⊢ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) |
| 4 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
| 5 | 3 4 | mpbir | ⊢ ∀ 𝑥 ∈ 𝐴 𝜑 |