20 - Contradictory Cases

When we explored proof by cases, each case led to the proof objective. 

In general, not all cases permitted by a hypothesis will lead to the proof objective. Some cases may lead to a contradiction, meaning they are ruled out as possible cases.

Task

If P is a proposition, show that

$$\mathrm{\neg }(\mathrm{\neg }P)⟹P$$

We may be tempted to cancel the two negations on the left. For this task we'll pretend we don't yet know this is a valid simplification. 

We haven't specified what proposition $P$ is. That means our theorem, if we can prove it, will hold for any proposition. 

So proving $\mathrm{\neg }(\mathrm{\neg }P)⟹P$ will justify our intuition that two negations do indeed cancel out.

Maths

A fundamental idea is that a proposition is either true or false, and there is no other possibility. This is called the Law of the Excluded Middle.

It means there are only two possibilities for our proposition $P$. It is either true, or it is false. 

Let's consider each case.

• P is true. This is the proof objective, so there is nothing more to do.
• P is false. That is, $\mathrm{\neg }P$ is true. This contradicts the given hypothesis that $\mathrm{\neg }(\mathrm{\neg }P)$ is true. A contradiction arises from an invalid assumption, so it can't be the case that $P$ is false. 

To summarise, we've shown that $P$ true is possible, but $P$ false is not.

A couple of points about our reasoning are worth explaining. 

First, two statements of the form $Q$ and $\mathrm{\neg }Q$ are contradictory. This is how, in the second case, we justify $\mathrm{\neg }P$ and $\mathrm{\neg }(\mathrm{\neg }P)$ are contradictory.

Second, it may look like a circular argument that the first case assumes $P$ is true to prove $P$ is true. It isn't circular because we consider all the possibilities for $P$, which here means considering $P$ is false. It just so happens we then rule out this possibility. 

Let's try to write this in small steps as preparation for a Lean proof.

$$\begin{array}{rlrl}\mathrm{\neg }(\mathrm{\neg }P)& ⟹P& & \text{proof objective}\\ & & & \\ \text{(1)}& & \mathrm{\neg }(\mathrm{\neg }P)& & \text{hypothesis}\text{(2)}& & P& & \text{proof goal}& & & \\ \text{(3)}& P& \vee \mathrm{\neg }P& & \text{law of excluded middle}& & & \\ \text{case }P& & & \text{using fact }(\text{3})\\ & P& & \text{proof goal}\\ & & & \\ \text{case }\mathrm{\neg }P& & & \text{using fact }(\text{3})\\ & \mathrm{\neg }P& & \text{contradicts hypothesis }(\text{1})\\ & & & \\ ◻& \mathrm{\neg }(\mathrm{\neg }P)& ⟹P& & \text{only consistent case}\end{array}$$

We've not proved an implication before so let's clarify how it's done. To prove an implication $A⟹B$, we assume $A$ as a hypothesis and then prove $B$. 

So to prove $\mathrm{\neg }(\mathrm{\neg }P)⟹P$, we take $\mathrm{\neg }(\mathrm{\neg }P)$ as a hypothesis (1) and set $P$ as a proof goal (2).

The rest is a proof by cases, and proceeds just as we discussed above.

Code

The following Lean program proves $\mathrm{\neg }(\mathrm{\neg }P)⟹P$, where $P$ is a proposition.

-- 20 - Contradictory Cases

import Mathlib.Tactic

example {P : Prop} : ¬(¬P) → P := by
  intro g
  by_cases h : P
  · exact h
  · contradiction

The proof header declares P as a proposition using {P : Prop}. 

The proof starts with intro g which converts the proof objective, the implication ¬(¬P) → P, into a hypothesis g : ¬¬P and a new goal P. 

Next, by_cases h : P creates the two cases for P using the Law of the Excluded Middle. Just like a proof by cases, Lean will replace the current goal with two new separate goals, one with h : P as a hypothesis, the other with h : ¬P as a hypothesis.

The rest of the proof handles each case, using focussing dots to organise the sub-proofs.

• The first case is h : P. This exactly matches the goal P, so we can use exact h to resolve this case.
• The second case is h : ¬P. This directly contradicts the hypothesis g : ¬¬P created at the start of the proof, so we can use contradiction to resolve this case. That means ¬P is ruled out as a possibility.

Infoview

Placing the cursor before intro g shows the original proof goal.

⊢ ¬¬P → P

Moving the cursor to the start of the next line shows ¬¬P established as a new hypothesis g, and P set as the new goal.

g : ¬¬P
⊢ P

Placing the curser after by_cases h : P shows the two new goals, one for each case.

case pos
P : Prop
g : ¬¬P
h : P
⊢ P

case neg
P : Prop
g : ¬¬P
h : ¬P
⊢ P

---

Exercise

If $P$ is a proposition, write a Lean program to show that

$$P⟹\mathrm{\neg }(\mathrm{\neg }P)$$

To keep the proof as short as the example above, try applying the law of the excluded middle, not to $P$, but to $(\mathrm{\neg }P)$.