[FOM] 211:Coding in Reverse Mathematics 2

Harvey Friedman friedman at math.ohio-state.edu
Wed Feb 4 10:52:44 EST 2004


We continue from posting #210, Coding in Reverse Mathematics 1.

CODING IN REVERSE MATHEMATICS 2
by
Harvey M. Friedman
February 4, 2004

1. REAL NUMBERS.

We will assume that we are working over some appropriate extension T of RCA0
in which the field of rational numbers has been properly handled, as well as
infinite sequences of rational numbers and sets of rational numbers.
(Codings of these items of course are not problematic).

Let L1 be the following language.

1. LRM (language of reverse mathematics).
2. A new sort RE for real numbers.
3. The ordered field constants, relations, and functions, for RE. (We do not
use any special equality for the sort RE, but rather general equality; see
the discussion in posting #210).
4. The identity function I(Q,Z) from the sort of rational numbers Q one-one
into RE.
5. General equality.

There are two main types of codings of L1 into T. Within each type, there
are some important choices.

1. Dedekind cut codings. In the strict left Dedekind cut coding, RE is
interpreted as the strict left cuts of rationals; i.e., sets of rationals
closed to the left, missing at least one rational, and with no maximum
element. In the left Dedekind cut coding, we omit the requirement that there
is no greatest element. In the strict left Dedekind cut coding, two left
cuts are equal if and only if they have the same elements. In the left
Dedekind cut coding, equality two left Dedekind cuts are considered equal if
and only if they have the same nonmaximum elements. In both cases, the cuts
are not considered equal to any element of the other sorts, including the
sort for sets of rationals. In either case, we give the usual ordered field
structure over T. I(Q,Z) is defined in the obvious way. Note that in the
case of left Dedekind cut coding, we have to be alert about the equality
relation.

2. Cauchy sequence codings. In the exponential Cauchy sequence coding, RE is
interpreted as infinite sequences of rational numbers, obeying

m < n implies |q_m - q_n| < 2^-m

as stated in Simpson's SOSOA, page 27. In estimated Cauchy sequence coding,
RE is interpreted as infinite sequences of rational numbers, such that for
some increasing (<=) and unbounded f:N into N (stated in the usual way in
T), 

m < n implies |q_m - q_n)| < 1/f(m).

Finally, in general Cauchy sequence coding, RE is interpreted as infinite
seqeunces of rational numbers, such that for all rationals epsilon > 0 there
exists M in N such that

m,n >= M implies |q_m - q_n| < epsilon.

In Cauchy sequence codings, equality between two appropriate sequences
p0,p1,..., and q0,q1,..., is defined by

for all rationals epsilon > 0 there exists M in N such that

m >= M implies |p_m - q_m| < epsilon.

For all five of these codings, we can define the field operations and order
in the obvious way. In each case, it is provable in T that the field
operations and the order respect the equality relation, and that we have
defined an ordered field. Also we interpret I(Q,RE) in the obvious way, with
the obvious cuts and the obvious constant sequences. Also we can prove in T
that for each of these codings, we have the required axioms for equality for
the general equality relation.

We can prove in T that the first four of these codings are equivalent. Or we
just say that these first four codings are equivalent - since part of the
coding is the designation of L1 and T. This means that there are
isomorphisms between the first four, provably in T. Or more precisely,
isomorphisms can be defined which provably work within T.

However, the fifth coding is NOT equivalent to the other four. There is no
isomorphism that provably works in T.

However, there are isomorphisms between all five codings that provable works
in T + ACA0. So if we consider these five codings to be from L1 into T +
ACA0, rather than from L1 into T, then they become equivalent (isomorphic)
codings. 

We now come to the crucial matter of the appropriate common
iso-axiomatization for the first four codings form L1 into T, above.

1. T.
2. RE forms an ordered field under the ordered field primitives, including
general equality (for this purpose, only the behavior of general equality on
the sort RE is relevant).
3. I(Q,RE) is an isomorphic embedding, as ordered fields.
4. For every x in sort RE, there is a set of all rationals q such that
I(Q,RE)(q) < x.
5. For every A in sort P(Q), i.e., A is a set of rationals, if A forms a
left cut in Q, then the values of I(Q,RE) on the elements of A have a least
upper bound in RE.

