FOM: Prioirty arguments necessary?

[Harvey Friedman]

Are there formal criteria associated with the necessity of using a priority
argument to prove a theorem?

There seem to be at least two interesting, natural, and relevant formal
criteria.

1. Through Proof Theory/Reverse Mathematics.

It appears that priority arguments cannot be done in the fairly strong
theory ISigma_1 (i.e., Sigma_1 induction). This is credited to C.T.Chong
and K.M. Mourad, Sigma_n definable sets and Sigma_n induction, TAMS (334),
1992, no. 1, 349-363.

This reference and many others are present in the state of the art preprint

 C. T. Chong, Lei Qian, T. Slaman, and Yue Yang, Sigma_2 Induction and
Infinite Injury Priority Arguments, Part III: Prompt Sets, Minimal Pairs
and Shoenfield's Conjecture, Israel Journal of Mathematics, to appear.

obtainable from the website

http://www.math.berkeley.edu/~slaman/papers/chong-etal.pdf

There is a substantial investigation into independence results and
reversals (in the sense of Reverse Mathematics) here, where the reversals
are especially difficult to come by.

Now it also appears that just about everything in the recursion theory of
r.e. sets and partial recursive functions that doesn't need a priority
argument is provable in ISigma_1. And perhaps even less. Even here, it
would be interesting to use, say, ISigma_0(exp) as a base theory and
perhaps derive ISigma_1 from some elementary recursion theoretic
statements, or show that this cannot be derived. (There may be some
spadework to show that a system like ISigma_0(exp) is completely suitable
as a base theory for this. PRA (primitive recursive arithmetic) is another
natural choice, although it has the disadvantage of being somewhat
stronger.

So here is a suggestion.

When people claim that something or other can be done without a priority
argument, that they strive to provide a proof in ISigma_1 or perhaps even
less.

When people claim that something or other cannot be done without a priority
argument, that they strive to show that there is no proof in ISigma_1.

2. Through Intuitionism.

It appears that the just about everything in the recursion theory of r.e.
sets and partial recursive functions that doesn't need a priority argument
is provable in HA = Heyting arithmetic. One can also maintain that this is
true for intuitionistic ISigma_1 or perhaps even less.

On the other hand, it appears that priority arguments cannot be done in HA.

So here is another suggestion.

When people claim that something or other can be done without a priority
argument, that they strive to provide a proof in HA, in intuitionistic
ISigma_1 or perhaps even less.

When people claim that something or other cannot be done without a priority
argument, that they strive to show that there is no proof in HA.

To be sure, an investigation of recursion theory of r.e. sets and partial
recursive functions from the standpoint of HA will require a lot of
spadework about constructive formulations, but this should be interesting
and informative.

3. Final remarks.

Perhaps some subscribers will show me some cases where these criteria break
down. I just was thinking of some very standard situations like:

a) recursively inseparable r.e. sets;
b) all creative sets are recursively isomorphic (Myhill);
c) Turing incomparable r.e. sets (Friedberg);
d) Friedberg enumeration theorem.

By the way, has d) been analyzed metamathematically?