В Гильб. исчислени высказываний есть аксиома о снятии дв. отрицания - фактически эквивалентная "доказательству от противного".
Это уже похоже на фричество. Ну докажите, что они фактически эквивалентны.
Дальше я привёл доказательство, которое IMO наиболее релевантно вашему вопросу.
Возьмём гильбертовскую систему из Википедии. C помощью естественного вывода выводим


(могу подробнее, но это надо рисовать диаграммы). Согласно теореме о дедукции, естественный вывод транслируется в

. Таким образом, вывод не использует

(исключение третьего), которая эквивалентна снятию двойного отрицания.