How to prove ⊢B→(A→B) (no premise) using natural deduction?

Question

One of the problems in my latest logic homework asks us to prove ⊢B→(A→B) using any of the many rules of natural deduction. I've been at it for several minutes yet can't seem to find a way to solve this... my answer always turns out to be dependent on assumptions I'm unable to eliminate. Is it actually even possible to provide proof when there are no premises? If so, how (in this particular case)?

Answer 1

Yes, the homework is possible to solve.

A proof without premise is, by the completeness theorem (you might not have gotten to this yet in your class) always possible to compute iff the sentence you want to prove is a tautology. If you put up the truth diagram for $B\to(A\to B)$ you can clearly see that it is a tautology, thus a proof exist. However, at times the proof is quite hard to find.

Note that computing $\vdash B\to (A\to B)$ without premises does not say that we can not, as a part of the proof, use assumptions. For instance; if we want to prove $A\to B$ we assume that $A$ hold and, somehow, prove that B hold.

So in your case where you want to prove $B\to (A\to B)$ you need to assume $B$ as a premise and, somehow, prove $(A\to B)$. If you succeed with this, then you can use $\to-$introduction in order to deduce $B\to(A\to B)$ without any assumptions. Can you do this?

Answer 2

I use a Fitch-style layout, where we indent when we start a subproof. But you can massage what follows into your preferred version of a natural deduction system, whatever it is!

One option is to produce a proof that looks like this:

$\quad\quad|\quad B \\ \quad\quad|\quad \vdots\\ \quad\quad|\quad \neg(A \land \neg B)\\ \quad\quad|\quad \vdots\\ \quad\quad|\quad (A \to B)\\ (B \to (A \to B))$

You should know how to fill in the dots -- as both the proof from $B$ to $\neg(A \land \neg B)$ and the proof from $\neg(A \land \neg B)$ to $(A \to B)$ are very elementary natural deduction exercises. Paste the proofs together and you have a proof from the temporary assumption $B$ to $(A \to B)$. So now discharge the temporary assumption, use conditional proof, and you are done!

But there is a much shorter proof available in standard systems. Simply this:

$\quad\quad|\quad B \quad\quad\quad\quad\ \text{temporary assumption}\\ \quad\quad|\quad \quad | \quad A\quad\quad\text{temporary assumption}\\ \quad\quad|\quad \quad | \quad B \quad\quad\text{by iteration}\\ \quad\quad|\quad (A \to B)\quad\quad\text{by conditional proof}\\ (B \to A \to B))\quad\quad\quad\text{by conditional proof}$

For most standard systems of natural deduction allow iteration, and allow 'vacuous discharge' (meaning that all that is required to establish $(A \to B)$ by conditional proof is a subproof starting $A$ and finishing $B$; so $B$ doesn't actually have to depend on $A$).

Of course the second proof looks a bit tricksy: that's why I started with the first one!

Answer 3

my answer always turns out to be dependent on assumptions I'm unable to eliminate.

Work backwards.

• Examine the destination $$\vdash B\to (A\to B)$$
• You would obtain that by using conditional elimination$$B\vdash A\to B$$
• You would obtain that by using conditional elimination$$A,B\vdash B$$
• So...
  • Clearly $B$ is true under the assumption of $A$ and $B$
  • Use two conditional introductions to discharge those two assuptions.
  • Therefore proving the sequent you require with no undischarged assumptions (premises).

$$\begin{split}A,B&\vdash B\\ \hline B & \vdash A\to B\\ \hline &\vdash B\to(A\to B)\end{split}$$

Write that natural deduction proof in your prefered format.