[FOM] Proofs in Computability Theories
Aatu Koskensilta
Aatu.Koskensilta at uta.fi
Sun Sep 20 19:04:00 EDT 2009
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
More information about the FOM
mailing list