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