Axiomatic proofs in propositional logic I have to use these three axioms
(A1) $P \to (Q \to P)$ 
(A2) $(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$
(A3) $(\neg Q \to \neg P) \to ((\neg Q \to P) \to Q)$
along with Modus Ponens to prove :


*

*$(\neg\neg P \to \neg Q) \vdash (Q \to \neg P)$

*$\neg(\neg \neg P \to \neg Q), (\neg \neg P \to \neg Q) \vdash P$
I understand the process of creating the proof, but I have tried many things and have racked my brain to no avail. Any help would be appreciated, thanks.
 A: For the first one:  If you are allowed to use the Deduction Theorem, it's pretty straightforward. First, let's prove $\neg \neg P \to \neg Q, Q \vdash \neg P$:
$1 \ \neg \neg P \to \neg Q \ Assumption$
$2 \ Q \ Assumption$
$3 \ Q \to (\neg \neg P \to Q) \ Axiom \ 1$
$4 \ \neg \neg P \to Q \ MP \ 2,3$
$5 \ (\neg \neg P \to \neg Q) \to ((\neg \neg P \to Q) \to \neg P) \ Axiom \ 3$
$6 \ (\neg \neg P \to Q) \to \neg P \ MP \ 1,5$
$7 \ \neg P \ MP \ 4,6$
OK, so now that we have $\neg \neg P \to \neg Q, Q \vdash \neg P$, we just use the Deduction Theorem, and we get $\neg \neg P \to \neg Q \vdash Q \to \neg P$
If you are not allowed to use the Deduction Theorem, then this one gets a good bit nastier:
$1 \ \neg \neg P \to \neg Q \ Assumption$
$2 \ (\neg \neg P \to \neg Q) \to (Q \to  (\neg \neg P \to \neg Q)) \ Axiom \ 1$
$3 \ Q \to  (\neg \neg P \to \neg Q) \ MP \ 1,2$
$4 \ Q \to  (\neg \neg P \to Q) \ Axiom \ 1$
$5 \ (\neg \neg P \to \neg Q) \to ((\neg \neg P \to Q) \to \neg P) \ Axiom \ 3$
$6 \ ((\neg \neg P \to \neg Q) \to ((\neg \neg P \to Q) \to \neg P)) \to (Q \to ((\neg \neg P \to \neg Q) \to ((\neg \neg P \to Q) \to \neg P))) \ Axiom \ 1$
$7 \ Q \to ((\neg \neg P \to \neg Q) \to ((\neg \neg P \to Q) \to \neg P)) \ MP \ 5,6$
$8 \ (Q \to ((\neg \neg P \to \neg Q) \to ((\neg \neg P \to Q) \to \neg P))) \to ((Q \to (\neg \neg P \to \neg Q)) \to (Q \to ((\neg \neg P \to Q) \to \neg P))) \ Axiom \ 2$
$9 \ (Q \to (\neg \neg P \to \neg Q)) \to (Q \to ((\neg \neg P \to Q) \to \neg P)) \ MP \ 7,8$
$10 \ Q \to ((\neg \neg P \to Q) \to \neg P) \ MP \ 3,9$
$11 \ (Q \to ((\neg \neg P \to Q) \to \neg P)) \to ((Q \to (\neg \neg P \to Q)) \to (Q \to \neg P)) \ Axiom \ 2$ 
$12 \ (Q \to (\neg \neg P \to Q)) \to (Q \to \neg P) \ MP \ 10, 11$
$13 \ Q \to \neg P \ MP \ 4,12$
The second one is of the form $\neg Q, Q \vdash P$, and that is actually really easy to prove:
$1 \ \neg Q \ Assumption$
$2 \ Q \ Assumption$
$3 \ \neg Q \to (\neg P \to \neg Q) \ Axiom \ 1$
$4 \ \neg P \to \neg Q \ MP \ 1,3$
$5 \ Q \to (\neg P \to Q) \ Axiom \ 1$
$6 \ \neg P \to Q \ MP \ 2,5$
$7 \ (\neg P \to \neg Q) \to ((\neg P \to Q) \to P) \ Axiom 3$
$8 \ (\neg P \to Q) \to P \ MP \ 4,7$
$9 \ P \ MP \ 6,8$
So, instead of $Q$, use $\neg \neg P \to \neg Q$ in the above proof, and you're done. Here is a computer-verified proof:

