FOM: Re: Simpson on Soare on Harrington

[Leo Harrington]

	Simpson is correct about about the result on
the existence of an omega-model of boldface Sigma^1_1 choice in which 
lightface Sigma^1_1 dependent choice fails.
	It is due to Friedman.

	The confusion here is due to me (Harrington); I mistakenly mentioned
the above result to Soare as an example of the interplay between
forcing and priority arguments which can transfer boldface examples 
into lightface ones. Apparently Soare then consulted Steel who very
collegially went along with my misattribution. I was induced to mention
the result to Soare since I too was startled by Simpson's claim that
there was no connection between priority arguments and fom.

	As I now recall, the above mentioned result was proved by
Friedman using Godel`s theorem on consistency proofs (in omega-logic).

	The example I was actually thinking of was (I now think)
the result that boldface Delta^1_1 comprehension does not imply
lightface Sigma^1_1 choice. (I've now had a chance to see some
of the correspondence on this, and it is this result that Steel
mentions).

	A proof of the boldface version of this (and up till now
what I had thought to be the first proof of the boldface version) 
was due to Steel using his forcing. I then converted that into the above 
lightface version using Sacks' shiny little box and priorty arguments. 
(A similar method could be used to prove the above mentioned result
of Friedman - I think this is why I and then Steel got the results
muddled).

	I gather from Simpson`s comments that this result (an
omega-model of boldface Delta^1_1 comprehension in which lightface
Sigma^1_1 AC fails) had been proved earlier.

	I apologize for calling up all this confusion.



	But since I have been induced to start to write something I might as
well continue a bit.

	(1) Another result which I thought used priority arguments
and the shiny little box is:

	Let B = Baire space. 
	For all countable ordinals a, there is a closed binary relation R 
of B such that for all x in B the set {y | <x,y> is in R} is non-empty and
countable (in fact of size two) such that for all Borel functions f which
uniformize R, (ie for all x in B <x,f(x)> is in R), the graph of f does not 
have Borel rank less than a.

	Does anyone know if this result is already in the literature? 


	(2) I noticed that the Gurevich-Harrington proof of the
Rabin S2S decidability result has been mentioned in the context of
priority arguments. I personally never thought about it in those terms:
	Some of the manipulations of the Buchi automata might be vaguely
similar to priority arguments since Buchi automata have outputs depending 
on what happens infinitely often, but this would seem to be stretching things
alot.
	Also, the proof with Gurevich relies on determinacy, in particular
determinacy of boolean combinations of Pi^0_2 sets. Now I think (although
I have a tendency to be wrong often enough when I do that) but I think that
Martin himself thought that his proof of Borel determinacy was suggestive
of the priority argument technique; but in our S2S proof Gurevich and I
relied on the pre-Martin proof of Pi^0_2 determinacy, so again I don't
see priority arguments there.
	And going to the source, Rabin: although Pi^0_2 determinacy is 
expressible as a sentence in the language S2S and although Rabin did 
produce a decision proceedure for that language, I don't see that he 
ever applied his decision proceedure to that sentence, or did anything
suggestive of priority arguments. 


	(3) I would though in conclusion like to point out that the
method of priority arguments is at least one way to convert 
a bunch of competing and conflicting and demanding requirements into
a bunch of competing and conflicting and demanding requirements that
actually achieve a coherent common goal. The key is to ensure that
all the requirements, no matter how strong or how weak, no matter
how ridiculous or wrong or false or bad they look to each other,
that all requirements respect each other in their contributions
toward the coherent common goal.
	And so, to return to foundations, what is the common goal?
	What is the common goal of fom? (or FOM, or f.o.m.; when I think
I get such things confused).

	Leo Harrington