What ¬P really means
A negation is a function into False. Apply it like one.
In this course 3 / 11
¬P, typed \not, is notation for P → False, and False is the proposition with no proofs at all. So a proof of ¬P is a function that would turn a proof of P into a proof of False. Since nothing proves False, holding such a function is exactly the claim that nothing proves P either.
That definition is what makes negation usable. hnp : ¬P and hp : P are a function and an argument, so hnp hp is an ordinary application and its type is False. Negation needs no special tactics.
Being an implication, it also works backwards. With the goal ⊢ False and hnp : ¬P in context, apply hnp leaves ⊢ P. And to prove a negation ¬P, you intro its premise like any implication and then aim at False.
A goal of False looks alarming and is routine. It means: show these assumptions cannot all hold at once. Whenever the context contains both hp : P and hnp : ¬P, you are one application away from closing it.
Worked example
example (A B : Prop) (hna : ¬A) (hba : B → A) (hb : B) : False := by
apply hna
apply hba
exact hbRead the goal after each line: ⊢ False, then ⊢ A, then ⊢ B. The first apply works because ¬A is the implication A → False. Your exercise is the shortest version of this chain, with the proof already in hand.
¬P unfolds to P → False. Apply a negation to a proof of P to get False, forwards or backwards, and prove one with intro.
- 5. Contrapositive Easy
- 29. No witness means never Medium
- 33. Cantor’s diagonal argument Medium
Derive False from hp and hnp.
Suggested steps
- Apply the negation to the proof of P
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct