Friedberg–Muchnik theorem (source code)

= Friedberg–Muchnik theorem
{c}
{wiki}

There are <computably enumerable sets> $A,B$ with $A\not\leq_TB$ and $B\not\leq_TA$. A <finite-injury priority construction> alternates requirements preventing oracle programs for $B$ from computing $A$ and programs for $A$ from computing $B$. Each requirement uses a private witness, enumerates it when the opposing computation gives zero, and restrains the oracle segment preserving that disagreement. Verification inducts on priority. Both degrees are noncomputable and strictly below the halting degree, resolving <Post problem>.

The incomparable-degree formulation is stated in https://people.math.wisc.edu/~slempp/papers/prio.pdf[Steffen Lempp's notes, section 1.1].