[FOM] Is current computability theory intuitionistic?

[Antonino Drago]

> Wednesday, June 19, 2013 3:58 AM  Arnon Avron  wrote
:
> As far as I can judge, the central issue in computability
> theory, Church Thesis (or Church-Turing Thesis),
> is meaningless from an intuitionistic point of view.

I remark that this Thesis is not meaningless from an intuitionist viewpoint.
(Incidentally, Why it is called thesis? Just
because it is not a theorem drwan from axioms, notwithstanding when it was
suggested someones tried to prove it).
It may be enounced through a doubly negated proposition, as Kleene did:
"Every general recursive function cannot conflict with the intuitive notion 
which is supposed to complete." [Introduction to Metamathematics, Van 
Nostrand, Princeton, 1952, p. 318-319; emphasis added]. This statement 
confirms what Martin Davis wrote the 19th:
<<In "Introduction to Metamathematics", Kleene is very careful to stick
to constructive proofs in his treatment of computability aka general
recursiveness.>>

The question about the computability theory is analogous to the question
whether there is a constructive version of classical mechanics.
In fact, a century after Newton's version of the inertia principle, Lazare 
Carnot
suggested a new version through a doubly negated proposition:
"Once a body is at rest it cannot move by itself; when in motion, it changes
neither its direction nor its speed" (Principes fondamentaux de l'équilibre 
et du
mouvement, Crapelet, Paris, 1802, p. 49). The operative nature of his 
principles have been remarked by the historians (R. Dugas: Histoire de la 
Mécanique, Griffon, Neuchatel, 1956, p. 309).
Indeed, Carnot dismissed also the "metaphysical" notion of cause-force, for
rather basing his theory on the principle of virtual velocities, which does 
not
necessarily make use of infinitesimal operations.
As a result, his basic equations make uise of either algebraic or 
trigonometric operations only; nevertheless they give for the first in the 
history
of theoretical physics the invariants of the motion (see my
paper:" A new appraisal of old formulations of mechanics", Am. J. Phys., 72 
(3)
2004, 407-99).
Incidentally, this fact shows that a formulation of a theory of the 
constructive kind may lead to gain in profundity and in innovation.

In conclusion, my answer to the question is that computability theory may be
translated in an intuitionist theory provided that one changes the versions
of his principles and moreover assumes a new radical viewpoint which
addresses the theory to solve problems rather than deduce theorems.
In the case of the computability theory, to solve the well-known two basic 
problems,
i.e. the Universal computing machine
and the halt problem
(For a similar theory, see A. and E. Drago: Information science as a
paradigmatic instance of a problem-based theory, in W. Hofkirchner (ed.):The 
Quest for an Unified Theory of Information, Gordon and Breach, London,1999, 
45-66).

Best greetings
Antonino Drago