[FOM] Projective Determinacy and Finite Structures

[Dmytro Taranovsky]

Can projective determinacy be interpreted as a natural property of 
natural finite structures?  Here, I present a plausible yes answer.

This and many other results are in my paper "Finitistic Properties of 
High Complexity"
http://web.mit.edu/dmytro/www/FinitismPaper.htm

Definition:
A level 0 estimator is a pair of natural numbers (a, b) with 'a' 
sufficiently large, and 'b' sufficiently large relative to 'a'.
A level n+1 estimator is a sufficiently complete finite set of level n 
estimators, where 'sufficient completeness' is defined such that it does 
not prevent the notion of level n estimators from being arbitrarily strict.
(Sufficiency depends on the problem/calculation considered.)

On the one hand, the definition intuitively makes sense as a finite 
definition, and the resulting sets are natural as finite structures.  
The 'arbitrarily strict' qualifier is necessary because the notion of a 
level 0 estimator (as a specific notion as opposed to an ideal) is vague 
or dependent on the problem, so it should not be an error to be on the 
safe side and construe the notion more strictly, and the definition 
reflects that.

On the other hand, the use of 'sufficiently' presents an obstacle to 
formalizing uses of this definition.  Still, there is a unique preferred 
formalization of this definition, the catch being that the formalization 
has the same expressiveness as second order arithmetic.  See my paper 
for details and proofs, but basically I use a directed system of valid 
notions of estimators with each level adding a second order quantifier.

A key intuition is that even an arbitrarily high completeness of a level 
k+2 estimator cannot negate completeness of level k+1.  We build on this 
by naturally choosing a game (or a class of games) that pits level k+1 
completeness against level k+2 completeness, and the resulting assertion 
(in its strong form) is equivalent to projective determinacy.  In part 
(b), the use of Z simulates a second order infinite quantifier; this 
construction also works for other formulas.  Also, there is a single 
universal P sufficient for the theorem.

Theorem:
(a) Lightface projective determinacy holds iff for every k>0 and every 
primitive recursive (equivalently, elementary time) predicate P(n,X,Y) 
(X, Y and (below) Z are predicates on natural numbers, and by virtue of 
the bounds in P, can be treated as bounded sets and thus the game 
constructing X and Y is finite), for some (equivalently, every) level 
k+2 estimator s (sufficiently good relative to P), one of the players 
has a winning strategy in the following game:
player I - X_0, player II - Y_0, player I X_1, player II Y_1, ...
Player I wins iff forall s_{k+1} in s thereis s_k in s_{k+1} such that 
P(s_k,X,Y).
Player II wins iff forall s_{k+1} in s thereis s_k in s_{k+1} such that 
not P(s_k,X,Y).
(b) Projective determinacy holds iff for every k>0 and every P(n,X,Y,Z) 
(as above), for some (equivalently, every) level k+3 estimator t 
(sufficiently good relative to P), for every Z, there is s in t such 
that one of the players has a winning strategy in the above game (using 
P(s_k,X,Y,Z)).

Note that the theorem is an *equivalence* and not just an 
equiconsistency.  However, we also want an equiconsistency with a simple 
intuitive axiomatization of estimators that does not use infinite sets.  
It appears that the following axiomatization works.

A k-n-estimator will be an k-estimator sufficiently good relative to n.  
We idealize 'sufficiently good' with a schema such that if the schema is 
cut off at any finite point, there are particular notions consistent 
with the axioms.  An alternative would be to explicitly adjust n based 
on the formula size (and in the axiom 7 and definition of explicitly 
invariant below, use a number coding the subformula, the free variables, 
and k in place of max(x_2,...,x_i)).

We start with arithmetic, and add a predicate for k-n-estimators, with 
one predicate symbol per k.  An alternative to a predicate would be a 
function: n -> example of k-n-estimator, and application of basic 
closure operations would lead to a predicate consistent with the 
axioms.  Also, with some added complexity, one can axiomatize a single 
example of a k-n-estimator and using minimal arithmetical axioms.

Definition: A formula is explicitly invariant if all of its uses of 
k-n-estimators are in the form  thereis s (s is k-n-estimator) ... where 
n is the maximum of the free variables (not including s) at that 
location of the formula, and k is a numeral.  Finite sets will be coded 
by numbers (using any reasonable coding).
Note: The intent is that by virtue of its syntactic form, the formula is 
independent of how strictly we construe 'sufficiently complete'.

Language: arithmetic (using natural numbers), with predicates for 
k-n-estimators, with one predicate symbol per k>=-2.
Axioms:
1. Basic arithmetical axioms.
2. Induction for all formulas. [note: limited induction likely also works]
3. Every number is a -2-n-estimator [note: we use -2 rather than 0 so 
that 0-estimators will the same expressiveness (but different form) as 
above].
4. A k+1-n estimator is a finite set of k-n-estimators.
5. Adding a k-n-estimator as an element to a k+1-n-estimator results in 
a k+1-n-estimator.
6. Every k-n+1-estimator is a k-n-estimator.
7. (schema over explicitly invariant phi(x_1,...,x_i)) whether thereis 
s' subset s such that phi(s',x_2,...,x_i) holds is independent of the 
choice of the k-max(x_2,...,x_i)-estimator s.
8. For every n, a k-n-estimator exists.

Axiom 7 (combined with axioms 4 and 5) simply asserts that s is 
sufficiently complete as tested using phi and x_2,...,x_i.

I conjecture that the axioms are equiconsistent with second order 
arithmetic Z_2, and that the addition corresponding to the above theorem 
(using a schema over P, or a quantifier over codes and 
k-code(P)-estimators, or even a single universal instance) is 
equiconsistent with Z_2 + lightface projective determinacy for (a) and 
Z_2 + projective determinacy for (b).

Sincerely,
Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm