Proofs that use Infinite/Finite Priority Injury Method

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.

-
Do you have access to Robert Soare's Book on R.E. Sets and Degrees? There may be a later and better treatment, but I doubt it. Gerhard "Ask Me About System Design" Paseman, 2011.06.15 – Gerhard Paseman Jun 15 '11 at 23:58
(1) I am not a specialist in the field, and I am not aware of any writing of Post or Kleene on what you call "normal Priority arguments"; could you please specify a source? (2) there is a LARGE literature on priority arguments, with all sorts of results, part of which are included in the Soare text mentioned by Paseman in his comment above, so your question does not strike me as sufficiently focused. – Ali Enayat Jun 16 '11 at 1:24
Ali, my impression is that the question comes with no research done. I suspect ((you will get a cogent answer to your question above) iff (the poster is familiar with Soare's book)). Gerhard "Was Young And Inexperienced Once" Paseman, 2011.06.15 – Gerhard Paseman Jun 16 '11 at 2:32
As Gerhard mentioned, the classical reference for this is Robert Soare's Recursively Enumerable Sets and Degrees (Perspectives in Mathematical Logic, Springer-Verlag, 1987). Note that Soare will eventually publish a new book to replace this one - people.cs.uchicago.edu/~soare/cta – François G. Dorais Jun 16 '11 at 5:13
You may also enjoy these notes math.uconn.edu/~lerman/GFposet.pdf by Manny Lerman. However, be aware that Lerman's goal in these notes is to go well beyond infinite injury, so you may find the learning curve very steep. In a similar vein, Stephen Lempp has some notes and other material - math.wisc.edu/~lempp/papers/prio.pdf - math.wisc.edu/~lempp/papers/list.html#prio – François G. Dorais Jun 16 '11 at 5:14

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.

-
I agree with Carl that an important part of Martin's original proof of Borel Determinacy looks like a priority argument, but (if I remember correctly) Martin himself once told me that he didn't think of it that way. – Andreas Blass Jun 16 '11 at 13:44
Thanks for the info. I was basing my comments on Martin's remarks in the first paragraph of his 1985 paper, where he describes the original argument as a priority argument. But I may be taking that intro paragraph out of larger context, and I'm not familiar with the original argument at all to comment on it. – Carl Mummert Jun 16 '11 at 14:01
Many thanks! I shall look it up! – user15756 Jun 16 '11 at 22:40

One of my favorite applications is Leo Harrington's proof that a computable differential field has a computable differential closure. This is the only proof I know that the differential closure of the constant field of rationals is computable.

-
@Dave: could you please provide a reference for Harrington's proof? – Ali Enayat Jun 17 '11 at 2:44
@Ali, the paper is Harrington, Leo Recursively presentable prime models. J. Symbolic Logic 39 (1974), 305–309. He gives necessary and sufficient conditions for a complete decidable theory to have a decidable prime model. The proof is a finite injury priority argument. – Dave Marker Jun 17 '11 at 13:15
@Dave: Thanks for the reference. – Ali Enayat Jun 17 '11 at 13:38

I've heard of priority arguments being used in complexity theory. See this blog post for example.

-
Many thanks @Quinn.Culver - that post looks interesting! Answers the question as I had hoped. The use of random strings and oracles is unusual - not something I had thought of in the way they write. Additionally, the comments are interesting (and quite philosophical at points). – user15756 Jun 16 '11 at 12:44