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} $$ |
|||||||||||
|