The name is suggestive. One of the popular ways of cashing out natural deduction is that it is an application of the laws (rules, whatever) of logic to our "natural modes" of inference.

For instance, if I say that

- all men are mortal, and I say that
- Sammy is not mortal, then one naturally infers that
- Sammy must not be a man.

Now, an axiomatic system **could** handle such an inference (since it's valid, and all such deductions are captured by non-wimpy axiomatic systems), but this would require a proof adhering to very restrictive syntactical (typographical, if one likes) rules. The advantage of a natural deduction system is that it has an apparatus for dealing with the sort of assumptions we just made. That is, one can assume whatever s/he likes, and proceed to deduce whatever can be deduced given the rules of the system. The method is thought to be more like argument, and more akin to the practice of mathematicians.

Open your favorite math book. It's very unlikely that there are axiomatic proofs in that book (in any strict syntactical sense). Rather, the mathematician assumes something (which may be tentative, or an established fact- usually a fact) and then uses a bit of logic to show what must also be the case given the assumption (granted, s/he will almost always use certain "obvious" arithemtical properties in the proof-or other properties). In short, natural deduction systems are easier to work within. They are more natural.

A simple formal example of a natural deduction proof is

Prove: {A,B,C} |- A^B^C 1. A [Assumptiom] 2. B [Assumption] 3. C [Assumption 4. A^B [1,2 ^I] 5. A^B^C [4,3 ^I]Natural Deduction has Introduction and Elimination Rules for each logical connective such as