Encyclopedia  |   World Factbook  |   World Flags  |   Reference Tables  |   List of Lists     
   Academic Disciplines  |   Historical Timeline  |   Themed Timelines  |   Biographies  |   How-Tos     
Sponsor by The Tattoo Collection
Natural deduction
Main Page | See live article | Alphabetical index

Natural deduction

A natural deduction is an instruction on how to use binary logic to move from one line to another, during a linear sequential proof. Every natural deduction, is one of the tautologies of the propositional calculus. As an example of a natural deduction, consider the hypothetical syllogism HS.

Hypothetical Syllogism HS:If A then B, if B then C; therefore If A then C.

Consider the following deduction of hypothetical syllogism HS, which employs the natural deduction known as modus ponens, in order to 'deduce' that hypothetical syllogism is a natural deduction. Let A,B denote arbitrary statements.

  1. If A then B [Stipulated to be true]
  2. If B then C [Stipulated to be true]
  3. A [Open scope of first assumption]
  4. B [1,3; Modus Ponens]
  5. C [2,4; Modus Ponens]
  6. If A then C [Close scope of first assumption]

As can be seen, this proof that hypothetical syllogism is a natural deduction, relied on the reasoning agent already knowing that modus ponens is a natural deduction.

Modus Ponens MP: If A then B, A; therefore B

Thus, in order for a reasoning agent to learn that hypothetical syllogism is a valid natural deduction from this deduction(alternatively reasoning event), the reasoning agent had to already know that modus ponens is a natural deduction. Modus ponens is a priori knowledge of this reasoning event(knowledge posessed at the beginning of the reasoning event), and hypothetical syllogism is the a posteriori knowledge of this reasoning event(new knowledge).

A reasoning agent who already knows enough natural deductions, so that in principle (memory limitations aside), he can determine whether or not some statement is a natural deduction, is said to be logically omnisicent. See also, the problem of logical omniscience.

Table of contents
1 Systems Of Natural Deduction
2 References
3 External link

Systems Of Natural Deduction

Sometimes, it is said that systems of natural deductions don't have any axioms, but that is misleading. It raises the question, as to what is meant by the term 'axiom'. Setting that question aside, here we give an example of an axiomatic system of natural deduction. The section on symbolic logic also mentions axiomatic treatments of the subject.

Name Of System: L1

Let A,B denote statements.

Undefined terms: not, and

Axiom(conjunction C): A,B; therefore A and B

Axiom(simplification1 S1): A and B; therefore A

Axiom(simplification2 S2): A and B; therefore B

Axiom(double negation1 DN1): not(not A); therefore A

Axiom(double negation2 DN2): A; therefore not(not A)

Axiom(Conjunctive Syllogism CS): A,not(A and not B); therefore B

Definition: A or B = not(not A and not B)

Definition: If A then B = not(A and not B)

Definition: A if and only if B = (if A then B) and (if B then A)

Notice that the axioms were not framed using any of the definitions. This is consistent with common sense, which tells us that definitions aren't logically necessary, but represent abbreviations.

A simple formal example of a natural deduction proof is contained in the first theorem of this system.

Theorem1: A and B; therefore B and A

 1. A and B [Stipulated to be true]
 2. B [1, simplification2]
 3. A [1, simplification1]
 4. B and A [2,3; conjunction]

As you can see, the natural deduction above is a theorem of L1. Now, the question of whether or not L1 is complete, can be raised. That is, the question as to whether or not L1 contains enough axioms in order for a reasoning agent to figure out all possible natural deductions (memory limitations aside), can be raised. If the answer is yes, then the system is said to be complete. It turns out that L1 is complete, but proving so is rather difficult.

The name 'natural deductive system' is suggestive. One of the popular ways of viewing natural deduction is that it is an application of the axioms(laws, rules, whatever) of a system of natural deductive logic to what some have called our "natural modes" of inference.

For instance, if I say that

In the above 'inference', one of the natural deductions was used, but it isn't obvious which one. The answer is modus tollens.

What is happening, is this. The first premise of this argument is a statement made using first order logic. The statement that "all men are mortal" can be symbolized as follows:

For any X: if X is a man then X is mortal.

In fact, we can use set theory to simplify the statement above even more. Let A denote the set of men. Let M denote the set of mortals. Thus, the first premise can be symbolized as follows:

Premise1: For any X: if X is an element of A then X is an element of M.

The second premise of the argument is that sammy isn't mortal. This can be symbolized using set theory as follows. Let s denote the individual sammy.

Premise2: s isn't an element of M

The conclusion of the argument can be symbolized as follows:

Conclusion: s isn't an element of A

So here is the whole argument:

Premise1: For any X: if X is an element of A then X is an element of M.

Premise2: s isn't an element of M

Conclusion: s isn't an element of A

Now, one of the rules of first order logic, is called universal instantiation. There is a universal set which is called the domain of discourse, and only objects in that set can be instantiated for quantified variables. The quantified variable in premise1 above, is X. Even though the domain of discourse wasn't explicitly stated, we are to presume that sammy is one of the elements of the domain of discourse. Thus, s can be substituted(instantiated) for X. After using the rule of universal instantiation UI, we are to conclude that the following statement is true:

If s is an element of A then s is an element of M.

We can now see how modus tollens is being used in the argument above.

Let P=s is an element of A

Let Q=s is an element of M

So here is the structure of the argument above, after universal instantiation was used, properly symbolized for simplicity:

Premise1: If P then Q

Premise2: Not Q

Conclusion: not P

Now, here is the natural deduction known as modus tollens:

Modus Tollens MT: If A then B, not B; therefore not A

So you can see that indeed the argument above used modus tollens, but you can also see that it used universal instantiation. The first philosopher to really make an in depth analysis of first order logic, was Aristotle. In fact, one of his most studied (and consequently now famous) inferences, was this:

All men are mortal.

Socrates is a man.

Therefore, Socrates is mortal

In the roughly 2400 years following Aristotle, first order logic has been brought to near perfection. There are still problems with the concept of a domain of discourse. It isn't always clear what can and cannot be instantiated for a quantified variable, see Russell's Paradox. There are also problems with set theory as well. But these problems aren't problems with systems of natural deduction. Both first order logic, and set theory, have nothing whatsoever to do with natural deductions.

Natural deduction was rigorously worked on by S. Jaskowski in 1934, and G. Gentzen in 1935. However, serious work using natural deduction goes as far back as the ancient Greeks, who worked out the mathematics of geometry, using natural deductions. The greatest example of this, is Euclid's elements. Thus, the technique of natural deduction has been around for as long as there have been reasoners.


Hintikka, J. Knowledge and Belief: An Introduction to the Logic of the Two Notions, Cornell University Press, Ithaca: 1962.

External link