FOM: Church's Thesis Research

[Harvey Friedman]

Vorobey 2:58AM 11/8/98 wrote:

>First, the Thesis itself:
>
>   Church's Thesis. Every effectively computable function
>   is recursive.
>
>It's important to distinguish between two uses of the Thesis. It's
>often used in a relatively unimportant way: instead of formally
>defining a Turing machine or a lambda-calculus term etc. computing
>a certain function, we show why it's "obviously" effectively computable,
>often by sketching an informal algorithm. When we then conclude that
>it's really recursive, we're using the Thesis, but in an inessential
>way: all such "shortcuts" can in practice be replaced by strict
>formalization which is usually straightforward, though tedious.

An interesting question is: what is the status of your claim that "all such
"shortcuts" can in practice be replaced by strict formalization which is
usually straightforward, through tedious"? Is your claim a weak form of
Church's Thesis in the form you quote here, or is it equivalent to Church's
Thesis in the form you quote here? To put it differently, can you designate
something special about the kind of informal algorithm that is typically
sketched, which might be more obviously recursive than an arbitrary
"effectively computable function"?

>The essential use of the Thesis, on the other hand, is when we
>declare a problem _unsolvable_ (or the function _uncomputable_)
>on the basis of its being _non-recursive_.

This suggests some modified Church's Theses. E.g.,

every effectively computable function is recursive in 0'.
0' is not recursive in the graph of any effectively computable function.
every effectively computable function is of smaller Turing degree than 0'.

What is their status as compared to the usual, strong Church's Thesis?

>The Thesis, as stated, is ambigious in several ways. First of all,
>instead of formulating it for functions, one may formulate a
>(possible stronger) version, which Kreisel calls
>
>   Superthesis: Every effective *rule* is intensionally equivalent to
>   a program for an idealized computer (say, a Turing machine).
>
What is the best explanation you know of "intesnsional equivalence" for
this purpose?

>Even though we no longer believe that the world around us works
>according to the laws of classical mechanics (with or without
>relativity; what matters here is determinism), these laws do provide
>excellent approximation in most cases; furthermore, it's an easier
>case (to argue Thesis's truth in) and deserves to be treated separately.
>
>We thus define
>
>   Thesis M (for 'mechanical'): The behavior of any discrete physical
>   system evolving according to local mechanical laws is recursive.
>
A fascinating possibility is afforded by a "nonlocal" application of
Newton's inverse square law. E.g., let a finite number of distinct
positions in R^3 be specified with rational coordinates, and let a mass be
assigned to each such point as a rational number > 0. Also let a time
interval [0,t] be specified where t is a rational number > 0 or t =
infinity. Now assume that the inverse square law is acting. Is there a
collision within the time interval? I.e., is there an algorithm for
deciding this question?

>   Thesis C (for 'constructive'): Any constructive function is
>   recursive.

>The conclusion we have for Thesis C is that
>
>  we have collected very weak, and certanly inconclusive, evidence
>  in favor of Thesis C, and its validity must therefore remain
>  as unproved (which isn't surprising given the fact that we only
>  have a very partial grasp of what 'constructive' means).

My own view is that the real problem at this time is:

what should research on CT (all forms) look like?

Of course, research into the recursiveness of models of extramathematical
phenomena is clearly valuable - and perhaps in some cases extremely
difficult. E.g., the questions about many body problems stated above.

I think it is reasonably likely for there to be an unusually and
unexpectedly surprising and compelling characterization of the recursive
functions that will make it obvious in hindsight that continued persistent
and painstaking research on CT (various forms) is an important enterprise.
E.g., there is an ongoing research program led by Sieg at CMU/Phil, which
would be nice to flesh out on the FOM.