I consider a Hilbert system defined by the following:
$A \rightarrow (B \rightarrow A)$
$(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
I believe this is called something like minimal logic (?) What I would like to do is prove that Peirce's law cannot be proven in this system: $((A \rightarrow B) \rightarrow A) \rightarrow A$
And I would like to prove this without using ideas from model theory if possible. The idea of proof I have in mind would be to consider all possible combinations of the above rules and show by induction perhaps that they will never yield Peirce's law. Is this possible, if so how? (If it is doable in another logical system such as natural deduction I will also be happy with that)
Although I do a lot of math everyday, I am no expert In logic, I am trying to learn this on my free time, so there maybe well known things that I do not know of.
In general, purely proof-theoretic arguments of unprovability can be very hard to come by, so don't disparage model-theoretic approaches. However, in the case of minimal logic, the Curry-Howard isomorphism provides us with a very tractable representation of proofs as terms in the simply-typed $\lambda$-calculus. There is an algorithm due to Ben-Yelles that lets you count the number of proofs of any formula of minimal logic (which will obviously be $0$ for an unprovable formula). See Hindley's book Basic Simple Type Theory for details. I will sketch the proof of the unprovability of Peirce's law based on Ben-Yelles' ideas (Example 8B6 in Hindley). If you are not familiar with the simply typed $\lambda$-calculus, then the Wikipedia page should give you enough information to give a feel for what is going on.
We need to show that there are no closed simply-typed $\lambda$-terms of type $((A \to B) \to A) \to A$, it can be shown that any such term is equivalent to a term of the form $\lambda f : (A \to B) \to A.f\,U$ for some closed simply-typed $\lambda$-term $U$ of type $A \to B$. But then $U$ must be $\lambda y: A.w\,V_1\,\ldots V_n$ for some $V_1, \ldots, V_n$ ($n \ge 0$), where $w$ is either $y$ or $f$ and $w\,V_1\,\ldots,V_n$ has type $B$, but neither $y$ nor $f$ can deliver a result of type $B$, so there can be no such term and $((A \to B) \to A) \to A$ cannot be provable in minimal logic.
In fact, Peirce's law is not provable even if you add in the rest of intuitionistic logic, but to demonstrate that proof-theoretically requires quite a bit more work (via cut-elimination in a sequent calculus or normalisation in a natural deduction system). Demonstrating it semantically is easier (in my opinion): the very simplest example of a Heyting algebra that is not a Boolean algebra provides a counter-example. That said, I don't disparage the proof-theoretic approaches, because they are very useful in their own right.