[FOM] Proofs in Computability Theories

[Daniel Méhkeri]

[My apologies to the moderator for the total lack of 
clarity in the previous version of this post. I've
highlighted the statement in question and hopefully 
clarified the proof.]

Andrej Bauer writes:

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


It occurs to me that:

 (*) If both a set and its complement are c.e.,
     then the set is decidable

(is that really Post's theorem?) cannot be proven from 
anything weaker, because it *IS* Markov's Principle. 
In fact now that I see it, I'm surprised MP isn't just 
stated that way, because it seems to me a lot more elegant 
and pronounceable than the double negative (and surely I'm 
not the first to have noticed this equivalence).

Proof:

Of course, if a set and its complement are c.e.,
then to decide membership, do an unbounded search of both
until the number in question is found. MP asserts that
the search must terminate, so the set is decidable. 
So (*) holds.

For the reversal, let R be a decidable relation between 
natural numbers, and suppose that there exists no x for which 
there exists no y such that x R y. (Which is equivalent 
to: for all x, double-negative-there-exists some y 
such that x R y, the usual antecedent of MP.)

Let Q = { x | there exists some y such that x R y }
Then N\Q = { x | there exists no y such that x R y }
By hypothesis N\Q is empty. By itself this doesn't 
constructively establish that Q=N. 

But, clearly Q is c.e., and so is its complement (the empty set),
so (*) asserts Q is decidable. This does allow us to conclude Q=N.

So, for all x there exists some y such that x R y. 
We've eliminated the double-negative. That's MP.

(There's a minor technicality about c.e. and empty set, but it
doesn't affect the result.)
 
Best regards,
Daniel

-- 



      Découvrez les photos les plus intéressantes du jour.
http://www.flickr.com/explore/interesting/7days/