Proving Church's thesis (Q2701936)

The author argues against the traditional view that a proof of Church's Thesis (CT) is impossible. He repeats and supports the argument that CT has been proved in one direction (namely, that every recursive function is effectively computable), and he agrees (for example, with Shoenfield) that a proof in the other direction is conceivable (for example, by using suitable axioms for the notion of effectively computable function). He rejects recent arguments for the unprovability of CT by \textit{J. Folina} [ibid. 6, 302-323 (1998; Zbl 0916.03007)]. Her restriction to proofs in ZFC or some other standard axiom system stacks the deck against the provability of CT. The author points out that the notion of effectively computable function is not vague and can legitimately occur in mathematical proofs, although it does not occur in the standard axiom systems. This paper also contains an outline of an argument in favor of CT given by Saul Kripke (at a Logic Colloquium in Berlin in 1998), which seems to depend on the assumption that a function which can be shown to be computable within a first-order language must be recursive. Precise details of this argument are not given.