Axiomatic proofs in propositional logic

Question

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 :

1. $(\neg\neg P \to \neg Q) \vdash (Q \to \neg P)$

2. $\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.

Answer 1

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: