Natural Deduction

After we have looked at the general idea of deductive systems, we focus on the particular system we will be using in this course: (focused) Natural Deduction.

The Natural Deduction system was invented by the logician Gerhard Gentzen in 1934 as a way to formalise proofs in logic. We will be using a variant of Gentzen's system that is designed to be easy to use for building proofs interactively.

The key feature of Natural Deduction is its modularity. There are two basic rules of the system, Done and Use, that allow us to manage assumptions. Then there are separate rules for each connective "and", "implies", "or" and "not". For each connective, we have Introduction rules that tell us how to prove a statement using that connective, and Elimination rules that tell us how to use a statement built from that connective. The natural symmetry between introduction and elimination rules gives the whole system a balanced feel.

Slides for these videos (PDF).

Video: Introducing Natural Deduction

Online Proof Editor

To help you build proofs, these pages contain a proof editor specialised to the Natural Deduction proof system we will be using. The rest of this page contains information on how to use the editor for proofs involving And and Implication (see the next page on implication), and has some exercises for you to do.

Video

Commands for the Editor

The blue boxes represent parts of the proof that are unfinished. The comments (in green) tells you what the current goal is. Either the goal is unfocused:

{ goal: <some formula> }

or there is a formula is focus:

{ focus: <formula1>; goal: <formula2> }

The commands that you can use differ according to which mode youare in. The commands correspond directly to the proof rules given in the videos.

Unfocused mode

These rules can be used when there is no formula in the focus. These rules either act on the conclusion directly to break it down into simpler sub-goals, or switch to focused mode (the use command).

• split can be used when the goal is a conjunction P ∧ Q. The proof will split into two sub-proofs, one to prove the first half of the conjunction P, and one to prove the other half Q.

• true can be used when the goal to prove is ‘T’ (true). This will finish this branch of the proof.

• use H can be used whenever there is no current focus. H is the name of some assumption that is available on this branch of the proof.

Focused mode

These rules apply when there is a formula in focus. These rules either act upon the formula in focus, or finish the proof when the focused formula is the same as the goal.

• done can be used when the formula in focus is exactly the same as the goal formula. This will finish this branch of the proof.

• first can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘P’, the first part of the conjunction, and the proof continues.

• second can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘Q’, the second part of the conjunction, and the proof continues.

Exercises

Writing out formal proofs on paper is extremely tedious, so I have written an online proof editor tool that you will be using to build your own proofs.

1. A entails A:

   (config (assumptions (H "A")) (goal "A") (solution (Rule(Use H)((Rule Close())))))

2. A and B entails A /\ B

   (config (assumptions (H1 A) (H2 B)) (goal "A /\ B") (solution (Rule Split((Rule(Use H1)((Rule Close())))(Rule(Use H2)((Rule Close())))))))

3. A /\ B entails A /\ B

   (config (assumptions (H "A /\ B")) (goal "A /\ B") (solution (Rule Split((Rule(Use H)((Rule Conj_elim1((Rule Close())))))(Rule(Use H)((Rule Conj_elim2((Rule Close())))))))))

4. A /\ B entails B /\ A

   (config (assumptions (H "A /\ B")) (goal "B /\ A") (solution (Rule Split((Rule(Use H)((Rule Conj_elim2((Rule Close())))))(Rule(Use H)((Rule Conj_elim1((Rule Close())))))))))

5. Anything entails T

   (config (assumptions (H "A")) (goal "T") (solution (Rule Truth())))

6. True on the right:

   (config (assumptions (H "A")) (goal "A /\ T") (solution (Rule Split((Rule(Use H)((Rule Close())))(Rule Truth())))))

7. True on the left:

   (config (assumptions (H "A")) (goal "T /\ A") (solution (Rule Split((Rule Truth())(Rule(Use H)((Rule Close())))))))