Մաթ. Տրամ./Բանաձևերի արտածումները/2

$A\supset \mathrm{\neg }\mathrm{\neg }A$

$A⊢\mathrm{\neg }\mathrm{\neg }A$

$1.A⊢\left(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\supset A\right)\supset \left(\left(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\supset \mathrm{\neg }A\right)\supset \mathrm{\neg }\mathrm{\neg }A\right)$	// աքսիոմ 3 ($A=\mathrm{\neg }\mathrm{\neg }A,B=A$)
$2.A⊢A$	// նախադրյալ
$3.A⊢A\supset \left(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\supset A\right)$	// աքսիոմ 1 ($A=A,B=\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A$)
$4.A⊢\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\supset A$	// m.p. (2,3)
$5.A⊢\left(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\supset \mathrm{\neg }A\right)\supset \mathrm{\neg }\mathrm{\neg }A$	// m.p. (4,1)
$6.A⊢\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\supset \mathrm{\neg }A$	// բանաձև 1 ($A=\mathrm{\neg }A$)
$7.A⊢\mathrm{\neg }\mathrm{\neg }A$	// m.p. (6,5)
$8.A⊢A\supset \mathrm{\neg }\mathrm{\neg }A$	// դեդուկցիայի թեորեմը