Hostname: page-component-78c5997874-s2hrs Total loading time: 0 Render date: 2024-11-17T18:22:13.207Z Has data issue: false hasContentIssue false

Church's thesis without tears

Published online by Cambridge University Press:  12 March 2014

Fred Richman*
Affiliation:
New Mexico State University, Las Cruces, New Mexico 88003

Extract

The modern theory of computability is based on the works of Church, Markov and Turing who, starting from quite different models of computation, arrived at the same class of computable functions. The purpose of this paper is the show how the main results of the Church-Markov-Turing theory of computable functions may quickly be derived and understood without recourse to the largely irrelevant theories of recursive functions, Markov algorithms, or Turing machines. We do this by ignoring the problem of what constitutes a computable function and concentrating on the central feature of the Church-Markov-Turing theory: that the set of computable partial functions can be effectively enumerated. In this manner we are led directly to the heart of the theory of computability without having to fuss about what a computable function is.

The spirit of this approach is similar to that of [RGRS]. A major difference is that we operate in the context of constructive mathematics in the sense of Bishop [BSH1], so all functions are computable by definition, and the phrase “you can find” implies “by a finite calculation.” In particular if P is some property, then the statement “for each m there is n such that P(m, n)” means that we can construct a (computable) function θ such that P(m, θ(m)) for all m. Church's thesis has a different flavor in an environment like this where the notion of a computable function is primitive.

One point of such a treatment of Church's thesis is to make available to Bishopstyle constructivists the Markovian counterexamples of Russian constructivism and recursive function theory. The lack of serious candidates for computable functions other than recursive functions makes it quite implausible that a Bishopstyle constructivist could refute Church's thesis, or any consequence of Church's thesis. Hence counterexamples such as Specker's bounded increasing sequence of rational numbers that is eventually bounded away from any given real number [SPEC] may be used, as Brouwerian counterexamples are, as evidence of the unprovability of certain assertions.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1983

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[ABER]Aberth, O., Computable analysis, McGraw-Hill, New York, 1980.Google Scholar
[BEES]Beeson, M., The non-derivability in intuitionistic formal systems of theorems on the continuity of effective operations, this Journal, vol. 40 (1975), pp. 321346.Google Scholar
[BSH1]Bishop, E., Foundations of constructive analysis, McGraw-Hill, New York, 1967.Google Scholar
[BSH2]Bishop, E., Schizophrenia in contemporary mathematics, American Mathematical Society Colloquium Lectures, Missoula, Montana, 1973.Google Scholar
[CEIT]Ceitin, G.S., Algorithmic operators in constructive metric spaces, American Mathematical Society Translations, vol. 64 (1967), pp. 180.Google Scholar
[FRDM]Friedman, H., Axiomatic recursion theory, Logic Colloquium 69 (Gandy, R. and Yates, M., Editors), North-Holland, Amsterdam, 1971, pp. 113137.CrossRefGoogle Scholar
[MARK]Markov, A.A., On constructive functions, American Mathematical Society Translations, vol. 29 (1963), pp. 163195.Google Scholar
[MAYO]Machtey, M. and Young, P., An introduction to the general theory of algorithms, North-Holland, Amsterdam, 1978.Google Scholar
[RGRS]Rogers, H., Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967.Google Scholar
[SHNN]Sanin, N.A., Constructive real numbers and function spaces, American Mathematical Society Translations, vol. 21 (1968).Google Scholar
[SPEC]Specker, E., Nicht konstruktiv beweisbare Sätze der Analysis, this Journal, vol. 14 (1949), pp. 145158.Google Scholar