Motivation for natural deduction

Question

I've been learning natural deduction recently. I've seen many problems and am starting to be able to solve problems more easily.

For some reason I feel the need to ask what high school math students always ask about mathematics.

What is the point of natural deduction? I teach a problem class in a computer science module and I'm worried that when we come to these problems a student is going to ask me this.

For graph theory or number theory I can say something interesting, but what could I say that's at all interesting about natural deduction? Is there anything at all?

Answer 1

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).

Answer 2

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.

Answer 3

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.

Answer 4

In the context of computer science, natural deduction has a very important role to play. The structure of proofs in natural deduction can be read as simple functional programs with a reduction semantics given by the way the introduction and elimination rules for a certain connective fit together.

For example, consider a proof of (A ^ B) => (B ^ A). In natural deduction, this can be written

--------------x ---------------x A ^ B |- A ^ B A ^ B |- A ^ B -------------- ^E2 ----------------^E1 A ^ B |- B A ^ B |- A -------------------------------^I A ^ B |- B ^ A ---------------^I(x) |- A^B => B^A

A more concise way of writing this proof would would be (fun x = <#2 x, #1 x>). In other words, it's a function that takes a pair of values, and returns a pair of the second component followed by the first component.

In this interpretation of programs as proofs, the propositions proven true in natural deduction give a type system. By making sense of other logical connectives in terms of natural deduction, we get new type systems and sometimes new program constructs in the programming language.

This idea is frequently referred to as the Curry-Howard Correspondence, which forms the basis of a great deal of modern programming language research.

Answer 5

I know this is a late answer, but to me the most interesting thing about natural deduction is that the inference rules are so well-organized (every symbol has an introduction rule and and elimination rule) that they suggest the structure of your proof. If you have a symbol in the premises and not in the conclusion, that's a hint that you should probably structure your proof around that elimination rule. Similarly, if there's a symbol in the conclusion that's not in the premises, that's a hint that you might need to structure your proof around the corresponding introduction rule.

When you contrast natural deduction with, say, Copi's 19 Rules, you see that there is virtually no organization in Copi's Rules. The only way you could use their structure to help you out is to think about them just like how I said above. You could organize Copi's Rules yourself into rules that introduce symbols, and rules that eliminate symbols, and that would help somewhat.