FOM: The Church Thesis

[V. Sazonov]

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. 


Vladimir Sazonov