I am working on a proof in the Incredible Proof Machine. My priors are $A \rightarrow (A \rightarrow B)$ and $(A \rightarrow B) \rightarrow A$, and I'm asked to prove $B$. The only logical blocks that I have access to are conjunction, disjunction, modens ponens, and implication introduction.
Now, I happen to know that Pierce's Law allows one to prove that $((A \rightarrow B) \rightarrow A) \rightarrow A$ (and thence $B$), but the only way I know how to prove Pierce's Law is with double negation. My restricted set of options does not allow that at first glance.
Is it possible to prove Pierce's Law with implication directly? If not Pierce's Law, is it possible to prove that $B$ by other means?
Assume $A$
Combined with $A \rightarrow (A \rightarrow B)$ that gives you $A \rightarrow B$
Using $A$ again that gives you $B$.
So, the assumption of $A$ eventually gives you $B$, and so you can infer $A \rightarrow B$ (and this is where the assumption $A$ gets discharged)
Combine $A \rightarrow B$ with $(A \rightarrow B) \rightarrow A$ to give you $A$
And finally, combine that with $A \rightarrow B$ to get $B$
Here is a picture: