Theorem eximp-surprise2

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 ph , then the expression E. x ( ph -> ps ) as a whole is always true, no matter what ps is ( ps could even be false, F. ). New users of formal notation who use "there exists" with an implication should consider if they meant "and" instead of "implies". See eximp-surprise , which shows what implication really expands to. See also empty-surprise . (Contributed by David A. Wheeler, 18-Oct-2018)

	Ref	Expression
Hypothesis	eximp-surprise2.1	$$⊢\exists x\neg \phi$$
Assertion	eximp-surprise2	$$⊢\exists x\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eximp-surprise2.1	$$⊢\exists x\neg \phi$$
2		orc	$$⊢\neg \phi \to \left(\neg \phi \vee \psi \right)$$
3	1 2	eximii	$$⊢\exists x\left(\neg \phi \vee \psi \right)$$
4		eximp-surprise	$$⊢\exists x\left(\phi \to \psi \right)\leftrightarrow \exists x\left(\neg \phi \vee \psi \right)$$
5	3 4	mpbir	$$⊢\exists x\left(\phi \to \psi \right)$$