[FOM] Proofs in Computability Theories

[Andrej Bauer]

On Thu, Sep 24, 2009 at 2:19 AM, Daniel Méhkeri <dmehkeri at yahoo.ca> wrote:
> 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).

Very interesting. I have never noticed it either  Here is the more
abstract "syntethic computability" version of your proof. Let Omega be
the set of truth values (the powerset of a singleton).
Let Sigma be the set of semidecidable propositions, i.e.,

 Sigma = {p in Omega | exists f : N --> {0,1}, (p <==> exists n:N, f(n) = 1)}

Notice that we allow _any_ f here, not just those computed by Turing
machines. Of course, since we work constructively, we cannot show that
there exist non-computable f's. Consider the statements:

(MP)  forall p : Omega, p in Sigma ==> not not p = p

(P) forall p : Omega, p in Sigma and (not not p) in Sigma => p or not p.

The first one is an (abstract) Markov principle and the second is an
(abstract) Post's theorem (I thought it was called that, but Herb
Enderton pointed out that Martin Davies attributes the theorem to
Kleene (1943), Post in (1944), and Mostowski (1947) independently).

We have MP ==> P: suppose p in Sigma and (not not p) in Sigma. Because
Sigma is closed under disjunctions we see that (p or not p) in Sigma.
Now beause of (MP)

  (p or not p) = not not (p or not p) = not (not p and not not p) =
not false = true.

We also have P ==> MP: suppose p in Sigma and not not p. Then not p =
false is in Sigma. Then by P we see that p or not p holds. But since
not not p holds this implies that p holds, and we are done.

Excellent.

Andrej Bauer