# Prove: $((A \rightarrow B) \rightarrow A) \rightarrow A )$

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

-
You have supplied only axioms, and no rules of inference. – André Nicolas Feb 21 '12 at 7:14
Sorry. Modus ponens should be used. – user25376 Feb 21 '12 at 7:16
This is Peirce's law, which is equivalent to (3) in the presence of (1) and (2). – Zhen Lin Feb 21 '12 at 7:22
Thanks. I'm still not sure how to prove this. :| I'm pretty new to propositional calculus. – user25376 Feb 21 '12 at 8:16
@Arjang: It's fairly standard in logic to use $\to$ for the implication symbol in the object language and reserve ⟹ for implication in the metalanguage. – Chris Eagle Feb 21 '12 at 12:49

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.

-
I think to complete this you'd have to show how "Since $\Gamma$ and $\neg A$ are contradictory, they prove anything" can be derived in this system. – joriki Feb 21 '12 at 13:07

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

-
How did you produce firs step? Modus pones says $(A \implies B) \land A \vdash B$ but in your case A was not any axiom and it was not infered so it looks like you could not produce B. It looks like you used deduction theorem not modus ponens. – Trismegistos Feb 21 '12 at 17:59
@Trismegistos: I'm assuming that you mean the first step in the first of the two proofs. As indicated in the right-hand column, this is modus ponens applied to an instance of axiom $1$. The substitution for the $A\to(B\to A)$ axiom schema that produces this is $A\mapsto\neg A,B\mapsto\neg C$, yielding $\neg A\to(\neg C\to\neg A)$. The premise $\neg A$ is noted as a hypothesis on the left-hand side, and applying modus ponens yields $\neg C\to\neg A$. The deduction theorem moves premises from the left of the turnstyle to the right; modus ponens moves them from the right to the left. – joriki Feb 21 '12 at 18:00
but if you marked $\lnot A$ as hypotesis you showed that sentence you wanted to prove is true if your hypothesis $\lnot A$ is true. Isn't it? – Trismegistos Feb 21 '12 at 18:06
@Trismegistos: I'm not sure why you talk about truth. To my mind this is about proof. Apart from that, yes, I showed that the sentence $\neg C\to\neg A$ can be proved if the hypothesis $\neg A$ is assumed. That's what the deduction theorem is all about -- you assume hypotheses, prove something from them, then turn the hypotheses into antecedents of the proved statement by applying the deduction theorem. In this case, the hypothesis $\neg A$ is used in step 6 in applying the deduction theorem. – joriki Feb 21 '12 at 18:10
I undestood your proof after reading Chris Eagle message. – Trismegistos Feb 21 '12 at 18:12

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

-