How could I derive the following proposition:
$$ ((A \rightarrow B) \rightarrow A) \rightarrow A ) $$
using any of the following axioms:
1) $A→(B→A)$
2) $(A→(B→C))→((A→B)→(A→C))$
3) $((¬B)→(¬A))→(A→B)$
How could I derive the following proposition:
$$ ((A \rightarrow B) \rightarrow A) \rightarrow A ) $$
using any of the following axioms:
1) $A→(B→A)$
2) $(A→(B→C))→((A→B)→(A→C))$
3) $((¬B)→(¬A))→(A→B)$
By the deduction theorem, it's enough to show that $((A \to B) \to A) \vdash A$. This can be done by contradiction, i.e. we assume $((A \to B) \to A)$ and $\lnot A$ and derive a contradiction. From $\lnot A$, we can use axiom 1 and modus ponens to get $(\lnot B \to \lnot A)$, and then use axiom 3 and MP to get $(A \to B)$. Then using MP with $(A \to B)$ and $((A \to B) \to A)$ gives us $A$, contradicting $\lnot A$ as desired.
If you haven't seen the proof-by-contradiction inference rule before, here's how to derive it: we suppose $\Gamma$ (a set of sentences) and $\lnot A$ together lead to a contradiction, and want to show that $\Gamma \vdash A$. Since $\Gamma$ and $\lnot A$ are contradictory, they prove anything, so $\Gamma, \lnot A \vdash \lnot (A \to (A \to A))$ say (here $(A \to (A \to A))$ could be replaced by any tautology). Then by the deduction theorem, we have $\Gamma \vdash (\lnot A \to \lnot (A \to (A \to A)))$, and then by axiom 3 and MP, $\Gamma \vdash ((A \to (A \to A)) \to A)$. Since $(A \to (A \to A))$ is a tautology, using MP again gives $\Gamma \vdash A$, as desired.
joriki points out that my proof of proof-by-contradiction uses the fact that a contradiction implies anything, that is, the inference rule $A, \lnot A \vdash B$. As it happens, I did most of the work of proving this above, when I inferred $(A \to B)$ from $\lnot A$. One more use of MP gives the result.
Here's an unraveled version of Chris' proof, with proof by contradiction and ex falso quodlibet unraveled but the deduction theorem still being used:
$$ \begin{array}{lrcl} 1.&\neg A &\vdash& \neg C\to\neg A &&\text{axiom 1, modus ponens} \\ 2.& \neg A &\vdash& A\to C &&\text{1., axiom 3, modus ponens} \\ 3.& (A\to B)\to A,\neg A &\vdash& A &&\text{2.} [C\mapsto B]\text{, modus ponens} \\ 4.& (A\to B)\to A,\neg A &\vdash& A\to\neg(A\to(A\to A)) &&\text{2.} [C\mapsto \neg(A\to(A\to A))] \\ 5.& (A\to B)\to A,\neg A &\vdash& \neg(A\to(A\to A)) &&\text{3., 4., modus ponens} \\ 6.& (A\to B)\to A &\vdash& \neg A\to\neg(A\to(A\to A)) &&\text{5., deduction theorem} \\ 7.& (A\to B)\to A &\vdash& (A\to(A\to A))\to A &&\text{6., axiom 3, modus ponens} \\ 8.& (A\to B)\to A &\vdash& A &&\text{7., axiom 1, modus ponens} \\ 9.& &\vdash& ((A\to B)\to A)\to A &&\text{8., deduction theorem} \end{array} $$
If you want to unravel it further to use only the axioms and modus ponens, no deduction theorem, you can transform it as described here. The basic idea is that if you have a proof using hypothesis $A$, you conditionalize on $A$ by tacking $A$ on as a premise in front of every statement in the proof, including $A$ itself; then you transform every application of modus ponens that derives $C$ from $B$ and $B\to C$ by using axiom 2 and applying modus ponens twice (using the conditionalized inputs $A\to(B\to C)$ and $A\to B$ of the modus ponens step to derive its conditionalized output $A\to C$); then it just remains to prove the conditionalized hypothesis itself, $A\to A$, which is shown in the Wikipedia article:
$$ \begin{array}{lrl} 1.& (A→((A→A)→A))→((A→(A→A))→(A→A)) &\text{axiom 2} \\ 2.& A→((A→A)→A) & \text{axiom 1} \\ 3.&(A→(A→A))→(A→A)&\text{1., 2., modus ponens} \\ 4.&A→(A→A)&\text{axiom 1} \\ 5.&A→A&\text{3., 4., modus ponens} \end{array} $$
I use Polish notation and condensed detachment.
axiom 3 CpCqp recursive variable prefixing
axiom 4 CCpCqrCCpqCpr self-distribution
axiom 5 CCNpNqCqp strong transposition
D3.3 7 CpCqCrq prefixed recursive variable prefixing
D4.4 8 CCCpCqrCpqCCpCqrCpr distributed self-distribution
D3.4 9 CpCCqCrsCCqrCqs prefixed self-distribution
D4.3 10 CCpqCpp distributed recursive variable prefixing
D4.5 11 CCCNpNqqCCNpNqp distributed strong transposition
D3.5 12 CpCCNqNrCrq prefixing strong transposition
D4.7 13 CCpqCpCrq distributed prefixed recursive variable prefixing
D3.7 14 CpCqCrCsr prefixed prefixed recursive variable prefixing
D10.3 15 Cpp weak identity
D4.15 16 CCCpqpCCpqq distributed identity
D8.7 17 CCpCCqprCpr
D8.14 18 CCpCCqCrqsCps
D4.12 19 CCpCNqNrCpCrq
D17.12 20 CNpCpq Duns Scotus
D17.9 21 CCpqCCrpCrq double prefixing
D4.20 22 CCNppCNpq distributed Duns Scotus
D3.20 23 CpCNqCqr prefixed Duns Scotus
D16.23 24 CCCNpCpqrr specialized Duns Scotus assertion
D18.21 25 CCCpqrCqr double suffixed recursive variable prefixing
D25.16 26 CpCCpqq assertion
D25.11 27 CpCCNqNpq commuted strong transposition
D21.26 28 CCpqCpCCqrr double prefixed assertion
D4.27 29 CCpCNqNpCpq distributed commuted strong transposition
D24.28 30 CNpCCCpqrr
D24.29 31 CNNpp double negation out
D29.22 32 CCNppp Clavius
break...
D5.31 33 CpNNp double negation in
D21.33 34 CCpqCpNNq double prefixed double negation in
D21.32 35 CCpCNqqCpq double prefixed Clavius
D19.34 36 CCNpqCNqp negation-variable transposition
D36.30 37 CNCCCpqrrp
D35.13 38 CCNCpqqCpq
D38.37 39 CCCpqpp Peirce