| 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 3077). Thus, if 𝐴 is the empty
set, this expression is always true regardless of the value of
𝜑
(see alimp-surprise 50401).
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 4305, 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
nonexistent entities in his logic." (Groarke, "Aristotle:
Logic",
section 7. (Existential Assumptions), Internet Encyclopedia of
Philosophy, http://www.iep.utm.edu/aris-log/ 4305). 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 2695, celaront 2697, and cesaro 2704.
For another "surprise" for new users of classical logic, see
alimp-surprise 50401 and eximp-surprise 50405. (Contributed by David A.
Wheeler, 20-Oct-2018.) |
