So I have a question regarding natural deduction, are we allowed to "copy" our previous assumption inside a new assumption. I will use an example to illustrate.

$\vdash$ $P\Rightarrow(Q\Rightarrow P)$

So here are my steps.

1.) $P$ Assumption

2.)$Q$ Assumption

3.)$P$ Copy (1)

4.)$Q \Rightarrow P$ Implication Introduction

5.)$P \Rightarrow (Q \Rightarrow P)$ Implication Introduction

Is my proof correct, or is there something missing.

  • $\begingroup$ You don't have to "copy" the first assumption of $P$ — it remains an assumption! Otherwise, when would it end? You copy $P$ following the assumption of $Q$, but now it seems you'd have to copy $Q$... $\endgroup$ – BrianO Jan 31 '16 at 3:57
  • $\begingroup$ In 4. and 5. you're not "introducing" anything, you're discharging assumptions (2. and 1. respectively). $\endgroup$ – BrianO Jan 31 '16 at 4:00
  • $\begingroup$ I don't get what you are trying to tell me. So did I do anything wrong here ? Or its correct but with some unnecessary steps. If I make a mistake, could you kindly point it out for me. Thanks for replying $\endgroup$ – some1fromhell Jan 31 '16 at 4:03
  • $\begingroup$ @BrianO The proof rule that says "if $P \vdash Q$ then $\vdash P \Rightarrow Q$" is usually called "implication introduction". $\endgroup$ – Derek Elkins Jan 31 '16 at 4:18
  • 1
    $\begingroup$ @BrianO: The rule is indeed implication introduction in some presentations of natural deduction, especially Fitch-style. $\endgroup$ – user21820 Jan 31 '16 at 5:21

Just to make it clear why your solution is correct, here it is in Fitch-style: $\def\imp{\Rightarrow}$


If $P$: [(1)]

  If $Q$:

    $P$. [(2); copy from (1)]

  $Q \imp P$. [(3); implication introduction from (2)]

$P \imp ( Q \imp P )$. [implication introduction from (3)]


Intuitively it is obviously correct because whatever you can assert outside of any assumption is still true inside the assumption. That allows you to copy the outer assumption under the inner assumption as you did. The rest is just implication introduction as you did, which is nothing more than collapsing the assumption structure into a single line.

  • 1
    $\begingroup$ @user2875613: I should add that your solution is technically incorrect because you did not clearly specify the assumptions that are active for each line, unlike the Fitch-style solution I gave where the active assumptions are clearly shown using the indentation. $\endgroup$ – user21820 Jan 31 '16 at 11:37
  • $\begingroup$ @user2875613: Do you understand my answer? If it is helpful, you can upvote it, and if you are satisfied with it you can accept it. If not, feel free to ask on any particular point. $\endgroup$ – user21820 Feb 15 '16 at 3:18

Yes, your proof is correct (modulo $P$ is added using a different rule than $Q$).

In natural deduction you have structural rules called contraction, weakening, and exchange. $$ \frac{S,P,P,T \vdash Q}{S,P,T \vdash Q}\ \text{contraction} \quad \frac{S,T \vdash Q}{S, P, T \vdash Q}\ \text{weakening} \quad \frac{S,P,Q,T \vdash R}{S,Q,P,T \vdash R}\ \text{exchange} $$

Usually, these rules are used silently by saying that the collection of assumptions forms a set. You can imagine not having these as structural rules which leads to substructural logic, the most notable of which is linear logic which drops contraction and weakening.

We can now describe your proof (with the minor correction): $P$ is introduced via $P \vdash P$, then $Q$ is added to the assumptions via weakening ($P,Q \vdash P$), then you use contraction to duplicate $P$ ($P,P,Q \vdash P$) and exchange to bring it to the front of the context($P,Q,P\vdash P$), then two uses of implication introduction.

  • 1
    $\begingroup$ I believe the rules you describe are actually for sequent calculus, which Gentzen proved is bi-interpretable with natural deduction, though the two are quite different on the surface. $\endgroup$ – user21820 Jan 31 '16 at 5:19
  • $\begingroup$ @user21820 While I am using sequent notation, the rules are (derivable) rules of natural deduction. $\endgroup$ – Derek Elkins Jan 31 '16 at 5:29
  • 1
    $\begingroup$ Yup that's what I said; "bi-interpretable". $\endgroup$ – user21820 Jan 31 '16 at 5:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.