[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