The most likely reason one would use natural deduction in a proof is because it parallels the way people think. When trying to prove some complicated implication chain like $$(A\to(B\to C))\to((A\to B)\to(A\to C)),$$ most people find it more logical and reasonable to assume the left part and deduce the right part rather than working with axioms that deal with implication directly, even though the approaches can be shown to be equivalent. For the above tautology, it is less enlightening to make a truth table and show that it's true under all assignments than simply to reason in a deductive way:

Suppose $A\to(B\to C)$, $A\to B$, and $A$ are known. (I want to show $C$.) Since $A$ is true and $A$ implies $B$, we know $B$ is true, and since $A$ implies $B\to C$, that is true as well. But then $B$ and $B\to C$ are true, so $C$ is also true.

This approach scales much better than a truth table approach, and is easier to follow, so it has actually informed me in my own work in creating a system for emulating natural deduction proofs in Metamath, which is based on an axiomatic approach to manipulating implications.


Natural deduction has played a role in automated theorem proving.

Also, setting up natural deductive derivations and then converting those derivations to axiomatic proofs can give you a list of formulas that might work well as resonators when using an automated theorem prover which might help you find a shorter axiomatic proof. Or even make it easier to find a first automated proof. For instance, I recently hand-wrote a natural deductive derivation and turned it into a 94 step axiomatic proof, where each step indicates a use of condensed detachment to generate a theorem which is not an axiom. Then using those steps as resonators, shorter proofs of the same theorem in the same system got found (and someone got the proof down to even fewer steps, probably using some other techniques). Or those natural deduction derivations, if converted to axiomatic proofs, can help find theorems in say weaker theories, such as Lukasiewicz 3-valued logic or intuitionistic logic or relevant logic using Bob Veroff's method of proof sketches (search "proof sketches" in the link).


Shortly, natural deduction is a proof calculus that models the natural way people conduct their deductive reasoning - it is a Kalkül des natürlichen Schließens (Gentzen, 1943).

Natural deduction opposes the early "artificial" treatment of logic found in Frege, Russell & Whitehead or Hilbert by means of the axiomatization of the logical thinking. Proofs in those so called "Hilbert-style" systems can be very troublesome, as I put elsewhere:

[Axiomatic] proofs tend to be much more puzzling and laborious then Gentzen-style ones. Presumably, a natural deduction experienced logician would have troubles to prove the same theorem he just proved in the latter system using the former (For instance, note that the shortest known proof in Mendelson's system $M$ of the (trivial?) '$A \wedge B \vdash A$' requires $-$ as far as I know $-$ over 50 lines! [§2.3]).

You can then have a check there how an axiomatic proof of $¬A→B⊢¬B→A$ proceeds, and compare it providing a natural deduction counterpart proof of it.