[FOM] 181:Strict Reverse Mathematics 2

Harvey Friedman friedman at math.ohio-state.edu
Thu Jun 19 02:06:26 EDT 2003


COMMENT ON #180, Provable Functions of PA, 6/16/03, 12:42AM. Some 
stronger results exist in the literature, which I was not aware of, 
due to Sam Buss and Jeremy Avigad. See Avigad in the Feferfest volume 
(Reflections on the Foundations of Mathematics, Lecture Notes in 
Logic, Essays in Honor of Solomon Feferman, ed. Sieg, Sommer, 
Talcott, ASL, 2002), See Buss in the Proceedings of the ninth 
international congress on logic, methodology, and philosophy of 
science, Uppsala, Sweden, 1991, Elsevier, 1994.

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

In #177, Strict Reverse Mathematics 1, we initiated the development 
of strict reverse mathematics for finite mathematics. We used the 
discrete ordered ring of integers, and finite sequences of integers, 
as the basis for that development. The axioms used are claimed to be 
strictly mathematical.

Of course that doesn't mean that research should stop, or even pause, 
in making these axioms for minimalistically mathematical. But it has 
reached a critical level.

We now want to try to do the same thing for (countably infinite) 
discrete mathematics. A great deal of the development of ordinary 
Reverse Mathematics surrounds countable structures, where one works 
with structures on omega, assuming a coding of relevant finite 
objects as elements of omega.

The finite coding into omega is not really a problem - once we have 
#177. Yes, it needs to be addressed carefully. I will address it in a 
later posting, where I consider the strict reverse mathematics of 
general finite mathematics. But it is more urgent to see how one can 
purely mathematically introduce enough infinite objects for reverse 
mathematics.

#THE SYSTEM DORISE#

DORISE stands for "discrete ordered ring with infinite sequences and 
exponentiation".

DORISE uses two sorts. One sort is for integers, and the other sort 
is for infinite sequences of integers.

We use variables x_n, n >= 1, over integers, and variables alpha_n, 
n >= 1, over infinite sequences of integers.

We use 0,1,+,x,-,<,= on the integers, as well as exponentiation. We 
only care about exponentiation with exponent >= 0. We follow the 
convention x^0 = 1.

For infinite sequences, we use alpha_n(t), where t is a numerical 
term, for the t-th term of the infinite sequence alpha_n, counting 
from 1.

We can either use the standard logic that allows undefined terms, or 
we can set alpha_n(t) by default to be 0 if t <= 0, or we can be 
agnostic about integer alpha_n(t) is, if t <= 0. This is a matter of 
choice. Similarly for x^y where y < 0.

I personally prefer biting the bullet and allowing undefined terms, 
with the associated standard complete system of axioms and rules of 
logic. So in the intended interpretation, alpha_n(t) is defined if 
and only if t > 0, and x^y is defined if and only if y >= 0.

We are going to state the axioms of DORISE in semiformal style. We 
will use the term "sequence" for "infinite sequence". There are 
substantial redundancies in these axioms, but that is not important.

1. The usual discrete ordered ring axioms, together with x^0 = 1, 
x^(y+1) = x^y dot x. Also x^y denotes if and only if y >= 0. And 
alpha[n] denotes if and only if n > 0.
2. Every arithmetic series with any integer difference, starting with 
any integer, exists. This is stated using plus and times. This axiom 
is given using addition and multiplication.
3. Every geometric series with any integer ratio, starting with any 
integer, exists. This axiom is given using exponentiation.
4. Any two sequences can be pointwise added, pointwise multiplied, 
pointwise maximized, and pointwise minimized.
5. Let alpha be a sequence and beta be a sequence all of whose terms 
are positive. We can form the sequence whose n-th term is the 
beta(n)-th term of alpha.
6. Let alpha,beta,gamma be sequences, and n,m,r > 0. We can form the 
strictly increasing sequence which begins with the reordering in 
strictly increasing order of the first n terms of alpha with the 
first m terms of beta deleted (informally, first delete then 
reorder). This is followed by the first r terms of gamma repeated 
infinitely often. This axiom is formulated using the obvious 
numerical operations on indices.
7. There are two sequences that together form a one-one enumeration 
of all ordered pairs of integers. I.e., there are alpha,beta such 
that for all integers n,m, there is a unique i such that alpha_i = n 
and beta_i = m.
8. Every permutation of N has an inverse. I.e., let alpha be one-one 
and onto the positive integers. Then there exists beta such that for 
all n > 0, alpha(beta(n)) = n.

This Strict Reverse Mathematics system, DORISE, is a conservative 
extension of IDelta0(Z,exp) which is essentially IDelta0(N,exp) = EFA 
(exponential function arithmetic).

DORISE is actually equivalent to the Reverse Mathematics system of 
RCA0*, in Simpson, Subsystems of second order arithmetic, Springer 
(and soon to be ASL), 1999, p. 410-411, provided we take into account 
Z versus omega, and infinite sequences of integers versus infinite 
subsets of omega.

#EXTENSIONS OF DORISE#

There are some important extensions of the Strict Reverse Mathematics 
system DORISE.

To derive Sigma1 induction, and therefore equivalence with my base 
theory RCA0 for Reverse Mathematics, we can just add

9. Every sequence has a term of least magnitude.

NOTE: The system 1-9 is therefore already not provably consistent in 
PRA = primitive recursive arithmetic.

We obtain equivalence with ACA0 by taking 1-8 together with

10. Every sequence of positive terms whose terms are unbounded, can 
be rewritten in strictly increasing order (i.e., with the same terms 
but reordered).

ACA0 is also equivalent to 1-10.

#FURTHER DEVELOPMENTS#

We will continue in an expected way, in a later posting, by adding 
axioms for the full range of finite mathematics, and also some 
additional axioms for the full range of discrete mathematics.

In the usual development of Reverse Mathematics, once we have RCA0 
(or perhaps RCA0*), we consider that we have an appropriate base 
theory for the full range of discrete mathematics. This is because 
obvious standard coding of an apparently unproblematic nature is 
accepted. We agree that it is unproblematic, but we still wish to 
adhere to Strict Reverse Mathematics, which doesn't accept any 
coding, and only strictly mathematical axioms.

Also, in the usual development of Reverse Mathematics, once we have 
RCA0 (or perhaps RCA0*), we consider that we have an appropriate base 
theory for real analysis. The codings for real analysis are much more 
delicate than the codings for discrete mathematics, and are given in 
Simpson's book cited above.

Although I think that these codings are ultimately inevitable, this 
needs to be justified, and I know pretty much how to justify them 
with further developments in Strict Reverse Mathematics.

Thus we see the obvious need for Strict Reverse Mathematics and a 
return to my original vision that I had when setting up Reverse 
Mathematics starting in the late sixties. As discussed in my posting 
#177, 8:37PM, 6/10/03, that vision has only been partially realized 
by my setting up of Reverse Mathematics.

Strict Reverse Mathematics promises to realize my original vision - 
or at least my original vision to a significantly greater extent than 
Reverse Mathematics.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 181st 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
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM

Harvey Friedman



More information about the FOM mailing list