Easy question on Logic and Modes Ponens

Question

I got confused with these:

using ONLY this three axioms and Modus Ponens:$$1. \ F \implies (G\implies F) \\ 2. \ (F \implies (G\implies H))\implies ((F \implies G)\implies (F \implies H)) \\ 3. \ (\neg G \implies \neg F)\implies ((\neg G\implies F)\implies G)$$

I need to prove: $$4. \ (F \implies G)\implies ((G \implies H)\implies(F\implies H))\\$$ I see it intuitively, but I have to use ONLY the axioms.

I started like this: $$1. F \implies G\\2. \ H \implies (F \implies G) \ by \ (1)\\3.((H\implies F)\implies (H \implies G)) \ by \ (2)$$ but that is not what I want

Thank you for your help.

Answer 1

The automated theorem prover OTTER has found a 10 step, level 5 proof:

----> UNIT CONFLICT at   4.26 sec ----> 11611 [binary,11610.1,2.1] $F.

Length of proof is 10.  Level of proof is 5.

---------------- PROOF ----------------

1 [] -P(i(x,y))| -P(x)|P(y).
2 [] -P(i(i(a,b),i(i(b,c),i(a,c)))).
3 [] P(i(x,i(y,x))).
4 [] P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
5 [hyper,1,4,4] P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).
7 [hyper,1,3,4] P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).
8 [hyper,1,3,3] P(i(x,i(y,i(z,y)))).
16 [hyper,1,4,7] P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))).
18 [hyper,1,5,8] P(i(i(x,i(i(y,x),z)),i(x,z))).
42 [hyper,1,16,16] P(i(i(x,i(y,i(z,u))),i(i(x,i(y,z)),i(x,i(y,u))))).
56 [hyper,1,3,18] P(i(x,i(i(y,i(i(z,y),u)),i(y,u)))).
230 [hyper,1,42,3] P(i(i(i(x,y),i(z,x)),i(i(x,y),i(z,y)))).
431 [hyper,1,18,56] P(i(i(i(x,y),z),i(y,z))).
11610 [hyper,1,431,230] P(i(i(x,y),i(i(y,z),i(x,z)))).
11611 [binary,11610.1,2.1] $F.

Interestingly enough, there exists at least two proofs with a greater level, but which have less steps. OTTER found a 9 step, level 7 proof:

 ----> UNIT CONFLICT at   0.17 sec ----> 514 [binary,513.1,2.1] $F.

 Length of proof is 9.  Level of proof is 7.

 ---------------- PROOF ----------------

 1 [] -P(i(x,y))| -P(x)|P(y).
 2 [] -P(i(i(a,b),i(i(b,c),i(a,c)))).
 3 [] P(i(x,i(y,x))).
 4 [] P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
 5 [hyper,1,4,4] P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).
 8 [hyper,1,3,3] P(i(x,i(y,i(z,y)))).
 14 [hyper,1,5,8] P(i(i(x,i(i(y,x),z)),i(x,z))).
 24 [hyper,1,3,14] P(i(x,i(i(y,i(i(z,y),u)),i(y,u)))).
 56 [hyper,1,14,24] P(i(i(i(x,y),z),i(y,z))).
 120 [hyper,1,3,56] P(i(x,i(i(i(y,z),u),i(z,u)))).
 125 [hyper,1,56,5] P(i(i(x,y),i(i(x,i(y,z)),i(x,z)))).
 275 [hyper,1,4,120] P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))).
 513 [hyper,1,275,125] P(i(i(x,y),i(i(y,z),i(x,z)))).
 514 [binary,513.1,2.1] $F.

And a 7 step, level 6 proof:

 ----> UNIT CONFLICT at   0.37 sec ----> 2045 [binary,2044.1,2.1] $F.

 Length of proof is 7.  Level of proof is 6.

 ---------------- PROOF ----------------

 1 [] -P(i(x,y))| -P(x)|P(y).
 2 [] -P(i(i(a,b),i(i(b,c),i(a,c)))).
 3 [] P(i(x,i(y,x))).
 4 [] P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
 7 [hyper,1,3,4] P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).
 13 [hyper,1,4,7] P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))).
 25 [hyper,1,13,13] P(i(i(x,i(y,i(z,u))),i(i(x,i(y,z)),i(x,i(y,u))))).
 29 [hyper,1,13,3] P(i(i(x,y),i(i(z,x),i(z,y)))).
 85 [hyper,1,25,3] P(i(i(i(x,y),i(z,x)),i(i(x,y),i(z,y)))).
 357 [hyper,1,29,85] P(i(i(x,i(i(y,z),i(u,y))),i(x,i(i(y,z),i(u,z))))).
 2044 [hyper,1,357,3] P(i(i(x,y),i(i(y,z),i(x,z)))).
 2045 [binary,2044.1,2.1] $F.