反证法
theorem proof_by_contrad (A: wff): $ (\neg A \imp \false) \imp A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | ((\neg A \imp \false) \imp \neg \neg A) \imp (\neg \neg A \imp A) \imp (\neg A \imp \false) \imp A |
|
| 2 | iff_decomp | (\neg A \imp \false \iff \neg \neg A) \imp (\neg A \imp \false) \imp \neg \neg A |
|
| 3 | impfalse_eqv_negself | \neg A \imp \false \iff \neg \neg A |
|
| 4 | 2, 3 | ax_mp | (\neg A \imp \false) \imp \neg \neg A |
| 5 | 1, 4 | ax_mp | (\neg \neg A \imp A) \imp (\neg A \imp \false) \imp A |
| 6 | negneg_elim | \neg \neg A \imp A |
|
| 7 | 5, 6 | ax_mp | (\neg A \imp \false) \imp A |