Is there a purely syntactic proof of modus ponens with tableau?

Question

The question, more precisely, is this: can we have a purely syntactic proof of the fact that if $S \vdash X$ and $S \vdash X \rightarrow Y$ then $S \vdash Y$ with a Smullyan-style tableau proof system?

It is clear that we have $S \cup \{X, X\rightarrow Y\} \vdash Y$, and it is also clear that by Completeness, if we have that if $S \vDash X$ and $S \vDash X \rightarrow Y$, then $S \vDash Y$, then we have the syntactic version, but this already involves Completeness and semantics.

But how can it be proved that if we have a closed tableau for $S, \neg X$, and a closed tableau for $S, \neg(X \rightarrow Y)$, then we also have a closed tableau for $S, \neg Y$? If $S$ is inconsistent, it is trivial. It is also trivial if $Y$ is a theorem. It is also trivial if $S, X, \neg Y$ closes without making use of any (not necessarily proper) subformula of $X$.

But what if, e.g., $S, \neg(X \rightarrow Y)$ closes through a subformula of $X$ ($Y$) and its negation that is a subformula of $Y$ ($X$)? Then we do not seem to have that subformula of $X$ available in our tableau for $S, \neg Y$ so we cannot just "cut and tack on" the useful part of that tableau to the tableau for $S, \neg Y$.

Answer 1

Your question relates to a fascinating point.

Call a tree proof system using Smullyan's own original rules a Pure Tree System. Call such a tree system augmented with Excluded Middle (in the form: to any open branch you can add a fork with one branch to $A$ and the other to $\neg A$) an Impure Tree System.

Here is an easy result:

Theorem: In an Impure System, if $S \vdash X$ and $S \vdash X \to Y$ and then $S \vdash Y$.

Proof: Start a tree with $S, \neg Y$ and then apply excluded middle, to get [left] $X$ and [right] $\neg X$ on the two branches. The tree that shows $S \vdash X$, i.e. the closed tree headed $S, \neg X$, can then be added to close the right branch. Now take the $S, \neg Y, X$ branch, and use excluded middle again to extend the tree [left] $(X \to Y)$ and [right] $\neg(X \to Y)$. The left branch trivially closes. The right branch closes by appending the tree that shows that $S \vdash X \to Y$, i.e. the closed tree headed $S, \neg (X \to Y)$. QED

Now you might think, ok, surely the difference between a Pure and Impure system should be a minor technical one, and we should get an equally easy theorem for Pure systems. But not so. The difference between the two systems is huge! In effect, adding Excluded Middle, aswe've just shown, is adding a Cut rule. Proving a Cut Elimination theorem -- which is what you want here -- can be tough. And equivalent systems with and without Cut can be dramatically different in how they work. In fact, famously, we have:

Theorem: There are deductions whose smallest closed tree in an Impure Tree System takes just a few pages, and whose smallest closed tree in a Pure Tree System takes more symbols than nanoseconds between Big Bangs.

Proof: George Boolos, "Don't Eliminate Cut".

Answer 2

You are right: there is no straightforward 'syntactical' proof that $S,\neg Y$ closes on the basis of $S, \neg X$ closing and $S, \neg (X \rightarrow Y)$ closing. At least not when using Smullyan's original rules.

There are extensions of Smullyan's system, though, that have a 'splitting' rule, that says that at any point, you can branch on $\phi$ and $\neg \phi$ for any statement $\phi$. And now a purely syntactical proof can easily be found, as starting with $S, \neg Y$, you can start out with 'splitting' on $X \rightarrow Y$ ... and you can fill in the rest.

But yes, with Smullyan's original rules, you'll have to do a bit of semantics to complete the proof.