2
$\begingroup$

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.

$\endgroup$
9
  • $\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, 2016 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, 2016 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, 2016 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 left SE
    Jan 31, 2016 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, 2016 at 5:21

2 Answers 2

Reset to default
3
$\begingroup$

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

Solution

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)]

Notes

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.

$\endgroup$
2
  • 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, 2016 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, 2016 at 3:18
1
$\begingroup$

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.

$\endgroup$
3
  • 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, 2016 at 5:19
  • $\begingroup$ @user21820 While I am using sequent notation, the rules are (derivable) rules of natural deduction. $\endgroup$
    – Derek Elkins left SE
    Jan 31, 2016 at 5:29
  • 1
    $\begingroup$ Yup that's what I said; "bi-interpretable". $\endgroup$
    – user21820
    Jan 31, 2016 at 5:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .