2
$\begingroup$

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.

$\endgroup$
6
  • 1
    $\begingroup$ 1. is simply Contraposition : $(\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta)$. You can find a proof of it in this post. $\endgroup$ – Mauro ALLEGRANZA Sep 17 '19 at 12:32
  • 1
    $\begingroup$ 2. is an instance of Ef Falso : $\lnot \alpha \to (\alpha \to \beta)$. You can find a proof of it in this post. $\endgroup$ – Mauro ALLEGRANZA Sep 17 '19 at 12:37
  • $\begingroup$ @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. $\endgroup$ – asilentfrog Sep 17 '19 at 13:06
  • 1
    $\begingroup$ Use Modus Ponens. $\endgroup$ – Mauro ALLEGRANZA Sep 17 '19 at 13:10
  • $\begingroup$ Oh as an additional last step. Is the proof the exact same though? Having the additional assumption doesn't make them any simpler? $\endgroup$ – asilentfrog Sep 17 '19 at 13:19
0
$\begingroup$

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:

enter image description here

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.