Description: Demonstrate that when
using "for all" and material implication the
consequent can be both always true and always false if there is no case
where the antecedent is true.
Those inexperienced with formal notations of classical logic can be
surprised with what "for all" and material implication do
together when
the implication's antecedent is never true. This can happen, for
example, when the antecedent is set membership but the set is the empty
set (e.g., and ).
This is perhaps best explained using an example. The sentence "All
Martians are green" would typically be represented formally using
the
expression . In this
expression is
true
iff is a
Martian and is
true iff is green.
Similarly, "All Martians are not green" would typically be
represented
as
. However, if there are no Martians
( ), then both of those expressions are true. That
is
surprising to the inexperienced, because the two expressions seem to be
the opposite of each other. The reason this occurs is because in
classical logic the implication
is equivalent to
(as proven in imor 428). When is always false,
is always true, and
an or with true is always true.
Here are a few technical notes. In this notation, and are
predicates that return a true or false value and may depend on .
We only say may because it actually doesn't matter for our proof.
In
metamath this simply means that we do not require that , ,
and be distinct
(so can be part of
or ).
In natural language the term "implies" often presumes that the
antecedent can occur in at one least circumstance and that
there is
some sort of causality. However, exactly what causality means is
complex and situation-dependent. Modern logic typically uses material
implication instead; this has a rigorous definition, but it is important
for new users of formal notation to precisely understand it. There are
ways to solve this, e.g., expressly stating that the antecedent exists
(see alimp-no-surprise 42527) or using the allsome quantifier
(df-alsi 42534) .
For other "surprises" for new users of classical logic, see
empty-surprise 42528 and eximp-surprise 42530. (Contributed by David A.
Wheeler, 17-Oct-2018.) |