[FOM] 177:Strict Reverse Mathematics 1

[Harvey Friedman]

It has been slowly dawning on me that it IS possible to do reverse 
mathematics perfectly, without compromise - although I am fully 
confident about this so far only in the context of finite 
mathematics. Nevertheless, this will take us up to the proof 
theoretic level of impredicative systems.

Incorporating infinite objects with this level of perfection is going 
to need some major ideas. What I have presently in mind doesn't reach 
this level of perfection.

Given the approach taken here in this posting, let me put the work in 
the last posting, 175, in context. There I was trying to do my best 
staying strictly in the language of ordered rings. It would be very 
interesting to see how this can be improved on.

Note that I changed the name from "honest reverse mathematics" to 
"strict reverse mathematics".

#######################

We go beyond the language of ordered rings by adding finite sequences 
of ring elements.

We will have two sorts, one for integers, one for finite sequences of 
integers. We have the usual 0,1,+,-,x,< on integers. We have 
lth(alpha) for the length of the finite sequence alpha, and alpha(i) 
for the i-th term of alpha. We count from 1 through lth(alpha). If we 
want to keep this in a standard two sorted system of first order 
logic without undefined terms, then we would merely remain agnostic 
about the value of alpha(i) if 1 <= i <= lth(alpha) is false. Also, 
we would not have = between sequences, but of course have it between 
integers.

We now state the axioms semiformally..

1. DOR. Discrete ordered ring axioms.
2. If alpha,beta are finite sequences of the same length, we can add 
and multiply alpha,beta termwise.
3. Constant sequences of any length exist.
4. The sequence 1,2,...,n exists for any n >= 0.
5. Concatenation. Let alpha,beta be finite sequences of lengths 
n,m >= 0 respectively, and let r >= 1. We can form the sequence 
alpha,beta,beta,...,beta, where there are r beta's. I.e., there is a 
finite sequence gamma of length n+rm whose i-th term, 1 <= i <= n, is 
the i-th term of alpha, and whose n+jm+k-th term, 1 <= j <= r, 1 <= k 
<= m, is the k-th term of beta.
6. Removal. Let alpha,beta be finite sequences. There is a finite 
sequence which lists the terms in alpha that are not in beta in 
strictly increasing order.

In 6, we don't need to assert anything about uniqueness.

1-6 outright implies IDelta0(Z,...). I.e., bounded induction with 
respect to the extended language above. However, bounded induction 
for formulas with quantification over, say, all finite sequences from 
[1,n] of length n, is not allowed.

We can also handle IDelta0(Z,exp,...). I.e., bounded induction with 
respect to the extended language above but with exponentiation added.

7. For all a,b >= 0, a^0 = 1 and a^b+1 = (a^b)a.

8. For all a,b >= 0, there is a finite sequence of length b whose 
i-th term is a^i,

1-8 proves IDelta0(Z,exp) outright, and in fact also proves bounded 
induction in the extended language. Also, the reverse is true, so 
that we have equivalence with IDelta0(Z,exp,...).

With regard to axiom 5. Clearly when one studies the semigroup in k 
generators, one wants to construct alpha(beta^n). That is normally 
rigorously supported by 5. Of course, one can go further than I have, 
and try to weaken 5 through introducing concatenation as a primitive, 
as well as beta^n. All this is done without considering the indices 
as in 5.

Although I think that 1-6 and 1-8 are sufficiently "perfect" to 
support Strict Reverse Mathematics, obviously one can appropriately 
get quite interested in being even more minimal about this than I 
have. The previous paragraph is just an example of such an 
investigation.

What I like very much about the move to finite sequences of integers 
is the following.

Recall my block subsequence theorem from
H. Friedman, Long Finite Sequences, Journal of Combinatorial Theory, 
Series A 95, 102-144 (2001).

"Fix k >= 1. In any sufficiently long finite sequence x from 
{1,...,k}, some consecutive block x[i],...,x[2i] is a subsequence of 
some later consecutive block x[j],...,x[2j]."

This is provable in 3 quantifier arithmetic but not in 2 quantifier 
arithmetic, and the associated growth rate lies just beyond the 
multiply recursive functions.

9. Block Subsequence Theorem.

9 is trivially and naturally stated in the language 1-6.

We can prove that the system 1-6 + 9 cannot be proved consistent in 2 
quantifier induction. We don't even need axioms 7,8 for this result.

In fact, 1-6 + 9 is equivalent to IDelta0(Z,...) plus the 
formalization of "every multiply recursive function is total".

Also, 1-6 + 9, 1-9, and 2 quantifier induction prove the same 
sentences in the language of ordered rings.

What is the best way to get even stronger systems? The Paris 
Harrington theorem requires use of sets of subsets of {1,...,n}. So 
this requires a little finesse since we have to expand the language 
and make sure that we support bounded induction with respect to the 
new language.

Better is to use Kruskal's theorem. Here, though, we must use my 
finite forms. The state of the art finite form is given in

H. Friedman, Internal finite tree embeddings, Reflections on the 
Foundations of Mathematics: Essays in honor of Solomon Feferman, ed. 
Sieg, Sommer, Talcott, Lecture Notes in Logic, volume 15, 62-93, 
2002, ASL.

This requires the expansion of the language to labeled finite trees, 
and needs to be thought through.

It would also be valuable to do this for the original Kruskal 
theorem. However, the original Kruskal theorem involves infinite 
sequences of finite trees. Obviously, this has no strength at all 
unless we have a way of proving that there are a reasonable variety 
of infinite sequences of finite trees.

But we can try to get around this problem as follows. We will take 
weak Konig's Lemma as an axiom. I.e., a finitely branching tree with 
no infinite paths is finite.

There are obvious finitely branching trees that we want to apply this 
to. Fix k >= 1. The tree of all finite sequences of finite trees, the 
i-th term having at most k+i vertices, for which no term is Kruskal 
embeddable into a later term.

I showed that if these trees is finite then we get the 1-consistency 
of ATR and beyond, and so we have impredicativity.

However, the problem is: how do we prove that this finitely branching 
tree exists?

We need some fundamental way of constructing such trees using only 
strictly mathematical axioms. It is not yet clear how to do this.

But the finite form about a sufficiently large finite tree in the 
Feferman volume above, is not a problem, assuming that we can handle 
labeled finite trees and embeddings.

So the next steps are to

1) handle such finite combinatorial material appropriately, so that 
we always get bounded induction with respect to the new language. 
That is very doable, and will be taken up in a later posting.

2) the major step of figuring out how to introduce infinite objects. 
I will attempt to do this for the most critical situation of all - 
that of real analysis. The future of Strict Reverse Mathematics 
depends critically on how "perfect" this can be accomplished. 
Otherwise, we will just have "Strict Reverse Finite Mathematics", and 
also (the beginnings of) "Strict Reverse Number Theory".

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 177th in a series of self contained numbered postings to 
FOM covering a wide range of topics in f.o.m. The list of previous 
numbered postings #1-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM

Harvey Friedman