Formal logic proof verification I am trying to prove the following sequent formally.
$$P, (P \land Q)\Rightarrow  \sim R \vdash R\Rightarrow \sim Q$$
I have come up with the following formal proof, but I am not completely sure if this is correct. I feel a little uncomfortable about throwing in $R$ as an assumption.

 A: $$\begin{array}{|l|l:l|}\hdashline
1.1&\quad P &\text{A}  \\
1.2&\quad (P \land Q) \rightarrow \neg R &\text{A} \\
1.3&\quad (P \land ((P \land Q) \rightarrow \neg R) &1.1,1.2\ \land \text{I} \\ \hdashline
2.1&\qquad R \qquad &\text{A} \\
2.2&\qquad \neg \neg R \rightarrow \neg(P \land Q) &1.2\ \text{MT} \\
2.3&\qquad R \rightarrow \neg(P \land Q) &2.2\ \text{DN} \\
2.4&\qquad \neg(P \land Q) \qquad &2.1,2.3  \\ \hdashline
3.1&\qquad\quad Q \qquad &\text{A} \\
3.2&\qquad\quad (P \land Q) \qquad &1.1,3.1\ \land \text{I} \\
3.3&\qquad\quad Q \rightarrow (P \land Q) &3.1,3.2 \\
3.4&\qquad\quad \neg(P \land Q) \rightarrow \neg Q &3.3\ \text{MT} \\
3.5&\qquad\quad \neg Q &2.4,3.4 \\
3.6&\qquad\quad Q \land \neg Q &3.1,3.5\ \land \text{I} \\
3.7 &\qquad\quad \perp \qquad &3.6 \\ \hline
2.5 &\qquad \neg Q \qquad &3.1,3.7 \\ \hline
1.4 &\quad R \rightarrow \neg Q &2.1,2.5 \\ \hline
0.1 & (P \land ((P \land Q) \rightarrow \neg R) \rightarrow (R \rightarrow \neg Q) & 1.3,1.4 \\\hline
\end{array}$$
Note that the horizontal lines, indentation, and numbering system reflect the 'scope' of the assumptions made. This might be a little verbose but I think it's correct.

Update: three years later, I'd do it this way
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}
\fitch{~~1.~P\\~~2.~(P\land Q)\to\lnot R}{\fitch{~~3.~R}{\fitch{~~4.~Q}{~~5.~P\land Q\hspace{5ex}\land\,\mathsf {Intro},1,4\\~~6.~\lnot R\hspace{8ex}\to\mathsf {Elim}, 1,5\\~~7.~\bot\hspace{10ex}\lnot\,\mathsf {Elim}, 3,6}\\~~8.~\lnot Q\hspace{12ex}\lnot\,\mathsf {Intro}, 4{-}7}\\~~9.~R\to\lnot Q\hspace{9.5ex}\to\mathsf {Intro}, 3{-}8}$$
A: 
I feel a little uncomfortable about throwing in $R$ as an assumption.

Assuming $R$ is fine; you discharged that assumption correctly to obtain the desired conditional.   That's exactly what you needed to do.
Your actual problem child was properly obtaining the needed consequent, $\neg Q$.
Since you can use modus tollens for conditional elimination, here's how I'd do it using your rules of inference.
$$\begin{align} & \boxed{ \begin{array}{|r|l:l:r|}
1 & P & \textsf{Premise} & \text{A} \\
2 & (P\wedge Q)\to\neg R & \textsf{Premise} & \text{A} \\ \hdashline
3 & \quad R & \textsf{Assumption} & \text{A} \\
4 & \quad \neg\neg R & 3, \neg\neg\textsf{Introduction} & 3,\text{DN} \\
5 & \quad \neg (P\wedge Q) & 2,4,\to\textsf{Elimination (Modus Tollens)} & 2,4,\text{MT} \\ \hdashline
6 & \qquad Q & \textsf{Assumption} & \text{A} \\
7 & \qquad P\wedge Q & 1,6,\wedge\textsf{Introduction} &  1,6,\wedge \text{I} \\ \hline
8 & \quad Q\to (P\wedge Q) & 6,7, \to\textsf{Introduction} & 6,7,\text{CP} \\
9 & \quad \neg Q & 5,8,\to\textsf{Elimination (Modus Tollens)} & 5,8,\text{MT} \\\hline
10 & R\to \neg Q & 3,9,\to\textsf{Introduction} & 3,9,\text{CP}
\end{array} } \\ \Box ~ & P~, (P\wedge Q)\to R~~\vdash~~R\to\neg Q\end{align}$$
A: As Doug Spoonwood noted in a comment, "Step 8 is not correct." $¬Q$ cannot be derived by conjunction elimination from $P ∧ Q$. 
The following is a proof that also assumes $R$ as the antecedent of the conditional that one desires to show. Having that as an assumption allows one to derive the conditional after deriving the consequent. 


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
