[FOM] Strict Reverse Math/correction

[Harvey Friedman]

I wrote http://www.cs.nyu.edu/pipermail/fom/2014-September/018159.html

1. Linearly ordered integral domain axioms.
2. Finite interval. [x,y] exists.
3. Boolean difference. A\B exists.
4. Set addition. A + B = {x+y: x in A and y in B} exists.
5. Set multiplication. AxB = {xy: x in A and y in B} exists.
6. Least element. Every nonempty set has a least element.
7. n^0 = 1. m >= 0 implies n^(m+1) = n^m x n. n^m defined implies m >= 0.
8. {n^0,...,n^m} exists.

and said that the above is a conservative extension of EFA =
exponential function arithmetic = ISigma0(exp).

8 needs to be changed to

8. {0+n^0,1+n^1,...,m+n^m} exists.

This issue is not a problem in SRM formulations with finite sequences
- we can get away with postulating that (n^0,n^1,...,n^m). In any
case, one first proves that 1-7 above is conservative over PFA =
polynomial function arithmetic = ISigma0.

Harvey