11
$\begingroup$

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?

$\endgroup$
2
7
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ By the way, the propositional calculus in Metamath is also based on system $M$. You can see the proof of the two quoted theorems at simpl and con1 (or, if you prefer actual deductions over implication equivalents, simpli and con1i). $\endgroup$ – Mario Carneiro Nov 20 '14 at 6:29
  • $\begingroup$ Also, the quote about 50 lines is misleading, because that is a direct-from-axioms proof, which no intelligent mathematician would ever do. Would you reprove the prime number theorem twice if you are going to use it twice in the proof? For some reason this kind of comparison is popular even though it would suggest that you can't get anything practical done without trillions of steps. (I hope to convince people that formal proof at the lowest level is not only possible but practical using Metamath as a case in point.) $\endgroup$ – Mario Carneiro Nov 20 '14 at 6:42
  • $\begingroup$ @MarioCarneiro Though the Mendelsohn system does have the same consequences as of the Metamath system, the axiom with negation symbols for Mendelsohn is CCNpNqCCNpqp, and for the Metamath/Lukasiewicz system is CCNpNqCqp. If we're really going to compare natural deduction derivations and axiomatic proofs, we'll want to point out that we can't make substitutions in formulas in natural deduction derivations, though you can make substitutions in formulas in axiomatic proofs. Also, axiomatic proofs prove many theorems at once. Natural deduction derivations only prove only theorem at a time. $\endgroup$ – Doug Spoonwood Nov 20 '14 at 7:11
  • $\begingroup$ @Doug (For my own and other's future reference, I believe you say $M$ uses the axiom $(\neg p\to\neg q)\to((\neg p\to q)\to p)$, while Metamath uses $(\neg p\to\neg q)\to(q\to p)$, after translating out of RPN notation.) I guess you are right about that third axiom, although the first two "implicational calculus" axioms are the same. Regarding substitutions, I would say that that is independent of the "natural deduction" aspect of a proof system, but every natural deduction-based system I have seen does allow substitution in formulas, ... $\endgroup$ – Mario Carneiro Nov 21 '14 at 2:09
  • $\begingroup$ ...although some use a derived rule to do it (i.e. wrapping a theorem in a universal quantifier, then instantiating it with a certain term). Logic textbooks often leave out a substitution axiom because it is provably conservative, but at the cost of an exponential blowup in proof length (because you can't reuse theorems). In any case, you can have a substitution axiom in either a natural deduction system or a hilbert system - the two aspects are not related very closely. $\endgroup$ – Mario Carneiro Nov 21 '14 at 2:12
3
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ Your example of (fun x = <#2 x, #1 x>)--what system is that in? Coq? An ML? I take it that #n x is just accessing the nth element of a tuple? So this is equivalent to, e.g., the Haskell (fst x)? $\endgroup$ – Shon Nov 20 '14 at 18:50
  • 1
    $\begingroup$ @ShonFeder For what it's worth, in Coq one way of writing this proof would be fun H : A /\ B => let '(conj HA HB) := H in conj HB HA. Compare to the function fun p : X * Y => let '(x, y) := p in (y, x) which defines an element of X * Y -> Y * X for types X and Y. $\endgroup$ – Daniel Schepler Apr 12 '17 at 22:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.