A deficiency of natural deduction (Q1104317)

In the article two examples are given, illustrating how Gentzen's system of natural deduction in the present form is not suited to express an effective mathematical reasoning, because natural deduction may lead to rather ineffective proofs. This defect of Gentzen's system consists in the fact that this system does not handle equivalence efficiently. The equivalence \(A\Leftrightarrow B\) in this system can only be expressed by (A\(\Rightarrow B)\wedge (B\Rightarrow A)\) or by (A\(\wedge B)\vee (\neg A\wedge \neg B)\) and therefore the formulae are twice as long as desirable. In the case of more than one equivalence this leads to exponential growth of the formulae. Gentzen states that one of the advantages of his deduction system is ``The close affinity to actual reasoning.... Hence the calculus leads itself in particular to formalisation of mathematical proofs''. The author's point of view is ``Since natural languages are ill-suited to express mathematical reasoning, such an affinity to actual reasoning in a natural language is rather a disadvantage of a formal deduction system''.