[FOM] Proofs in Computability Theories

Antonino Drago drago at unina.it
Thu Sep 17 15:50:23 EDT 2009

```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

```