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

-

1
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

3
@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
show 3 more comments

## 2 Answers

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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 54, "mathjax_display_tex": 3, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9321098923683167, "perplexity_flag": "head"}