Natural Deduction Tautology

Question

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

Answer 1

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

Answer 2

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:

Answer 3

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.

Answer 4

Pierce's Law: $$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{~~1.~(A\to B)\to A}{\fitch{~~2.~\neg A}{\fitch{~~3.~A}{~~4.~\bot\hspace{13.5ex}{\neg}\mathsf E~3,2\\~~5.~B\hspace{14ex}\mathsf X~4}\\~~6.~A\to B\hspace{11.5ex}{\to}\mathsf I~3{-}5\\~~7.~A\hspace{17ex}{\to}\mathsf E~6,1\\~~8.~\bot\hspace{17ex}\neg\mathsf E~7,2}\\~~9.~\neg\neg A\hspace{17ex}\neg\mathsf I~2{-}8\\10.~A\hspace{20ex}{\neg\neg}\mathsf E~9}\\11.~((A\to B)\to A)\to A\hspace{3ex}{\to}\mathsf I~1{-}10}$$