PROOF 26
Prove.
Proof by contradiction is justified
In propositional logic.
A way to read this proof
First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.
Definition D1
A contradiction is a statement of the form q ∧ ¬q. It is written ⊥.
Proof.
It means that some statement and its negation hold together.convention
∎
Definition D2
¬p means that p does not hold.
Proof.
Negation flips whether a statement holds. Which of p and ¬p holds is not settled by this definition.convention
∎
Lemma L1
⊥ does not hold.
Proof.
(1)⊥ is q ∧ ¬q.D1
(2)¬(q ∧ ¬q)A2
(3)Therefore ⊥ does not hold.(1), (2), D2
∎
Lemma L2
If p → ⊥, then ¬p.
Proof.
(1)Suppose p holds.assumption
(2)p → ⊥, so ⊥ holds.(1), assumption, A4
(3)⊥ does not hold.L1
(4)Therefore p does not hold.(2), (3)
(5)That is, ¬p.(4), D2
∎
Theorem T
If assuming ¬p yields a contradiction, then p holds.
Proof.
(1)Suppose ¬p → ⊥.assumption
(2)Applying L2 to ¬p yields ¬¬p.(1), L2
(3)¬¬p means that ¬p does not hold.(2), D2
(4)p ∨ ¬pA1
(5)Of the two disjuncts, ¬p does not hold, so p.(3), (4), A3
∎
Remark
Can A1 be removed from this proof?
The law of excluded middle is not proved; it is a rule accepted by agreement. Check which lines lose their justification when it is removed.