Modern Logic: Since G?del: Church
MODERN LOGIC: SINCE GÖDEL: CHURCH
From the beginning of the twentieth century questions concerning the decidability of logical and mathematical theories have held a special interest for logicians, mathematicians, and philosophers. A number of important concepts and far-reaching results in this field have come from Alonzo Church (1903–1995), author of a definitive text on logic and noted writer on the history of logic.
The notion of decidability is not one which a beginner in mathematics could explicitly formulate, but both this and related notions, such as that of effective calculability, have a place in the description of the most elementary mathematical concepts. Often our understanding of a particular numerical predicate is inextricably tied to our ability to determine whether or not an arbitrary number satisfies that predicate, and in many cases terms expressing the result of a calculation or computation can be fully grasped only by one who has the ability to carry out the sorts of computation in question. Thus, with the division of numbers into odd and even there is intimately associated a technique for determining which of these predicates applies to an arbitrary whole number; similarly, a person's grasp of the concepts of sum and product is measured by his ability to calculate sums and products. But although the grasp of concepts and the mastering of techniques may go hand in hand in many cases, the symbolism of arithmetic allows us to formulate propositions whose truth-value may resist determination by any obvious methods of computing or reasoning in general, a situation that frequently arises with the introduction of unrestricted quantification.
Consider, for instance, the proposition P, "There is at least one odd perfect number." A perfect number is a number that is equal to the sum of its divisors, itself excluded. Thus, 6 is perfect, being equal to the sum of 1, 2, and 3; so is 28, being equal to the sum of 1, 2, 4, 7, and 14. Like "x is odd," the predicate "x is perfect" is a decidable predicate, in the sense that given any number n, we can, after a finite number of steps, respond with an unambiguous yes or no to the question "Is n perfect?" But although both of the predicates entering into P are decidable, the infinitude of the positive integers is an obstacle to an immediate determination of the truth-value of P which would make use of the decidability of these predicates together with a case-by-case examination of the integers. Indeed, proposition P, along with Fermat's last theorem, Goldbach's conjecture, and many other propositions of elementary number theory, has as yet been neither proved nor disproved. Accordingly we may well wonder whether it is possible to devise a technique that, when applied to an arbitrary proposition of this class, would enable us to determine the truth or provability of the proposition. Now, for all we know, any one of these outstanding problems may eventually be resolved, but Church showed that no general technique could be devised which would allow us to ascertain in an effective manner the truth or provability of an arbitrary arithmetical proposition.
By a direct application of the method of diagonalization (a procedure whereby a hypothesized function is shown to differ from each member of a class of functions of which it must be a member if it is to exist), Church demonstrated not simply that such a technique has proved elusive but that the supposition of its existence involves an absurdity. In this respect arithmetic contrasts with the propositional calculus, but although the propositional calculus does have a decision procedure—the method of truth-tables—Church showed that the first-order functional calculus fares no better than arithmetic, it being impossible to find a method that allows us to recognize as provable or refutable an arbitrary formula of this calculus. It may prove—indeed, in many cases it has already been shown—that fragments of these systems are decidable, but Hilbert's aim of a general technique which would banish ignorance from mathematics appears to be unattainable.
In demonstrating his theorem Church was obliged to provide a formal counterpart of the intuitive notion of effective calculability, and he proposed that this notion be identified with that of recursiveness. The notion of a recursive function (of positive integers) was introduced by Gödel, acting on a suggestion of Herbrand, and was analyzed in detail by S. C. Kleene. A function is said to be (general) recursive (a generalization of the notion of primitive recursive) if, roughly speaking, its value for given arguments can be calculated from a set of equations by means of two rules, one allowing the replacement of variables by numerals, the other allowing the substitution of equals for equals. As Church remarks, the intuitive status of effective calculability rules out any complete justification of his proposal (since known as Church's thesis), but he adduces reasons for regarding the identification as plausible, and the plausibility of his thesis has subsequently been reinforced by the discovery that despite their apparent dissimilarity, various alternative attempts to characterize the intuitive concept have all proved equivalent to that of general recursiveness.
Thus, at the time Church put forward his thesis the Church-Kleene notion of λ -definability was already known to provide an equivalent, and Turing's "computability," Post's "1-definability" and "binormality," and Markov's "computability" provide alternatives defined with respect to machines and combinatorial operations. It should be mentioned, however, that Church's thesis has not met with universal support; a summary and criticism of a number of objections can be found in Elliot Mendelson's "On Some Recent Criticism of Church's Thesis" (in Notre Dame Journal of Formal Logic 4 : 201–205).
Bede Rundle (1967)