I'm trying to prove the following tautologies:

\begin{align} & ⊢ (A \to (B \to A)) \\ & ⊢ ((A \to B) \to A) \to A \end{align}

For the first one, what I did was:

  1. $A$ assumption
    1. $B$ assumption
    2. $A$ restated
  2. $B \to A$ arrow-introduction of 2 and 3
    1. $A \to (B \to A)$ arrow-introduction of 1-4

But this doesn't look right to me.

For the second one, here's what I have so far:

  1. ((A --> B) --> A) assumption
    1. A --> B assumption
    2. A arrow-elimination of 1 and 2
  • 5
    $\begingroup$ The first one is correct. $\endgroup$ – Git Gud Apr 30 '14 at 0:02
  • $\begingroup$ do you know how I would go about doing the second one? $\endgroup$ – user146767 Apr 30 '14 at 0:21
  • $\begingroup$ No, I'm thinking. Tough one! $\endgroup$ – Git Gud Apr 30 '14 at 0:23
  • $\begingroup$ I added (above), what I have so far $\endgroup$ – user146767 Apr 30 '14 at 0:26
  • 2
    $\begingroup$ What rules do you have at your disposal? $\endgroup$ – Hunan Rostomyan Apr 30 '14 at 0:39

You'll be starting by assuming $(A\to B)\to A$.

Ideally one would want to prove $A\to B$ and then $A$ would follow, but of course $A\to B$ is not a tautology, so it can't be proven. But $\neg (A\to B)\lor (A\to B)$ is a tautology and therefore it can be proven.

So you'll prove the aforementioned tautology, then you'll perform $\lor\text{-Elim}$ on this tautology.

One of the cases follows from the initial hypothesis.

It remains to be shown that you can prove $A$ from $\neg(A\to B)$.

This goes something like this:

  • $\neg (A\to B)$
  • $\,\,\,\,\neg A$ (Hypothesis)
  • $\,\,\,\,\,\,\,\,\,\,\,\, A$ (Hypothesis)
  • $\,\,\,\,\,\,\,\,\,\,\,\,\bot$
  • $\,\,\,\,\,\,\,\, \,\,\,\,B$
  • $\,\,\,\,A\to B$
  • $\,\,\,\, \bot$
  • $\neg \neg A$
  • $A.$
  • $\begingroup$ I'm not following the ¬(A→B) part. You show the contradiction, but then you go ahead and use A afterward... $\endgroup$ – user146767 Apr 30 '14 at 1:36
  • $\begingroup$ @user146767 Which line troubles you? $\endgroup$ – Git Gud Apr 30 '14 at 1:36
  • $\begingroup$ So I understand the not-A then A hypotheses (though I don't quite see the purpose of that yet), so of course it's a contradiction. But where does B come from, and how do you get A --> B after? $\endgroup$ – user146767 Apr 30 '14 at 1:38
  • $\begingroup$ Nice. I used contraposition, modus tollens, now you're explicitly appealing to excluded middle. I wonder if the formula we're both trying to prove is intuitionistically valid....If it's not then I wouldn't feel so bad for not being able to come up with a more 'direct' proof (if that makes sense). $\endgroup$ – Hunan Rostomyan Apr 30 '14 at 1:39
  • $\begingroup$ Do you have $\bot\text{-Elim}$? $\endgroup$ – Git Gud Apr 30 '14 at 1:39

You've solved the first, so here are two ways of proving the second one. 'Taut Con' is modus tollens.

enter image description here

I've taken the liberty of typing Git Gud's alternative proof more explicitly here (please vote his answer up if you too find it insightful). It highlights the connection to the law of excluded middle and is economical in its use of special rules (e.g. doesn't appeal to modus tollens). Here it is:

enter image description here

Another way would be to prove the contrapositive, using just $\rightarrow$-intro & Reit:

enter image description here

  • $\begingroup$ I'm not sure if I can use step 5... $\endgroup$ – user146767 Apr 30 '14 at 0:52
  • $\begingroup$ What do you mean? $\endgroup$ – user146767 Apr 30 '14 at 0:57
  • $\begingroup$ Barwise & Etchemendy's Fitch is the proof-checker; the rules are in their book Language, Proof, and Logic. $\endgroup$ – Hunan Rostomyan Apr 30 '14 at 0:57
  • $\begingroup$ @user146767 Does the proof by contraposition make sense? $\endgroup$ – Hunan Rostomyan Apr 30 '14 at 0:57
  • 1
    $\begingroup$ @HunanRostomyan Thanks for typing my proof, though personally I'd prove $\neg(A\to B)\lor (A\to B)\,\,\ddot \smile$ $\endgroup$ – Git Gud Apr 30 '14 at 1:57

I use Polish notation. The second formula becomes CCCabaa. The rule I'll use (other than arrow introduction, which I'll call "Ci", and detachment/conditional elimination, which I'll call "Co") is {CN$\alpha$$\beta$, CN$\alpha$N$\beta$} $\vdash$ $\alpha$, which I'll call "No".

hypothesis 1  |     CCaba
hypothesis 2  ||    Na
hypothesis 3  |||   a
hypothesis 4  ||||  Nb
hypothesis 5  ||||| a
Ci 5-5     6  ||||  Caa
Co 6, 3    7  ||||  a
Ci 4-7     8  |||   CNba
hypothesis 9  ||||  Nb
hypothesis 10 ||||| Na
Ci 10-10   11 ||||  CNaNa
Co 11, 2   12 ||||  Na
Ci 9-12    13 |||   CNbNa
No 13, 8   14 |||   b
Ci 3-14    15 ||    Cab
Co 1, 15   16 ||    a
Ci 2-16    17 |     CNaa
hypothesis 18 ||    Na
Ci 18-18   19 |     CNaNa
No 17, 19  20 |     a
Ci 1-20    21       CCCabaa

For the first one you could also write:

hypothesis 1 |   a
hypothesis 2 ||  b
hypothesis 3 ||| a
Ci 3-3     4 ||  Caa
Co 4, 1    5 ||  a
Ci 2-5     6 |   Cba
Ci 1-6     7     CaCba

I have to wonder why you didn't also get asked to prove CCpCqrCCpqCpr. Since you can prove CCpCqrCCpqCpr using only conditional introduction and detachment, a consequence here come as that all implications (well-formed formulas with just "C"'s and variables in them) which qualify as tautologies can get proved from conditional introduction, detachment, and the rule

{CN$\alpha$$\beta$, CN$\alpha$N$\beta$} $\vdash$ $\alpha$, since {CpCqp, CCpCqrCCpqCpr, CCCpqpp} under detachment and uniform substitution comes as sufficient for the implicational propositional calculus.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.