An alternative iso-axiomatization can be given using the first two kinds of
Cauchy sequences.
 
We leave it to the reader to verify that this is an iso-axiomatization for
the first four codings of L1 into T.

For the fifth coding, we have the following iso-axiomatization.

1. T.
2. RE forms an ordered field under the ordered field primitives, including
general equality (for this purpose, only the behavior of general equality on
the sort RE is relevant).
3. I(Q,RE) is an isomorphic embedding, as ordered fields.
4. For every x in sort RE, there is a general Cauchy sequence of rationals
(see above) such that the values of the sequence under I(Q,RE) converge to x
(in the general sense of convergence without any kind of estimate).
5. For every general Cauchy sequence of rationals (see above) there exists x
in sort RE such that the values of the sequence under I(Q,RE) converge to x
(in the general sense of convergence without any kind of estimate).

We leave it to the reader to verify that this is an iso-axiomatization for
the fifth coding of L1 into T.

We think we know that this fifth coding of L1 into T is very bad.

PROBLEM. Give a particularly simple and basic mathematical theorem involving
RE which cannot be proved from the iso-axiomatization of the fifth coding,
but can be proved from the iso-axiomatization of the first four codings.

2. INFINITE SEQUENCES OF REAL NUMBERS.

We now start with the iso-axiomatization T1 of L1 into T, which is the first
iso-axiomatization for the first four codings, from section 1.

We now introduce infinite sequences of real numbers to T1, and double
infinite sequences of real numbers, via the following language L2.

1. L1.
2. A new sort for infinite sequences of real numbers, UF(N,RE), for "unary
function from N into RE".
3. A new sort for double infinite sequences of real numbers, BF(N,RE), for
"binary function from N into RE".
4. The application functions A(f,n) and A(f,n,m), for f(n) and g(n,m),
respectively, where f is in sort UF(N,RE) and g is in sort BF(N,RE).

The first coding of UF(N,RE) and BF(N,RE) is by functions f:N^2 into Q and
g:N^3 into Q, where the cross sections are Cauchy sequence with exponential
bound (see section 1).

The second coding of UF(N,RE) and BF(N,RE) is by functions f:N^2 into Q and
g:N^3 into Q, where the cross sections are Cauchy sequence with nonspecific
function bound (see section 1).

The third coding of UF(N,RE) and BF(N,RE) is by functions f:N^2 into Q and
g:N^3 into Q, where the cross sections are general Cauchy sequences with no
bound (see section 1).

In all three cases, general equality on ISQ(RE) is defined coordinatewise.
Also, application is interpreted in the obvious way.

We introduce the following iso-axiomatization T2 for the first coding of L2
into T1. 

1. T1.
2. Every unary and binary infinite sequences of rationals defines a unary
and binary infinite sequence of reals via the embedding I(Q,R).
3. The unary and binary infinite sequences of reals are the same up to
bijections of indices (bijection from N one-one onto N^2).
4. If the cross sections of a binary infinite sequence of reals each define
Cauchy sequences of reals with exponential bound, then we can take the limit
sequence, which is a unary infinite sequence of reals.
5. To every unary infinite sequence of reals there is an approximating
binary infinite sequence of rationals, whose cross sections each converge to
the corresponding term in the given unary infinite sequence of reals, with
exponential estimates.

We leave it to the reader to verify that this is an iso-axiomatization of
the coding. 

The other two codings are very bad, we think. It seems that no two of these
three codings are equivalent.

PROBLEMS. Investigate these other two codings. Give appropriate
iso-axiomatizations. Find the most basic facts that are not provable in
these iso-axiomatizations, but are provable in T2.

To be continued... metric spaces, Polish spaces, continuous functions...

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 211th 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
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM
207:On foundations of special relativistic kinematics 2  1/26/04  12:18AM
208:On foundations of special relativistic kinematics 3  1/26/04  12:19AAM
209:Faithful Representation in Set Theory with Atoms 1/31/04 7:18AM
210:Coding in Reverse Mathematics 1  2/2/04  12:47AM

Harvey Friedman









More information about the FOM mailing list