[FOM] Proofs in Computability Theories

[Aatu Koskensilta]

Quoting Antonino Drago <drago at unina.it>:

> I apologize. I was wrong in my last post: of September 17, 2009 9:50 PM,
> when I wrote:
>
>> 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.
>
> I instead intended to write as an example the halting problem of a Turing
> machine.

It's obscure what you have in mind. The usual proof of the  
unsolvability of the halting problem is perfectly constructive: it  
shows how to construct, for any given Turing machine H, an explicit  
witness of failure of H to solve the halting problem. For  
non-constructive theorems in recursion theory we need look elsewhere,  
ranging from the classically trivial result that a finite set is  
decidable to more interesting stuff about immune sets etc.

-- 
Aatu Koskensilta (aatu.koskensilta at uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus