|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
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
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
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 842).
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.
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
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 43633) or using the allsome quantifier
(df-alsi 43640) .
For other "surprises" for new users of classical logic, see
empty-surprise 43634 and eximp-surprise 43636. (Contributed by David A.