排中律tf形式
theorem excluded_middle_tf (A: wff): $ (A \iff \true) \or (A \iff \false) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (\neg (A \iff \true) \imp \neg A) \imp (\neg A \imp (A \iff \false)) \imp \neg (A \iff \true) \imp (A \iff \false) |
|
| 2 | imp_introrev_neg | (A \imp (A \iff \true)) \imp \neg (A \iff \true) \imp \neg A |
|
| 3 | prov_iff_true | A \imp (A \iff \true) |
|
| 4 | 2, 3 | ax_mp | \neg (A \iff \true) \imp \neg A |
| 5 | 1, 4 | ax_mp | (\neg A \imp (A \iff \false)) \imp \neg (A \iff \true) \imp (A \iff \false) |
| 6 | provneg_iff_false | \neg A \imp (A \iff \false) |
|
| 7 | 5, 6 | ax_mp | \neg (A \iff \true) \imp (A \iff \false) |
| 8 | 7 | conv or | (A \iff \true) \or (A \iff \false) |