Is my proof that $(p \wedge \neg p) \Rightarrow q$ correct? I was asked by a professor a while ago to prove $(p \wedge \neg p)$ implies $q$.  Whether through laziness or cleverness, I came up with the following proof:


$p \wedge \neg p$ (by assumption).
Assume by way of contradiction $\neg q$.
$p \wedge \neg p$, therefore $p$ (I forget what this rule is called).
Similarly, $p \wedge \neg p$, therefore $\neg p$.
We have both $p$ and $\neg p$, a contradiction.
Therefore, our assumption, $\neg q$, must have been false, i.e., $q$ is true, the desired result.


Is this right?  I keep going either way about it to myself.  On the one hand, it definitely feels circular.  On the other hand, it seems contain all the correct elements of a contradiction proof. 

EDIT: many commenters seem concerned about what I am allowed or not allowed to "use".  I am allowed to use whatever you feel mathematically is correct, and not allowed to use things that aren't.  The context of the exercise was not a course in logic, or even in mathematics.  It was a computer science class in algorithms.  I think the professer just wanted to get a feel for our understanding of logic, and also wanted to demonstrate why inconsistant assumptions can be used to prove anything.  I don't even remember if the assignment was graded, or if it was what I got.  I do remember that when I presented it on the board that it (obviously) wasn't quite what the professor was looking for.
Given the tools you have chosen to work with, you have a valid proof of $p\land \neg p\Rightarrow \neg\neg q$. Formally you would need an extra step where you point out that $\neg\neg q$ is the same as $q$, but that's not the real problem here.

The reason why it feels circular is that what you're being asked to prove is one of several possible logical axioms that can be used to justify proof by contradiction in the first place, so the difference between the rule you use and the conclusion is only very slight. It is then natural to wonder whether you're supposed to prove it from more primitive ingredients than proof by contradiction. However, what those particular ingredients might be varies considerably between formalizations of logic.

Basically one can choose any of quite a lot of possible logical foundations to use as axioms, and then prove that all of the other ones follow as logical consequences of the axioms we have chosen. (For pedants in the audience, this is assuming that the axiom sets in question are all for classical first-order logic, blah blah blah). In ordinary mathematical reasoning one tacitly allows all of those standard consequences as single proof steps that need no explanation because the reader is always expected to be able to formalize them in his own favorite logic if he wants to. However, that won't work here, because then there wouldn't be anything for you to prove! So it is necessary to be explicit about which proof steps one allows here, because otherwise your exercise just implodes.

If one happens to choose an axiom set that includes $p\land \neg p\Rightarrow q$ as an axiom, then there's nothing to prove -- a full and complete proof would consist of the words "it's an axiom". But if you choose not to make it an axiom, then what counts as a valid proof depends critically upon what you do consider axioms.



If you do not have a particular formal system you must do your proof in, then I suspect that the expected solution is simply by truth tables -- for each of the possible 4 combinations of whether $p$ and $q$ are true or false, show that $p\land \neg p\Rightarrow q$ evaluates to true.

Then you have proved "$p\land \neg p\Rightarrow q$ is always true" which is just a more convoluted way of saying that you have proved $p\land \neg p\Rightarrow q$ itself.
The answer is: yes, your proof is correct.

Instead of reductio ad absurdum, your can use the principle of explosion. Falsum $\bot$ follows from $p$ and $\neg p$, and ex falso sequitur quodlibet, so one can conclude $q$ directly from $\bot$. This is trivial though, whereas your proof shows the strength of double negation elimination.