Proof for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR

Question

I can't find a for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR

HR is the following system:

axioms:

$A\rightarrow A$

$(A\rightarrow B)\rightarrow ((B\rightarrow C)\rightarrow (A \rightarrow C))$

$(A\rightarrow (B\rightarrow C))\rightarrow (B\rightarrow (A\rightarrow C))$

$(A\rightarrow (A\rightarrow B))\rightarrow (A\rightarrow B)$

and the inference rule is MP.

I already proved that general claim that might help:

If $T,A\vdash B$ and $T\nvdash B$ than $T\vdash A\rightarrow B$

So here it's easy to prove that $\{p,p\rightarrow (q\rightarrow r),(p\rightarrow q)\}\vdash r$ ,

but I have know idea how to show that $\{p,p\rightarrow (q\rightarrow r)\}\nvdash r$

Answer 1

We assume that we do not have the resource of Deduction Theorem available.

(1) --- $p \rightarrow (q \rightarrow r)$ --- Assumption

(2) --- $p$ --- Assumption

(3) --- $(q \rightarrow r)$ --- from (1) and (2) by modus ponens

(4) --- $\vdash (p \rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow r))$ --- Axiom 2

(5) --- $\vdash (q \rightarrow r) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$ --- from (4) and Axiom 3 by modus ponens

(6) --- $(p \rightarrow q) \rightarrow (p \rightarrow r)$ --- from (3) and (5) by modus ponens

Now we need the following form of Axiom 4 [$(A→(B→C))→(B→(A→C))$ - we use the substitution : $p \rightarrow q/A; p/B; r/C$ ] :

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

(8) --- $p \rightarrow ((p \rightarrow q) \rightarrow r)$ --- from (6) and (7) by modus ponens

Now, it's done : apply modus ponens using the Assumption $p$, and we will get :

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

The conclusion "depends" on the assumptions : $p$ and $p \rightarrow (q \rightarrow r)$.

Answer 2

Since Willemien thought it better to show that [p→((p→(q→r))→((p→q)→r))] is a theorem, I'll do that here.

I use Polish notation.

Your axioms are:

3 Cpp (weak law of identity)

4 CCpqCCqrCpr (syll or hypothetical syllogism)

5 CCpCqrCqCpr (commutation or "transposition")

6 CCpCpqCpq (contraction or Hilbert)

I use the notation Dx.y * z for condensed detachment with x as the major premise, y as the minor premise, and "z" as the resulting formula. I'll also write the annotation of the proof before the proof.

D4.4 * 8

 8 CCCCqrCprsCCpqs

D5.4 * 9

 9 CCqrCCpqCpr

D5.3 * 10

 10 CpCCpqq

D4.10 * 11

 11 CCCCpqqrCpr

D9.6 * 12

 12 CCrCpCpqCrCpq

D11.4 * 13

 13 CpCCqrCCpqr

D5.13 * 14

 14 CCpqCrCCrpq

D8.12 * 15

 15 CCpqCCqCprCpr

D5.15 * 16

 16 CCqCprCCpqCpr

D16.14 * 17

 17 CCrCpqCrCCrpq

D5.17 * 18

 18 CpCCpCqrCCpqr

Now we assume {p, CpCqr}. By 18 and "p" we detach CCpCqrCCpqr. From CpCqr and CCpCqrCCpqr we detach CCpqr.