[FOM] Finitistic Properties of High Complexity

[Dmytro Taranovsky]

The truth predicate for second order arithmetic refers to infinite sets, 
but it turns out that it can be expressed in terms of properties of 
certain natural finite structures, and hence it is arguably finitistic.  
Details, including a hierarchy of properties at different levels of 
expressiveness, are in my paper
http://web.mit.edu/dmytro/www/FinitismPaper.htm

but here I will describe the general approach and the interpretation of 
second order arithmetical truth.

The general strategy for these properties is the following:
- Intuitively define a notion using just finite numbers (without 
quantification over the totality of numbers, though one could argue that 
the quantification occurs indirectly).
- Give a formal definition using infinite sets.
- Argue that the intuitive and formal notions agree.
- Prove the complexity of the formal notion.

I intuitively define precise notions in a roundabout way:
- Give a vague notion A.
- Define a precise notion using A such that its definition does not 
depend on how the vagueness in A is resolved.

Argument that the intuitive notion agrees with the formal one:
* Express possible definitions of A using a directed system and show 
that for some choice A' every A'' that is at least as good as A' works.

First example:
Vague notion:  m is sufficiently large relative to n.
Precise notion: Define a Turing machine n to be halting (on the empty 
tape) iff it halts by time m, where m is sufficiently large relative to n.
Infinitary formal definition:  Turing machine n halts iff it halts at 
some finite time (note that quantification over all natural numbers is, 
from a computational perspective, a use of infinity).

Main system:  Truth predicate for second order arithmetic.
Vague notion:
A level 0 estimator is a pair (a, b) with b sufficiently large relative 
to a and the problem size.
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.

Precise notion:  The truth predicate for sentences in second order 
arithmetic is defined as follows:
* Use standard rules to convert the sentence to Q X_1 Q X_2 … E X_n Ax 
Ey>x P where n>0, each Q is a quantifier (A is 'for all' and E is 
'exists'), and P is a bounded quantifier formula that does not use x 
(and P can even be chosen to be polynomial time computable).
* Pick any (it does not matter which one) level n estimator on problem 
sizes at least as large as the sentence.  The sentence is true iff it 
passes the estimator.
* A formula Ax Ey>x P(y, ...) (P as above) passes a level zero estimator 
(a, b) iff Ey (a<=y<b) P(y, ...).
* A formula AX phi(X) passes an estimator iff for every binary sequence 
X, phi(X) passes at least one of the estimators included.
* A formula EX phi(X) passes an estimator iff for some binary sequence 
X, phi(X) passes all of the estimators included.
   (Note: Because P is bounded quantifier and an estimator is finite, 
the search over X is also finite).

To prove correctness, we first have to formalize what we want prove. If 
we treat 'sufficiently' as a parameter in the definition:
* A notion R of 0-estimators is valid iff (R(a,b) and c<=a and b<=d) ==> 
R(c,d) and Aa Eb R(a,b).
* A notion R of n+1 estimators is valid iff
      - For every valid notion S of n-estimators, there is an element of 
R consisting of elements of S.
      - There is a valid notion T of n-estimators such that every 
element of R consists of elements of T, and adding an element of T to an 
element of R results in an element of R.

Given two valid notions R and S of n-estimators, R intersect S can also 
be shown to be a valid notion.  A sentence using an n-estimator as a 
parameter is well-defined iff there is a valid notion R such that all 
elements of R agree on whether the sentence is true, which is then the 
truth value of the sentence.  One then proves (see my paper) that the 
above notion of second order arithmetical truth is well-defined and 
agrees with the actual truth.

An interesting project would be to develop the theory of n-estimators, 
and in this way, connect the infinite to the finite.  For example, 
projective determinacy plays a central role in second order arithmetic, 
and we would want to naturally express it using finite structures and 
understand its combinatorial content.

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