البرهان غير المباشر و مشكلة التفاف البراهين و معياريتها في الاستنباط الطبيعي للمنطق الكلاسيكي

الملخص EN

The problem of the detour of proofs in natural deduction systems is a serious problem.

We can not find a counterpart for this problem in axiomatic systems.

It means, roughly speaking, repetition to the lines or steps of proof.

This is a fault from a derivative point of view.

G.

Gentzen, the first logician to put a calculus for natural deduction, knew this problem very well, he even could solve it in respect to intuitive natural deductions systems but not to classical ones.

He solved that problem by his Haupstaz or Normalization theorem for intuitive proofs, i.

e.

proving the possibility of eliminating the detours in proofs.

It was Dag Prawitz who put the first proof of the normalization of proofs in natural deduction for classical systems by indirect proof rule.

In this paper, I shall scrutinize the ability of that rule of doing what wanted from it and if there is an alternative one for it.

]