Natural deduction

The section on symbolic logic mentions axiomatic treatments of the subject. Here we say a bit about systems of natural deduction.

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.

The general move is this. One begins a proof by assuming 'all x are such that, if x is A then x is M'. Next assume that something (call it 's') is not M, ie. assume 'it is not the case that s is M'. Now, a system of natural deduction will license the use of these assumptions. Moreover, the rules of the system will license the move from the first assumption 'all x, A(x) then M(x)' to 'A(s) then M(s)'[it would be called 'universal instantiation' or something]. We have 'not M(s)', and it readily follows that not 'A(s)' (The rule is called modus tollens, for those systems that countenance it - it need not be countenanced if there are other "simpler rules" capable of handling the inference. If such simpler rules are present, the absence of modus tollens notwithstanding, the inference just takes more steps.)

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 and depicted as "^" above. Justifications for each step shown in square brackets explicitly identify which previous lines in the proof are used, as well as which inference rule.