# 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 :

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.

• 1. is simply Contraposition : $(\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta)$. You can find a proof of it in this post. – Mauro ALLEGRANZA Sep 17 '19 at 12:32
• 2. is an instance of Ef Falso : $\lnot \alpha \to (\alpha \to \beta)$. You can find a proof of it in this post. – Mauro ALLEGRANZA Sep 17 '19 at 12:37
• @MauroALLEGRANZA Thanks for the links, however I think my question differs in that I have a non-empty set of premise propositions. This would make the proofs different, no? As opposed to proving a theorem without any assumptions. – asilentfrog Sep 17 '19 at 13:06
• Use Modus Ponens. – Mauro ALLEGRANZA Sep 17 '19 at 13:10
• Oh as an additional last step. Is the proof the exact same though? Having the additional assumption doesn't make them any simpler? – asilentfrog Sep 17 '19 at 13:19

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: