Proof ¬q → ¬p from premise p → q using deductive system& Modus ponens

Question

Using the following deductive system D1:

(A1) A → (B → A)
(A2) (A → B) → ((A → (B → C)) → (A → C))
(A3) (A → B) → ((A → ¬B) → ¬A)
(A4) ¬¬A → A

(MP) A A → B
    ---------
        B

Premise: p → q . Conclusion: ¬q → ¬p

My attempt:

1. p → q

2. (p → q)→((p→ ¬q)→ ¬p) Using (A3) axiom

3. (p→ ¬q)→ ¬p Using Modus ponens- MP(1&2)

So as you see step 3 I have reached ¬p right hand, but I couldn't reach ¬q.

Answer 1

I use Polish notation.

Your axioms are

A1 CaCba

A2 CCabCCaCbcCac

A3 CCabCCaNbNa

A4 CNNaa

Note that {A1, A2} give you a deduction metatheorem. Thus, if we make a hypothesis h and we can then derive the result r, we could find a proof of Chr using the procedure (and other methods to make the work shorter if desired) outlined by a decent meta-proof of the deduction metatheorem.

We want CNqNp, so we'll hypothesize Nq.

  0  Cpq premise
  1  Nq  hypothesis
  2  CNqCpNq   instance of A1
  3  CpNq      2, 1 MP
  4  CCpqCCpNqNp  instance of A3
  5  CCpNqNp  4, 0 MP
  6  Np   5, 3 MP

Now, we just need to have the ability to find C10, C11, C12, C13, C14, C15, and getting to C16 will follow in 3 more steps. C11 follows from the proof of Cpp. C12, and C14 aren't too hard to find, since they're instances of CpCqCrq. CpCqCrq can get found by substituting CqCrq for "a" in A1, p for "b" in A1, and then taking the consequent of the resulting formula. C13 is an instance of A1. C10 isn't hard to find either. Now we just need to get C15 and C16. 5 comes from 4 and 0, and thus due to how a decent meta-proof of the deduction metatheorem works, C15 can come from C14 and C10. 6 comes from 5 and 3, and so C16 will come from C15 and C13. Thus...

  80  Cpq premise
  81  CCpqCNqCpq  instance of A1
  82  CNqCpq   81, 80 MP  (this is C10).
  83  CCCpqCCpNqNpCNqCCpqCCpNqNp instance of A1
  84  CCpqCCpNqNp instance of A3.
  85  CNqCCpqCCpNqNp 84, 83 MP (this is C14).
  86  C CNq Cpq C CNq C Cpq CCpNqNp CNqCCpNqNp instance of A1
  87  CCNqCCpqCCpNqNpCNqCCpNqNp  86, 82 MP
  88  CNqCCpNqNp 87, 85 MP (this is C15).
  89  CNqCpNq instance of A1 (this is C13).
  90  CCNqCpNqCCNqCCpNqNpCNqNp instance of A2
  91  CCNqCCpNqNpCNqNp 90, 89 MP
  92  CNqNp  91, 88 MP

Answer 2

Your axiom system is that of Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997). page 35.

With axioms (A1) and (A2) - as said by Doug - you may prove Deduction Theorem [see Mendelson, page 37 for a proof].

We need an "intermediate result" (we call it Syll) :

$\mathcal A \rightarrow \mathcal B, \mathcal B \rightarrow \mathcal C \vdash \mathcal A \rightarrow \mathcal C$ --- [Corollary 1.10a, page 38]

We prove it with DT :

(1) --- $\mathcal A \rightarrow \mathcal B$ --- assumption

(2) --- $\mathcal B \rightarrow \mathcal C$ --- assumption

(3) --- $\mathcal A$ --- assumption

(4) --- $\mathcal B$ --- from (3) and (1) by modus ponens

(5) --- $\mathcal C$ --- from (4) and (2) by modus ponens

thus : $\mathcal A \rightarrow \mathcal B, \mathcal B \rightarrow \mathcal C, \mathcal A \vdash \mathcal C$;

so : $\mathcal A \rightarrow \mathcal B, \mathcal B \rightarrow \mathcal C, \vdash \mathcal A \rightarrow \mathcal C$ --- by Deduction Theorem.

---

