Theorem contradiction_tf ≪ | index | src | ≫

矛盾律tf形式

theorem contradiction_tf (A: wff):
  $ \neg ((A \iff \true) \and (A \iff \false)) $;
StepHypRefExpression
1 negneg_intro 
((A \iff \true) \imp \neg (A \iff \false)) \imp \neg \neg ((A \iff \true) \imp \neg (A \iff \false))
2 imp_tran 
((A \iff \true) \imp A) \imp (A \imp \neg (A \iff \false)) \imp (A \iff \true) \imp \neg (A \iff \false)
3 iff_decompbwd 
(A \iff A \iff \true) \imp (A \iff \true) \imp A
4 assgin_true 
A \iff A \iff \true
5 3, 4 ax_mp 
(A \iff \true) \imp A
6 2, 5 ax_mp 
(A \imp \neg (A \iff \false)) \imp (A \iff \true) \imp \neg (A \iff \false)
7 imp_neg_swap 
((A \iff \false) \imp \neg A) \imp A \imp \neg (A \iff \false)
8 iff_decompbwd 
(\neg A \iff A \iff \false) \imp (A \iff \false) \imp \neg A
9 assign_false 
\neg A \iff A \iff \false
10 8, 9 ax_mp 
(A \iff \false) \imp \neg A
11 7, 10 ax_mp 
A \imp \neg (A \iff \false)
12 6, 11 ax_mp 
(A \iff \true) \imp \neg (A \iff \false)
13 1, 12 ax_mp 
\neg \neg ((A \iff \true) \imp \neg (A \iff \false))
14 13 conv and 
\neg ((A \iff \true) \and (A \iff \false))

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)