06 — Negation and Contradiction

The Mathematics

Negation is where logic gets its teeth. The proposition ¬P (read "not P") means "P is false." But what does that actually mean in formal logic?

Here's the key insight: in Lean 4, ¬P is defined as P → False. That's it. "P is false" literally means "if P were true, we could derive a contradiction." It's an implication to the impossible.

False is a proposition with no proof. Nothing can prove False — that's what makes it false. But if you ever do get a proof of False, you can prove anything (this is the principle of explosion, or ex falso quodlibet).

The key tactics for working with negation:

intro h — since ¬P is really P → False, you can intro to assume P and then try to derive False
contradiction — closes a goal when your hypotheses contain an obvious contradiction (like hp : P and hnp : ¬P)
absurd hp hnp — given hp : P and hnp : ¬P, produces a proof of anything
exact hnp hp — since hnp : ¬P is really hnp : P → False, you can just apply it to hp : P to get False

That last point is worth sitting with. Because ¬P is a function from P to False, you can literally call it on a proof of P. Negation is just function application.

The Lean Proof

Let's see negation in action. Here's a proof that P and ¬P can't both be true:

theorem not_and_self (P : Prop) (hp : P) (hnp : ¬P) : False := by
  exact hnp hp

Since hnp is really a function P → False, we just feed it hp. Out comes False.

We could also write this with contradiction:

theorem not_and_self' (P : Prop) (hp : P) (hnp : ¬P) : False := by
  contradiction

The contradiction tactic spots that hp and hnp are contradictory and closes the goal automatically. It's convenient, but understanding the function-application version gives you deeper insight.

Your Turn

Prove double negation introduction: if P is true, then ¬¬P (it's not the case that P is false). Remember, ¬¬P unfolds to (P → False) → False. So you need to assume P → False and derive False.

theorem not_not_intro (P : Prop) (hp : P) : ¬¬P := by
  sorry

You already have hp : P. If someone gives you a function that turns P into False... well, you have a P right there.

Hint

The goal ¬¬P is really (P → False) → False. So start with intro hnp to assume hnp : ¬P (i.e., hnp : P → False).

Now your goal is False, and you have hp : P and hnp : P → False. Apply the function to the argument.

Solution

theorem not_not_intro (P : Prop) (hp : P) : ¬¬P := by
  intro hnp
  exact hnp hp

We assume hnp : P → False and then apply it to hp : P to get False. The negation is a function, so we just call it. That's the whole proof.

Bonus: Contraposition

Here's a classic pattern: if P implies Q, and Q is false, then P must be false too. This is contraposition — one of the most useful proof techniques in all of mathematics.

theorem contra (P Q : Prop) (hpq : P → Q) (hnq : ¬Q) : ¬P := by
  sorry

Think about it as a chain: if P were true, then Q would be true (by hpq), but Q is false (by hnq). Contradiction. So P can't be true.

Bonus Hint

The goal ¬P is P → False. So intro hp to assume hp : P.

Now chain: apply hpq to hp to get a proof of Q. Then apply hnq to that proof of Q to get False.

You can do this in one step: exact hnq (hpq hp).

Bonus Solution

theorem contra (P Q : Prop) (hpq : P → Q) (hnq : ¬Q) : ¬P := by
  intro hp
  exact hnq (hpq hp)

We assume P, use hpq to get Q, and then use hnq (which is Q → False) to reach False. It's function composition: hnq ˆ hpq is a function from P to False, which is exactly ¬P. Elegant.

← If and only if Natural Numbers track →