Don't eliminate cut (Q1057847)

Semantic tableau methods are sometimes used in logic courses because they produce derivations of various formulas of first order logic in a straightforward way. The feasibility of these tableau methods depends, however, on the formulas to which they are applied. This paper provides a simple formula H whose derivation by the tableau methods of Smullyan and Jeffrey would have more than \(2^{128}\) characters, hence ''more symbols than there are nanoseconds between Big Bangs''. On the other hand, there is a derivation of H in, essentially, Gentzen's system of natural deduction, containing less than 3280 characters. The tableau methods in question are closely related to cut-free systems. What is really given here is a formula without a feasible cut-free derivation. The emphasis on natural deduction in the paper is a bit misleading. As the author mentions, the crucial point is that modus ponens provides for increased efficiency by allowing an appeal to previously established conclusions. The example shows in a vivid way just how great the gain in efficiency can be.