Axiomatic Proof of Conjunction Introduction I need to give an axiomatic proof from $\{\psi, \phi\}$ to $\neg(\phi\rightarrow\neg\psi)$.                             
I can use the deduction theorem, axioms PL1, PL2 and PL3 (I have also established that $\vdash P\rightarrow P, \vdash (\neg P \rightarrow P) \rightarrow P, \neg\neg P \vdash P)$ and the rules of Weakening, The MP Technique, Transitivity, Cut Elimination, Contraposition, Principle of Explosion, Negated Condition and Excluded Middle.                                                   
I'm stuck at a very long line of conditions that I got from a combination of Weakening, Contraposition and the schema of the results I've already proven. I'm having a hard time either getting a contradiction so that I can use the P.O.E. to get my result.                                                                
Does anyone have tips or advice about how to proceed? Maybe I should use the axioms more?                      
 A: Exactly what your proof will look like will depend on which inference rules you have access to. My best advice would be to proceed in three steps:


*

*Taking $\phi$, $\psi$ and $\phi \to \neg \psi$ as premises, can you arrive at a contradiction such as $\neg (\chi \to \chi)$? For this you will need modus ponens and your principle of explosion.

*Now that you know that $\phi$, $\psi$ and $\phi \to \neg \psi$ lead to a contradiction, can you use this derive $(\phi \to \neg \psi) \to \neg (\chi \to \chi)$ from $\phi$ and $\psi$? This is much easier if you are able to use the deduction theorem, which I notice you didn't explicitly say you could use. If you don't have the deduction theorem, this part is trickier, but it's possible to do it using the PL1 and PL2 axioms.

*Can you turn your proof of $(\phi \to \neg \psi) \to \neg (\chi \to \chi)$ into a proof of $\neg (\phi \to \neg \psi)$? For this you will need your contraposition rule (or PL3) and potentially the double-negation rule you derived earlier. Your proof of $\vdash P \to P$ and modus ponens is likely to come in handy for the last step.
This isn't a complete answer, but should hopefully be enough of a hint that you can fill the rest of the bits in.
