Published online by Cambridge University Press: 12 March 2014
A fundamental problem of symbolic logic is to define logical calculi sufficient to comprise important parts of mathematics, and to develop systematic methods of calculation therein.
The possibility of progress in this direction has been severely limited by Gödel's proof that a consistent system sufficient to comprise arithmetic must contain propositions whose truth-value cannot be decided within the system, and by Church's extension of Gödel's method to the result that even in the first order logical function calculus the general decision problem cannot be solved.
1 Gödel, Kurt, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, vol. 38 (1931), pp. 173–198.CrossRefGoogle Scholar
2 Church, Alonzo, A note on the Entscheidungsproblem, this Journal, vol. 1 (1936), pp. 40–41Google Scholar; Correction to A note on the Entscheidungsproblem, ibid., pp. 101-102.
3 Explained in Chapter IV of General analysis, Part II, by E. H. Moore with the cooperation of R. W. Barnard, American Philosophical Society, 1939.
4 Blake, Archie, Canonical expressions in Boolean algebra, University of Chicago doctoral dissertation, 1937.Google Scholar
5 It is of interest that the applicability of process II is not confined to the first order logical function calculus.
6 For the purpose of verifying that this and subsequent formulas belong to the first order logical function calculus, it is to be noted that each of the factors in parentheses is simply a truth-function of certain x's and y's.