Finite-injury priority construction

A finite-injury priority construction orders countably many requirements so that each has finitely many predecessors. A strategy may discard lower-priority strategies' current witnesses and restraints when it acts. If each requirement acts finitely often after its last such initialization, induction on priority shows that every requirement is injured only finitely often and eventually has a stable strategy. The Friedberg–Muchnik theorem is a central example.

To prevent a Turing functional ${\Phi }_e^B$ from computing the indicator function of an enumerated set $A$, reserve a permanently unique fresh witness $x$. On observing a convergent computation with oracle use $u$, enumerate $x$ into $A$ if the answer is zero; otherwise keep it out. Restrain subsequent lower-priority enumerations into $B$ below $u$. Higher-priority actions may initialize this strategy and retire its witness, but witnesses are never reused. In a finite-injury priority construction, mathematical induction on priority shows that the final computation, if observed, remains correct as a computation from the final oracle and disagrees with $A$ at $x$. If no computation is ever observed after the final initialization, the final oracle computation diverges, since any convergent computation uses only finitely many eventually stable oracle bits.

There are computably enumerable sets $A,B$ with $A/{\le }_{T}B$ and $B/{\le }_{T}A$. 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 Steffen Lempp's notes, section 1.1.

An injury discards a strategy's current witness or restraint when a higher-priority action changes its assumptions. Finite injury means that each strategy experiences only finitely many such resets. The final uninjured strategy must still be checked to satisfy its requirement; finite injury alone is not the conclusion.