A Cancellation Algorithm for Elementary Logic
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 syntactically2 or semantically3. Methods of this type have been adapted for use with electronic computers4. However, the cancellation algorithm presented here is primarily designed for use with computers4 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.
Unable to display preview. Download preview PDF.
- 2.E.g., cf. Kanger, S., Provability in Logic, Stockholm Studies in Philosophy I, Almquist & Wiksell, Stockholm, 1957.Google Scholar
- 3.E.g., cf. Beth, E. W., “Semantic Entailment and Formal Derivability”, Medel. der Kon. Nederl. Akad. van Wetensch., deel 18, no. 13, Amsterdam, 1955, and Hintikka, J., “Two Papers on Symbolic Logic”, Acta Philosophica Fennica, Fasc. VIII, Helsinki, 1955.Google Scholar
- 4.E.g., cf. Prawitz, D., “An Improved Proof Procedure”, Theoria, 26, no. 2, pp. 102–139, 1960.Google Scholar