[FOM] Proofs in Computability Theories

[Antonino Drago]

Steve Stevenson" <steve at cs.clemson.edu> wrote:

> In class the other day, a question arose about intuitionism and
> computability. I would appreciate views on these two aspects:
> 1. Shouldn't the study of computability be constructive - thinking of
> Markov,

1. The attitude to enlarge the study of computability by means of principles
including actual infinity (e.g. the pigeon-hole principle) is like to bluff
in a poker game: it may result in either a useful generalization or in an
idealisation without reference to reality; hence in an illusory more
powerful theoretical search. The dilemma may be solved after a very long
sequence of consequences. Hence, it would be bstter for pupil to adhere to
reality as much as possible, without what at a first glance seems a trick

>and
> 2. Shouldn't the proofs therefore be intuitionistic?

2. Historically, the study of computability is based upon not axioms but a
general problem, which traditional scientific methods were unable to solve:
What is computable? The situation is similar to the traditional
thermoduynamics, born on the problem: what part of heat is reducible to
work? Both theories studies machines.
Like thermodynamic Carnot' theorem, the main theorems of compuatbility
theory (e.g. the existence of the universal machine) are ad absurdum
theorems of the weak kind, i.e.. by concluding trough no more than a double 
negated sentence belonging to intuitionistic logic..
But at present this uncommon way of arguing is disregarded, although
it leads in an efficient way to important conclusions, likely in Carnot's 
thermodynamics and in some other scientific theories (I wrote papers on the 
subject).
In conclusion, all the proofs should be ad absurdum proof belonging to 
intuinistic logic, till up to solve in an universal way (for all machines) 
the general problem motivating th theory. After that, the cpnclusion is 
translated in the correpsonding positive sentence and it may work as the 
hypothesis of the following deductive development. In this way argued both 
Sadi Carnot and also Lobachevsky in Untersuchungen... 1840.
Best regards
Antonino Drago