[FOM] Proofs in Computability Theories

[Andrej Bauer]

The simplest satement in recursion theorem which I do not know how to
prove (purely) constructively is Post's theorem: if both a set and its
complement are c.e. then the set is decidable. As far as I can tell,
the proof requires Markov principle (or something slightly weaker).
Markov principle is a particular instance of the general classical
principle Reductio ad Absurdum (not not p implies p).

With kind regards,

Andrej

On Mon, Sep 21, 2009 at 1:04 AM, Aatu Koskensilta
<Aatu.Koskensilta at uta.fi> wrote:
>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.