Biconditional Introduction in natural deduction

Question

I'm working on a first-order logic question and I'm a little stuck as to what I should be assuming in my first subproof (this is always my problem). I'm supposed to prove this biconditional argument with no premises.

$P → (Q → R)) \leftrightarrow ((P ∧ Q) → R)$

I know that in order to do this, I need to prove that [P → (Q → R))] → [((P ∧ Q) → R)] ^ [((P ∧ Q) → R)] → [P → (Q → R))].

If I'm starting with my first subproof assuming P → (Q → R)), what is the next thing I need to assume so I can end up proving ((P ∧ Q) → R)? This is my thought process, but I get stuck at the point where I need to prove a →Intro.

P → (Q → R))
   P
   Q→R  →Elim 1
      Q
      P^Q  ^Intro 2,4
      R  →Elim 3,4

After this I'm not quite sure what to do - how can I isolate it out so that R is the consequence of both P and Q?

Answer 1

Okay, now I've tackled the first subproof. Thanks for your help! This is what I got.

(P→(Q→R))
   (P^Q)
   P  ^Elim2
   Q  ^Elim2
   (Q→R)
   R  →Elim 4,5
   ((P^Q)→R)  →Intro 2-6

Answer 2

It seems you really got it. Indeed, for a formal derivation using natural deduction in the general case, we just need to observe the logical form of the goals and decide which rules to use.

In your particular case, the statement you want to prove has the form of a biconditional $\phi \leftrightarrow \psi$, so we just have to prove that $\phi \rightarrow \psi$ and $\psi \rightarrow \phi$ holds first and appy the biconditional introduction rule:

$\frac{\frac{D}{\phi \rightarrow \psi}, \frac{D'}{\psi \rightarrow \phi}}{\phi \leftrightarrow \psi}$

Now we just observe the logical form of $\phi$ and $\psi$ and proceed with the other steps.