[FOM] Proofs in Computability Theories

[Andrej Bauer]

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

Could you please explain what you mean in the above paragraph, with
regards to the existence of the universal machine being proved ad
absurdum of the weak kind? I presume you are referring to the theorem
which says that there is a Turing machine which simulates all others.
The existence of such a machine is constructed very concretely, which
is why I am confused.

With kind regards,

Andrej Bauer