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

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

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

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