So here is the proposition I'd like to prove:
a ∨ ¬a ⊢((a→b)→a)→a
I have tried many way to find a proof, and always end up in a mess...
for example:
a ∨ ¬a ⊢((a→b)→a)→a
a ⊢((a→b)→a)→a (elimination of disjunction)
a ∧ (a→b)⊢ a→a
(a→b)∧ a ⊢ a→a
(a→b) ⊢ a→a→a
(a→b) ⊢ True?
Anybody has an idea how to get me out of my mess?
Thank you!
Suppose $a$. Then $((a\rightarrow b)\rightarrow a)\rightarrow a$.
Now suppose $\lnot a$. Then $(a\rightarrow b)$. So if $(a\rightarrow b)\rightarrow a$, by modus ponens $a$. So $((a\rightarrow b)\rightarrow a)\rightarrow a$.
In either case, we have $((a\rightarrow b)\rightarrow a)\rightarrow a$, so $a\lor \lnot a\vdash ((a\rightarrow b)\rightarrow a)\rightarrow a$.