Now with the main proof :

(1) $p \rightarrow q$ --- assumption

(2) $\vdash (p \rightarrow q) \rightarrow ((p \rightarrow \lnot q) \rightarrow \lnot p)$ --- (A3)

(3) $\vdash \lnot q \rightarrow (p \rightarrow \lnot q)$ --- (A1)

(4) $(p \rightarrow \lnot q) \rightarrow \lnot p$ --- from (1) and (2) by modus ponens

(5) $\lnot q \rightarrow \lnot p$ --- form (3) and (4) by Syll.

Thus : $p \rightarrow q \vdash \lnot q \rightarrow \lnot p$.

---

Appendix

If you cannot use the resource of Deduction Theorem, you must prove :

$\vdash (p \rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow r))$

and use it in step (5) of the above proof.

How to prove this [see Mendelson, page 37] ?

We may "mimick" the proof of the DT to find the proof of the above formula.

(Step 1)

(1) --- $\mathcal A \rightarrow \mathcal B$ --- assumption

(2) --- $\mathcal B \rightarrow \mathcal C$ --- assumption

(3) --- $\vdash (\mathcal B \rightarrow \mathcal C) \rightarrow (\mathcal A \rightarrow (\mathcal B \rightarrow \mathcal C))$ --- (A1)

(4) --- $\mathcal A \rightarrow (\mathcal B \rightarrow \mathcal C)$ --- from (2) and (3) by modus ponens

(5) --- $\vdash (\mathcal A \rightarrow \mathcal B) \rightarrow ((\mathcal A \rightarrow (\mathcal B \rightarrow C)) \rightarrow (\mathcal A \rightarrow \mathcal C))$ --- (A2)

(6) --- $(\mathcal A \rightarrow (\mathcal B \rightarrow C)) \rightarrow (\mathcal A \rightarrow \mathcal C)$ --- from (1) and (5) by modus ponens

(7) --- $\mathcal A \rightarrow \mathcal C$ --- from (4) and (6) by modus ponens.

Thus : $\mathcal A \rightarrow \mathcal B, \mathcal B \rightarrow \mathcal C \vdash \mathcal A \rightarrow \mathcal C$.

What have we obtained so far ? A proof of $\mathcal A \rightarrow \mathcal C$ from $\mathcal A \rightarrow \mathcal B$ and $\mathcal B \rightarrow \mathcal C$ without the use of the Deduction Theorem (using only (A1), (A2)).

Now we can repeat the procedure to get :

(Step 2)

(a) --- $\mathcal A \rightarrow \mathcal B$ --- assumption

(b) --- $\vdash (\mathcal A \rightarrow \mathcal B) \rightarrow [(\mathcal A \rightarrow (\mathcal B \rightarrow \mathcal C)) \rightarrow (\mathcal A \rightarrow \mathcal C)]$ --- (A2)

(c) --- $(\mathcal A \rightarrow (\mathcal B \rightarrow \mathcal C)) \rightarrow (\mathcal A \rightarrow \mathcal C)]$ --- from (a) and (b) by modus ponens [call this formula $\mathsf F$]

(d) --- $\vdash \mathsf F \rightarrow [(\mathcal B \rightarrow \mathcal C) \rightarrow \mathsf F]$ --- (A1)

(e) --- $(\mathcal B \rightarrow \mathcal C) \rightarrow \mathsf F$ --- from (c) and (d) by modus ponens

(f) --- $\vdash (\mathcal B \rightarrow \mathcal C) \rightarrow (\mathcal A \rightarrow (\mathcal B \rightarrow \mathcal C))$ --- (A1)

(g) --- $(\mathcal B \rightarrow \mathcal C) \rightarrow (\mathcal A \rightarrow \mathcal C)$ --- from (A2) with (f) and (e).

Thus : $\mathcal A \rightarrow \mathcal B \vdash (\mathcal B \rightarrow \mathcal C) \rightarrow (\mathcal A \rightarrow \mathcal C)$.

Finally, we repeat the above "procedure" to get :

(Step 3)

$\vdash \mathcal A \rightarrow \mathcal B \rightarrow ((\mathcal B \rightarrow \mathcal C) \rightarrow (\mathcal A \rightarrow \mathcal C))$.