# FOM: The Church Thesis

V. Sazonov V.Sazonov at doc.mmu.ac.uk
Tue Jan 30 08:12:08 EST 2001

Comments of Alasdair Urquhart on CT seem to me
quite reasonable. I would only say that whatever
proof of CT we consider it will be just a proof of
equivalence of two mathematical notions (like
holomorphic functions = analitic ones.) "Eventually"
such things as CT are devoted to relate intuition
and formalization.

On the other hand, let us consider a version of
Bounded Arithmetic. Let me recall that exponential
is not provably total there. We can easily formalize
the notion of Turing machine in BA. No exponential
is needed for this. If to do everything sufficiently
carefully, then we can construct universal TM and
prove in BA all the usual properties of UTM such as
s-m-n property and therefore to prove the ordinary
fixed point (i.e., actually, recursion theorem).
Cf. my paper

"An equivalence between polynomial constructivity of
Markov's principle and the equality P=NP",
{\em Siberian Advances in Mathematics\/}, 1991, v.1,
N4, pp. 92-121 (This is English translation of a paper
in Russian published in Matematicheskaja logika i
algoritmicheskie problemy, Trudy Instituta matematiki
SO AN SSSR, 12, Novosibirsk, Nauka'', Sibirskoe
otdelenie, 1989, pp. 138--165.)

Thus, we have the notion of Turing computability in the
framework of BA, we can associate with it a corresponding
CT (even postulate a formal CT in the framework of an
intuitionistic version of BA), but we cannot say that 2^n,
as we understand it in the ordinary arithmetic, is computable.
It is only  *partial recursive*.

I am wandering, why CT is usually considered in an
absolute (Platonistic?) way without relating it to
any formal theory which fixes a framework where we
can speak on any (computable) functions at all.

Even in the framework of PA or ZFC the extent of the
class of (total) computable functions is different.
What can TM do depends on a corresponding theory.

Moreover, if consider a weaker theory than BA, something
like feasible numbers theory (cf. corresponding my paper
available via
http://www.doc.mmu.ac.uk/STAFF/V.Sazonov/papers.html),
then it is more difficult to say without special
investigation what may happen with TM and CT. Say, the
notion of computability may split and we probably will
have several versions of CT.

Finally, let me ask, what is the difference between
CT and any other situation when mathematicians found
a formalization of an informal concept (like continuity
in terms of epsilon-delta or topological space) and
assert a deep satisfaction concerning the relation
between intuition and its formalization? What is so
special here about CT? I think - nothing, expect our
special interest to computability rather than, say,
to continuity notion.