A Cancellation Algorithm for Elementary Logic

Abstract

The purpose of the present essay is to set forth a convenient algorithm for the lower functional calculus with identity. The method is open-ended when applied to formulae of certain types and so, as was to be expected, it cannot in general be relied upon to show something not to be a logical truth when in fact it is not one. But when the method is applied to a formula expressing a logical truth, the method will eventually show it to be such, and it will not show something to be a logical truth unless it really is. The proof of these facts will not be given here, but it should be clear that the method is closely related to known systems with respect to which results of this sort have been established. These are the systems of natural deduction, either conceived syntactically² or semantically³. Methods of this type have been adapted for use with electronic computers⁴. However, the cancellation algorithm presented here is primarily designed for use with computers⁴ made of pencil and paper, and its convenience is to be judged in those terms. It is a mechanical procedure which is designed to provide maximum opportunity for shortcuts based on simple insight; it stands to conventional methods rather as Quine’s truth-value analysis stands to the full truth-table method.