[FOM] Projective Determinacy and Finite Structures
Dmytro Taranovsky
dmytro at mit.edu
Fri Jul 14 21:43:17 EDT 2017
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
More information about the FOM
mailing list