FOM: Pi^0_1 vs Pi^0_2: reply to Davis and Riis

[JOE SHIPMAN, BLOOMBERG/ SKILLMAN]

If a Pi^0_2 sentence of the form AxEy P(x,y) where P is a primitive recursive
predicate of x and y can be replaced by Ax P(x,f(x)) where f(x) is a primitive
recursive function, then we've certainly simplified the sentence down to Pi^0_1.
But there is no a priori reason to suppose that the least y such that P(x,y) is
bounded by a primitive recursive function of x.  In the case of, say, the
Poincare conjecture, you would need a result of the form "if a simplicial
3-manifold X and the 3-sphere have isomorphic subdivisions, the size of the
subdivision grows primitive recursively in the number of substitutions needed to
trivialize the standard presentation of the fundamental group of X".  But
innocent-looking problems can have non-primitive recursive growth. Two examples:
1) Can you add vectors from a given set together to make a path from a given
point in Z^n to the origin without leaving the 1st orthant?  (Hack and/or Rabin)
2) Theorem (Friedman) AkEn For any sequence s(1),...,s(n) drawn from {1,...,k}
there are i<j with s(i),...,s(2i) a subsequence of s(j),...,s(2j).  The growth
of n w.r.t. k has ordinal w^(w^w); this Theorem implies Pi^0_2 induction! -- JS