Completeness of propositional logic of $(p \to q)\to q \vdash (q\to p)\to p$

Question

I've been tasked to make a completeness proof with the style from the book "Logic in Computer Science" by Huth and Ryan. The proof is of $$(p \rightarrow q)\rightarrow q \vdash (q\rightarrow p)\rightarrow p$$ First task was to move everything from the left to right: $$\vdash ((p \rightarrow q)\rightarrow q)\rightarrow (q\rightarrow p)\rightarrow p$$ Next was the Truth-table:

Afterwards I'd been tasked to create the inductive proof for each of the steps with focus on the last line of the truth-table. Creation of the two first proofs was fairly simple:

The next step is to prove: $\neg p, \neg q \vdash (p\rightarrow q)\rightarrow q$, but I can't seem to get the proof right with the premises. How this is an inductive proof, and what is the next step?

Sorry, if the question is too long, or poorly stated. This have had me confused for days.

---

The part of the assignment I've had problems with is seen below. I might have found my problem. Thanks to Bram28 I had my suspicion confirmed, that it wasn't possible to create a direct proof of $\neg p, \neg q \vdash (p\to q) \to q$. Had a talk with some of my classmates and another look in the book, it seems like I've missed the bit, where it was stated, that we can prove the false statement by looking at $\phi_1 \land \neg \phi_2 \vdash \neg (\phi_1 \to \phi_2)$. This is where the induction is introduced.

When the assignment is returned, and I get a better grasp of the method, I'll write an answer to the best of my knowledge.

Answer 1

We have to follow the "proof schema" of page 52-53.

The tautology to be proved (call it $(\text A)$) has two propositional letters: $p$ and $q$. Thus, the proof will need : $p \lor \lnot p$ and $q \lor \lnot q$.

Thus, we have four cases to be dealt with : (i) $p, q \vdash (\text A)$, (ii) $p, \lnot q \vdash (\text A)$, (iii) $\lnot p, q \vdash (\text A)$ and (iv) $\lnot p, \lnot q \vdash (\text A)$.

Alternatively, we can consider : $(p → q) → q \vdash (q → p) → p$.

(i) and (ii) are straightforward, because they need $p$ only, i.e. :

$p \vdash ((p → q) → q) → ((q → p) → p)$.

The derivation is simple :

1) $p \vdash p$

and thus :

2) $p, (p → q) → q, q → p \vdash p$.

The result follows by two $\to$-intro's.

(iii) $\lnot p$ and $q$.

1) $(p \to q) \to q$ --- assumed [a]

2) $q \to p$ --- assumed [b]

3) $p$ --- from 2) and $q$

We have proved :

$\lnot p, q, (p → q) → q, q → p \vdash p$.

Again, two $\to$intro's to conclude the derivation.

(iv) The last case is $\lnot p, \lnot q$.

1) $(p → q) → q$ --- assumed [a]

2) $q \to p$ --- assumed [b]

3) $p$ --- assumed [c]

4) $\bot$ --- from 3) and $\lnot p$

5) $q$ --- from 4)

6) $p \to q$ --- from 3) and 5), discharging [c]

7) $q$ --- from 6) and 1)

8) $\bot$

9) $p$ --- from 8).

We have proved :

$\lnot p, \lnot q, (p → q) → q, q → p \vdash p$.

The last step uses again $\to$-intro, to discharge [a] and [b].