Given ∼R and ∼ B, derive ∼ (R ∨ B) *This question deals with the derivation system SD (Sentential Derivation), the rules of which can be seen on pages 3-4 here: http://www.shamik.net/teaching/materials/dasgupta%20SL%20definitions.pdf
I've begun with the assumption (R v B) with the intentions of using Negation Introduction, then within that subderivation another 2 separate assumptions R and B with the intentions of using Disjunction Elimination. I'm trying to find a contradiction within the first subderivation in order to introduce the negation. Any help would be greatly appreciated.
Edit: In my class we use ~ instead of ¬, in case anyone was confused (trivial, I know)
 A: So you're assuming $\neg R$ and $\neg B$, and have further assumed $R\lor B$ with the intention of using your $\neg\mathbf{Intro}$ rule in order to conclude $\neg(R\lor B)$. So far so good. You now need to produce a contradiction.
It also looks right to use the $\lor\mathbf{Exit}$ on the $R\lor B$ assumption. The problem now is that in each of those branches it's easy to produce a contradiction -- in one of them you're assuming $R$ which contradicts your overall $\neg R$ assumption, and in the other you're assuming $B$ which contradicts the overall $\neg B$ assumption. But the $\lor\mathbf{Exit}$ rule wants the two branches to have the same conclusion, and what you have easily is two different contradictions.
The trick for getting around this is to use $\neg\mathbf{Exit}$ in one of the branches to convert one contradiction to another. For example, let's say we're in the $R$ branch and we want to conclude $B\&\neg B$. Preparing to use $\neg\mathbf{Exit}$ we assume $\neg(B\&\neg B)$, and then immediately derive our already-present contradiction $R$ with $\neg R$. (We never use the assumption $\neg(B\&\neg B)$ while doing that, but nobody says we have to, as long as we end up with the premises the rule wants!). Thus we can conclude $B\&\neg B$. We can also immediately get that in the $B$ branch, so the proof now fits together!
As a bit of optimization we can save a bit of "plumbing" by letting the conclusion of the $\lor\mathbf{Exit}$ be just $B$ instead of $B\&\neg B$. Then we can draw on overall $\neg B$ assumption outside $\lor\mathbf{Exit}$. The $B$ branch of $\lor\mathbf{Exit}$ is now extremely simple; in the $R$ branch we conclude $B$ using $\neg\mathbf{Exit}$. (Namely, assume $\neg B$ (in addition to the assumption we already have), ignore that assumption, and pull the contradiction $R$ with $\neg R$ out of the other assumptions).
(Sorry if the prose description is hard to follow. It's not clear to me how your system wants formal proof sequences written down graphically such that assumptions are being properly kept track of).
