Mathbox for David A. Wheeler < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  alimp-surprise Structured version   Visualization version   GIF version

Theorem alimp-surprise 42335
 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 427). 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 42336) or using the allsome quantifier (df-alsi 42343) . For other "surprises" for new users of classical logic, see empty-surprise 42337 and eximp-surprise 42339. (Contributed by David A. Wheeler, 17-Oct-2018.)
Hypothesis
Ref Expression
alimp-surprise.1 ¬ ∃𝑥𝜑
Assertion
Ref Expression
alimp-surprise (∀𝑥(𝜑𝜓) ∧ ∀𝑥(𝜑 → ¬ 𝜓))

Proof of Theorem alimp-surprise
StepHypRef Expression
1 imor 427 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21albii 1737 . . 3 (∀𝑥(𝜑𝜓) ↔ ∀𝑥𝜑𝜓))
3 alimp-surprise.1 . . . . 5 ¬ ∃𝑥𝜑
43nexr 2050 . . . 4 ¬ 𝜑
54orci 404 . . 3 𝜑𝜓)
62, 5mpgbir 1717 . 2 𝑥(𝜑𝜓)
7 imor 427 . . . 4 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
87albii 1737 . . 3 (∀𝑥(𝜑 → ¬ 𝜓) ↔ ∀𝑥𝜑 ∨ ¬ 𝜓))
94orci 404 . . 3 𝜑 ∨ ¬ 𝜓)
108, 9mpgbir 1717 . 2 𝑥(𝜑 → ¬ 𝜓)
116, 10pm3.2i 470 1 (∀𝑥(𝜑𝜓) ∧ ∀𝑥(𝜑 → ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696 This theorem is referenced by:  empty-surprise  42337
 Copyright terms: Public domain W3C validator