How do I prove the Deduction theorem using tableaux in propositional logic?

Question

How do I prove the Deduction theorem using tableaux in propositional logic?

I heard it is easier than proving it from the Hilbert's calculus, but couldn't find the proof.

Answer 1

The deduction theorem in propositional logic using tableaux is a direct result of the tableaux rule which says from $\lnot (A \to B)$ we may deduce $A$ and $\lnot B$. (For a reference on this rule, see Graham Priest, An Introduction to Non-Classical Logic, section 1.4. The book is about non-classical logic but chapter 1 reviews classical propositional logic using the tableaux style of proof.)

Interpret $\vdash$ in the tableuax sense, and suppose that $\Delta \cup \{A\} \vdash B$. To prove the deduction theorem, we want to show $\Delta \vdash A \to B$. (Here, $\Delta$ is a possibly infinite set of sentences of propositional logic, and $A$ and $B$ are single sentences of propositional logic.)

"$\Delta \cup \{A\} \vdash B$" means there is a closed tableaux starting from the assumptions $\Delta_0 \subseteq \Delta$, $A$, and $\lnot B$, where $\Delta_0$ is some finite subset of $\Delta$. Call this tableuax $T$.

Now we want to construct a tableaux proving $\Delta \vdash A \to B$, i.e. a closed tableuax $T'$ from the assumptions $\Delta$ and $\lnot (A \to B)$. So to construct $T'$, begin with assumptions $\Delta_0$ and $\lnot (A \to B)$, then apply the deduction rule from $\lnot (A \to B)$ to get $A$ and $\lnot B$. Then simply append the tableaux $T$. Since we have all the assumptions of $T$, $T'$ is a valid tableaux. Since $T$ closes, $T'$ closes. This completes the proof.