# [FOM] 177:Strict Reverse Mathematics 1

Harvey Friedman friedman at math.ohio-state.edu
Tue Jun 10 20:27:37 EDT 2003

```It has been slowly dawning on me that it IS possible to do reverse
mathematics perfectly, without compromise - although I am fully
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
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

```