Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > eximp-surprise2 | Structured version Visualization version GIF version |
Description: Show that "there
exists" with an implication is always true if there
exists a situation where the antecedent is false.
Those inexperienced with formal notations of classical logic may use expressions combining "there exists" with implication. This is usually a mistake, because that combination does not mean what an inexperienced person might think it means. For example, if there is some object that does not meet the precondition 𝜑, then the expression ∃𝑥(𝜑 → 𝜓) as a whole is always true, no matter what 𝜓 is (𝜓 could even be false, ⊥). New users of formal notation who use "there exists" with an implication should consider if they meant "and" instead of "implies". See eximp-surprise 44252, which shows what implication really expands to. See also empty-surprise 44250. (Contributed by David A. Wheeler, 18-Oct-2018.) |
Ref | Expression |
---|---|
eximp-surprise2.1 | ⊢ ∃𝑥 ¬ 𝜑 |
Ref | Expression |
---|---|
eximp-surprise2 | ⊢ ∃𝑥(𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximp-surprise2.1 | . . 3 ⊢ ∃𝑥 ¬ 𝜑 | |
2 | orc 853 | . . 3 ⊢ (¬ 𝜑 → (¬ 𝜑 ∨ 𝜓)) | |
3 | 1, 2 | eximii 1799 | . 2 ⊢ ∃𝑥(¬ 𝜑 ∨ 𝜓) |
4 | eximp-surprise 44252 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ ∃𝑥(¬ 𝜑 ∨ 𝜓)) | |
5 | 3, 4 | mpbir 223 | 1 ⊢ ∃𝑥(𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 833 ∃wex 1742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 |
This theorem depends on definitions: df-bi 199 df-or 834 df-ex 1743 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |