Why does natural deduction get its name?

Question

For example, I want to prove $\psi$ from the assumption $\{\varphi,\varphi\to\psi\}$ , the "most natural" proof would be:

$\varphi$

$\varphi\to\psi$

$\psi$(MP)

But using natural deduction, I must write the following sequence:

1. $\varphi\vdash\varphi$ (Ref)

2. $\varphi,\varphi\to\psi\vdash\varphi$ (+,1)

3. $\varphi\to\psi\vdash\varphi\to\psi$ (Ref)

4. $\varphi,\varphi\to\psi\vdash\varphi\to\psi$ (+,3)

5. $\varphi,\varphi\to\psi\vdash\psi$ ($\to$-,2,4)

This does not look "natural" at all. I cannot write a formula alone on a line. Every line is of the form: $\sum_i\vdash A_i$. Many logic books use this kind of proof system. My "most natural" proof looks like a Hilbert proof system, but Hilbert proof system was considered not natural thus natural deduction system was invented.

Did I misunderstand natural deduction proof system, or use natural deduction in a wrong way?

Answer 1

As an example, let's consider the simple tautology $(B\rightarrow C) \rightarrow ((A\rightarrow B) \rightarrow (A\rightarrow C))$. This just says if $B$ implies $C$ and $A$ implies $B$, then you can compose the two and conclude $A$ implies $C$.

For a Hilbert style proof: for clarity, A1 will be the axiom schema $A\rightarrow (B\rightarrow A)$ and A2 will be the axiom schema $(A\rightarrow (B\rightarrow C)) \rightarrow ((A\rightarrow B) \rightarrow (A\rightarrow C))$.

1. A2: $((B\rightarrow C)\rightarrow((A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))))\rightarrow(((B\rightarrow C)\rightarrow(A\rightarrow(B\rightarrow C)))\rightarrow((B\rightarrow C)\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))))$.
2. A1: $((A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C)))\rightarrow((B\rightarrow C)\rightarrow((A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))))$.
3. A2: $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$.
4. MP on 2 and 3: $(B\rightarrow C)\rightarrow((A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C)))$.
5. MP on 1 and 4: $((B\rightarrow C)\rightarrow(A\rightarrow(B\rightarrow C)))\rightarrow((B\rightarrow C)\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C)))$.
6. A1: $(B\rightarrow C)\rightarrow(A\rightarrow(B\rightarrow C))$.
7. MP on 5 and 6: $(B\rightarrow C)\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$.

Awful, right? And this was one I selected for being one of the easiest cases with a lot of coincidental optimizations available, to reduce the amount I would have to type. If for example you had reversed the hypotheses and wanted to prove $(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$, then things wouldn't have worked out even this nicely.

And for that matter, why accept A1 and A2 as axioms in the first place? Yes, you can give informal arguments for why each is true, but those arguments suggest that there should be a more reasonable way to prove things.

Now as for the natural deduction proof:

1. $B\rightarrow C, A\rightarrow B, A \vdash A\rightarrow B$: assumption.
2. $B\rightarrow C, A\rightarrow B, A \vdash A$: assumption.
3. $B\rightarrow C, A\rightarrow B, A \vdash B$: ${\rightarrow}E$ on 1 and 2.
4. $B\rightarrow C, A\rightarrow B, A \vdash B\rightarrow C$: assumption.
5. $B\rightarrow C, A\rightarrow B, A \vdash C$: ${\rightarrow}E$ on 4 and 3.
6. $B\rightarrow C, A\rightarrow B \vdash A\rightarrow C$: ${\rightarrow}I$ on 5.
7. $B\rightarrow C \vdash (A\rightarrow B)\rightarrow(A\rightarrow C)$: ${\rightarrow}I$ on 6.
8. $\vdash (B\rightarrow C)\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C)$: ${\rightarrow}I$ on 7.

If you read this from bottom to top (mostly) and then from 1 through 5 top to bottom, this more closely reflects how we would informally argue that the formula is a tautology: if you assume $B\rightarrow C$, then you assume $A\rightarrow B$, then you furthermore assume $A$, then from the last two you can conclude $B$, and then combining with the first hypothesis, you can also conclude $C$. Therefore, if you know $B\rightarrow C$ and $A\rightarrow B$, you can conclude $A\rightarrow C$. As a result, if you know $B\rightarrow C$, then you also know $(A\rightarrow B)\rightarrow(A\rightarrow C)$; and therefore, the given formula is a tautology as we wanted to show.

(It does seem that your formulation of natural deduction doesn't have "assumption" as a primitive proof rule, and instead forces you to start with the proof rule R and then add the unused hypotheses. Still, this is a minor point and when you want to extract an assumption from the context, it's straightforward to make this argument. It doesn't fundamentally result in an exponential explosion of the proof length and unreadable intermediate terms, the way that proofs in a Hilbert style system tend to do - once you've expanded any uses of the Deduction Theorem. And proofs in a Hilbert system using the Deduction Theorem tend to look much closer to a natural deduction type of proof in practice, anyway -- so at that point, why not just use a natural deduction system in the first place?)

Answer 2

In Hilbert-style proofs, the order in which the formulae of the proof are presented is ambiguous. Also, in order to make it readable, you need annotations. I just presented two problems that natural deduction systems don't have. As for the name, it stems not from the fight of who has the better proof writing system, but from historical reasons. As a last point, since they are just writing systems, formalities to make our life easier, it really comes down to preference.

Answer 3

What you have is not "The Natural Deduction System", rather it is "A Natural Deduction System".

Natural Deduction proof systems are those with many Rules of Inference and few Axiomatic Schema (preferably none), where the justification for those rules are based on "natural reasoning processes about the logical connectives". They are simple, easy to follow instructions, that may have a tendency to build bulky proofs of even obvious statements.

The other category of proof systems are "Axiomatic", which have many "Axiom Schema" and few "Rules of Inference" (usually just one: modus ponens). Hilbert's system is an axiomatic system.