Theorem alimp-surprise

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., x e. M and M = (/) ).

This is perhaps best explained using an example. The sentence "All Martians are green" would typically be represented formally using the expression A. x ( ph -> ps ) . In this expression ph is true iff x is a Martian and ps is true iff x is green. Similarly, "All Martians are not green" would typically be represented as A. x ( ph -> -. ps ) . However, if there are no Martians ( -. E. x ph ), then both of those expressions aretrue. 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 ( ph -> ps ) is equivalent to -. ph \/ ps (as proven in imor ). When ph is always false, -. ph is always true, and anor with true is always true.

Here are a few technical notes. In this notation, ph and ps are predicates that return a true or false value and may depend on x . We only saymay because it actually doesn't matter for our proof. In Metamath this simply means that we do not require that ph , ps , and x be distinct (so x can be part of ph or ps ).

In natural language the term "implies" often presumes that the antecedentcan occur in at one least circumstanceand 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 ) or using the allsome quantifier ( df-alsi ) .

For other "surprises" for new users of classical logic, see empty-surprise and eximp-surprise . (Contributed by David A. Wheeler, 17-Oct-2018)

	Ref	Expression
Hypothesis	alimp-surprise.1	$$⊢\neg \exists x\phi$$
Assertion	alimp-surprise	$$⊢\left(\forall x\left(\phi \to \psi \right)\wedge \forall x\left(\phi \to \neg \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		alimp-surprise.1	$$⊢\neg \exists x\phi$$
2		imor	$$⊢\left(\phi \to \psi \right)\leftrightarrow \left(\neg \phi \vee \psi \right)$$
3	2	albii	$$⊢\forall x\left(\phi \to \psi \right)\leftrightarrow \forall x\left(\neg \phi \vee \psi \right)$$
4	1	nexr	$$⊢\neg \phi$$
5	4	orci	$$⊢\left(\neg \phi \vee \psi \right)$$
6	3 5	mpgbir	$$⊢\forall x\left(\phi \to \psi \right)$$
7		imor	$$⊢\left(\phi \to \neg \psi \right)\leftrightarrow \left(\neg \phi \vee \neg \psi \right)$$
8	7	albii	$$⊢\forall x\left(\phi \to \neg \psi \right)\leftrightarrow \forall x\left(\neg \phi \vee \neg \psi \right)$$
9	4	orci	$$⊢\left(\neg \phi \vee \neg \psi \right)$$
10	8 9	mpgbir	$$⊢\forall x\left(\phi \to \neg \psi \right)$$
11	6 10	pm3.2i	$$⊢\left(\forall x\left(\phi \to \psi \right)\wedge \forall x\left(\phi \to \neg \psi \right)\right)$$