# Natural Deduction Tautology

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
-
The first one is correct. –  Git Gud Apr 30 at 0:02
do you know how I would go about doing the second one? –  user146767 Apr 30 at 0:21
No, I'm thinking. Tough one! –  Git Gud Apr 30 at 0:23
I added (above), what I have so far –  user146767 Apr 30 at 0:26
What rules do you have at your disposal? –  Hunan Rostomyan Apr 30 at 0:39

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

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:

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

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

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.$
-
I'm not following the ¬(A→B) part. You show the contradiction, but then you go ahead and use A afterward... –  user146767 Apr 30 at 1:36
@user146767 Which line troubles you? –  Git Gud Apr 30 at 1:36
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? –  user146767 Apr 30 at 1:38
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). –  Hunan Rostomyan Apr 30 at 1:39
Do you have $\bot\text{-Elim}$? –  Git Gud Apr 30 at 1:39

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\alphaN\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.

-