I'm reading the "Introduction to deep inference" notes https://hal.inria.fr/hal-02390267/document and trying to do the Exercise 1.1.4 from there which is about proving the Peirce's law $((A\to B)\to A)\to A$ in Hilbert System H.
The axioms of the system are following:
1. $A\to(B\to A)$.
2. $(A\to(B\to C))\to(A\to B)\to A\to C$.
3. $A\to(A\lor B)$.
4. $B\to(A\lor B)$.
5. $(A\to C)\to (B\to C) \to ((A\lor B) \to C)$.
6. $(A\land B)\to A$.
7. $(A\land B)\to B$.
8. $\texttt{f}\to A$.
9. $\neg\neg A\to A$.
10. $A\to(B\to(A\land B))$.
And the Modus Ponens Rule of Inference.
So, I would like to do this proof using only these axiom schemes and Modus Ponens but encountered some difficulties. I have an idea to use Axioms 1, 2 and 9, but don't actually know how to connect them in a right way.
Since this is a conclusion the Peirce's law should be the instance of Modus Ponens rule at the end. But I don't know for now what should it be.
Will be grateful for any help.
IMO, there is something missing in the description of the system: something linking $\text f$ with the negation sign: $\lnot$.
The simplest way to add it is to define the latter with the former:
If so, the derivation of Peirce's Law is straightforward, using Deduction Theorem (provable with MP, Ax,1 and Ax.2: see many similar posts on this site):
1) $(A \to B) \to A$ --- premise
2) $\lnot A$ --- assumption [a]
3) $A$ --- Assumption [b]
4) $\text f$ --- from 2) and 3) by MP, using the definition of $\lnot A$
5) $B$ --- from 4) and Ax.8, by MP
6)$A \to B$ --- from 3) and 5) by DT, discharging assumption [b]
7) $A$ --- from 6) and 1) by MP
8) $\text f$ --- from 2) and 7)
9) $\lnot \lnot A$ --- from 2) and 8) by DT and using again the def of $\lnot A$, discharging assumption [a]
10) $A$ --- from 9) Ax.9, by MP