[FOM] Is current computability theory intuitionistic?
Antonino Drago
drago at unina.it
Thu Jun 20 17:03:01 EDT 2013
> 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
More information about the FOM
mailing list