Can anyone point me to any proofs (pref. interesting ones!) that make good (or bad) use of the Finite or Infinite Priority Injury Argument?


**Edit:** I would suppose that my question could be put this way too. Are priority injury method proofs limited to recursion theory, or have they been used elsewhere?


Motivation: It's a technique that crops up a lot in recursion/computability theory, especially in the Friedberg-Muchnik theorem. As a development of normal Priority Arguments (set up by Kleene and Post), I wish to explore any interesting, or just additional, formulations.


As I said, I'm familiar with 'Movable Marker' proofs, and with 'Priority Method' proofs, and I'm looking for proofs that make use of the injury side of the method.


For those who are unsure; the priority injury method utilises the notion that for a set of requirements that we have to meet, $R\_{2e}$ for one side and $R\_{2e+1}$ on the other side of our computation, we define the 'use' of each side, and then choose a *witness* $x$ s.t. $A(x)\neq \Phi^B\_i (x)$, where $A$ and $B$ are the sets that we're trying to make incomparable in the Friedberg-Muchnik theorem. The key point is that we allow ourselves to finitely/infinitely *injure* the requirements that have been satisfied before so that we can satisfy a stronger requirement - it is *this* technique that I'm interested to see further examples of...


Any proofs considered!


With thanks, M.



Proofs that use Infinite/Finite Priority Injury Method
The original proof of Borel determinacy by Donald Martin (1975, Annals of Mathematics) used a priority argument; I haven't read that paper, but Martin cited the complexity of the original proof as a motivation in the paper where he published his second, "purely inductive", proof (1985, Proc. Sympos. Pure Math. 42). The second proof eliminated the priority argument. 


Note: the second paper was published in 1985, but was presented in 1982. 


