[FOM] 210:Coding in Reverse Mathematics 1
Harvey Friedman
friedman at math.ohio-state.edu
Mon Feb 2 00:47:09 EST 2004
CODING IN REVERSE MATHEMATICS 1
by
Harvey M. Friedman
February 2, 2004
1. INTRODUCTION.
The usual language for reverse mathematics is a two sorted system, with one
sort for nonnegative integers with the usual ordered ring operations, called
the N sort, and the second sort for sets of nonnegative integers, call the
S(N) sort. The epsilon relation connects the two sorts. Equality between the
nonnegative integers is taken for granted, but equality between sets of
nonnegative integers is optional.
A good reason for the choice of the language of reverse mathematics, LRM, is
to avoid the bookkeeping complexities involved in using a dynamic language
in which one continually expands the language with new symbols as one
analyzes more and more mathematical statements. In such a continual
expansion, one will also be introducing more and more sorts.
Such a development is not only quite cumbersome, but has the added
disadvantage that different researchers will want to go about such a
development in at least slightly different ways. Of course, some of these
differences will be only a matter of style, whereas others may be more
substantive.
In fact, such a development risks throwing us back into the situation before
the development of set theoretic foundations, where there was a huge
proliferation of notions, and nobody had a clear idea of what was allowable
and what was not. Set theory clarified matters greatly, particularly because
the language is kept to such a minimum.
However, the development of reverse mathematics through the adherence to its
very simple language, LRM, is completely dependent on a device that long
predates RM - namely coding.
We recommend that RM continue its steady development without expanding the
language, through the use of coding. At least this should be the main, very
robust, line of development of RM, as it is nowhere near completely
developed, and is still an enormously productive source of problems,
particularly for recursion theorists.
Here we develop formal tools and indicate how they are used to bear on the
issue of the appropriate of a proposed coding scheme. The tools give
practical criteria for the evaluation and comparison of coding schemes.
However, in order to carry out the analysis that we propose of coding
schemes, we must consider a rather substantial proliferation of many sorted
extensions of LRM and (at least) the base theory RCA0.
In other words, we cannot take coding for granted when carrying out this
program for analyzing and evaluating coding mechanisms. This is as expected.
To be sure, as this program presented here is developed, one can confidently
short circuit much of this language proliferation, focusing on the crucial
points. But that would be at best premature while we are presenting this
program for the first time.
Once again, we are not proposing that RM expand its language or renounce its
adherence to coding mechanisms. We are only proposing that we must do so
when engaging in an appropriate analysis of coding mechanisms.
#############################
Not much mathematics is normally strictly formulated within LRM, and so one
uses standard coding devices in order to give formalizations of a very wide
variety of mathematical statements within LRM.
For a wide variety of mathematical statements, the "correctness" or
"appropriateness" of the coding used is completely unpoblematic, and goes
virtually unnoticed. Part of the reason why it goes virtually unnoticed is
that such coding mechanisms - in such unproblematic cases - are essentially
the same as those that occur in virtually all aspects of recursion theory,
in proof theory, and at least the finite part of set theory.
For other mathematical statements, the "correctness" or "appropriateness" of
certain coding mechanisms is, in varying degrees, controversial. The main
reason for this controversy is the presence of alternatives that seem
equally reasonable, but are "substantially different".
The judging of the "correctness" or "appropriateness" of coding mechanisms
has largely been of an informal, even sometimes polemical, nature. Here we
wish to present some formal criteria that should go far in clarifying the
issues, and open up new research programs.
The emergence of the systematic foundational investigation that is now known
as reverse mathematics (the term I championed) was documented by me in [1].
Here we propose a new systematic foundational investigation, aimed at
systematically addressing the coding issues in reverse mathematics.
1. ISOAXIOMATIZATIONS OF CODINGS.
Let T be a set of axioms in many sorted first order logic, such as the
fundamental systems of reverse mathematics, RCA0, WKL0, ACA0, ATR0,
Pi11-CA0, that we set up in [2] and [3]. We will assume that the language
L(T) is finite. The typical case is where T is finitely axiomatized, but we
will not make this assumption.
Let T' be an extension of T, again in a finite language L(T'). L(T') may
have additional sorts. This is the case we are most interested in.
A language extension of T is a language L' extending L(T). We will assume
that the language L' is again finite.
The notion of an interpretation of L' into L(T) goes back to Tarski. We give
an informal description of this notion. There are some slight ambiguities
about just how general a form an interpretation can take, in the literature.
However, in practice, such distinctions do not make any difference. In the
present context, we will make one simplification - we will not allow
parameters in interpretations.
It will be convenient for this program to treat equality as follows.
There will be only one equality relation, =, and it makes sense for any two
objects, regardless of sort. It must be interpreted as identity. We call
this the general equality relation.
This is intended to facilitate the construction of combined sorts, which is
very convenient. E.g., suppose we wish to treat infinite sequences from
various sorts of objects that have been built up. Suppose that each of these
various sorts of objects consist of only "finitary" objects. Then rather
than have to introduce infinite sequences for each of these sorts of objects
separately, we can introduce a new combined sort ("union" sort), and then
introduce a sort for infinite sequences from that combined sort. Of course,
if we later want to introduce yet more sorts consisting of only "finitary"
objects, we will have to introduce yet another combined sort by "union", and
then the infinite sequence sort yet again.
So if one wishes to be practical about this, one needs to exercise some
careful planning in order to keep the development under reasonable control.
a. For each sort, we provide a first order definition in L(T), without
parameters, that carves out the "objects" of that sort under the
interpretation. The "objects" of this sort can be tuples of varying lengths
of objects of any of the sorts of L(T).
b. We have a first order definition in L(T), without parameters, for the
equality relation between all "objects", regardless of their sort. It must
be provable in T that this definition defines an equivalence relation.
c. For each constant, relation, and function of L', we have corresponding
definitions in L(T), without parameters. We require that it is provable in T
that the appropriate existence and uniqueness conditions hold, where
uniqueness is expressed in terms of equality relations. It must be provable
in T that "equality" interacts properly with the interpretation of the
constant, relation, and functions of L'. I.e., "equal" objects behave the
same way, as in the standard equality axioms.
If an interpretation of L' into L(T) is the identity on L(T), in the obvious
sense, then we say that it is a
*coding of L' into L(T).*
Now how are we going to judge the appropriateness of a proposed coding of
some L' into L(T)?
Let C be a coding of L' into T. We say that C is iso-axiomatized by T' if
and only if
a. T' is an extension of T with language L'.
b. Let M' be a model of T' and let M be the reduct of M' to L(T). Let C[M]
be the L' structure defined by the coding C from M. Then there is a
definable isomorphism from C[M] onto M', where the definition of the
isomorphism is given by a single fixed formula of L', without parameters,
independently of M,M'.
By compactness, this is equivalent to
a. Same.
b. Let M' be a model of T' and let M be the reduct of M' to L(T). Let C[M]
be the L' structure defined by the coding C from M. Then there is a
definable isomorphism from C[M] onto M', where the definition of the
isomorphism is given by a formula of L', without parameters, that may depend
on M,M'.
We judge a coding C of L' into L(T) as follows. We formulate a theory T'
such that C is iso-axiomatized by T', where
the axioms of T' are chosen to be as mathematically fundamental as possible.
Thus we require that codings be iso-axiomatizable, and that the
iso-axiomatizations state fundamental mathematical facts.
As we shall see, in practice, the relevant iso-axiomatizations embody
theorems - where the theorems come out explicitly in the proof that the
coding is in fact a coding, and that a naturally presented isoaxiomatization
of the coding is in fact such.
Let C1 and C2 be codings of L' into T. We say that C1 and C2 are equivalent
if and only if the following holds. Let M be a model of T and let C1[M],
C2[M] be the L' structures defined by C1,C2. We require that C1[M] and C2[M]
are isomorphic by an isomorphism that is given by a formula of L, without
parameters, that does not depend on M, and which is the identity on L(T).
We now can productively talk about the issue of alternative codings. This
simply means that we have two or more codings C1,...,Ck, of L' into T, with
respective iso-axiomatizations of competing fundamental mathematical
importance, which are not equivalent in the sense of the previous paragraph.
Generally, we will not want to be automatically dogmatic about the choice of
Ci. Instead, we will want to add adjectives to the notions being coded, in
order to conveniently refer to these inequivalent codings. In the long run,
it may be clear that some of these inequivalent codings are of greater
central importance than others.
The matter of choice can be kept fluid in this way, as an arsenal of
reversals is accumulated. Multiple codings may survive in this way, giving
rise to alternative branches of RM = reverse mathematics.
2. SOME INTRODUCTORY EXAMPLES OF CODINGS AND ISOAXIOMATIZATIONS.
Here we will restrict attention to codings into RCA0.
We start with the very simple step of properly adjoining the ring of
integers, Z to RCA0. Notice that even this extremely basic step is of some
complexity.
Let L1 be the following language.
1. The N sort and the P(N) sort of LRM.
2. The new Z sort for integers.
3. The new P(Z) sort for sets of integers.
4. The symbols 0,1,<,+,x,epsilon of LRM.
5. The new symbols 0(Z),1(Z),<(Z),+(Z),x(Z),-(Z) on the Z sort.
6. The new symbol epsilon(Z,P(Z)).
7. Injection function I(N,Z) of sort N into sort Z.
8. General equality =.
The obvious coding C1 interprets integers as the n,0 and n+1,1, n in N. We
interpret the symbols in 5 by the usual explicit definitions from elementary
school arithmetic. (We are working over RCA0). We interpret sets of integers
as X,Y, where X,Y are from P(N), 0 not in Y.
We interpret an integer n,0 being in a set of integers X,Y if and only n
lies in X. We interpret an integer n+1,1 being in a set of integers X,Y if
and only if n+1 lies in Y.
We interpret I(N,Z) by: n goes to n,0.
We now come to the general equality relation (see the discussion of the
convention concerning general equality). We interpret equality as equality
in RCA0. (Equality in RCA0 is, by convention, general equality, and we have
the extensionality axiom for P(N)).
It is obvious that we have given a coding C1 of L1 into RCA0. (It is
understood that we are leaving LRM unchanged in the interpretation).
What is the appropriate iso-axiomatization T1 of C1?
1. The injection of N into Z is one-one onto the objects in Z that are not
<(Z) 0(Z). The injection of N preserves 0,1,<,+,x.
2. Symbols in 5 make Z into a discrete ordered ring.
3. If A,B are in P(N) then there is a set of integers consisting of the
values of I(N,Z) at elements of A together with the minuses (i.e., -(Z)) of
the values of I(N,Z) at elements of B.
4. If E is in P(Z) then the set of all nonnegative integers whose injection
into Z lies in E exists, and the set of all nonnegative integers such that
the minus of its injection in to Z lies in E, also exists.
5. If A,B are in P(Z) then A = B if and only if A,B have the same elements.
6. RCA0.
This iso-axiomatization T1 is indeed of the proper fundamental mathematical
character, with no ad hoc features.
To verify that T1 is indeed an iso-axiomatization of C1, let M1 be a model
of T1 and M be the reduct of M to LRM. We must define an isomorphism of
C1[M] onto M1, uniformly in L1. We leave this to the reader.
Now we have RCA0, L1, C1, T1. We now introduce unary and binary functions
from Z into Z.
Let L2 be the following language.
1. L1.
2. The new sorts UF(Z), BF(Z), for "unary function from Z into Z" and
"binary function from Z into Z".
3. The new sort BR(Z) for "binary relation on Z".
4. The application operations A(f,n) and A(f,n,m), where f is in sort UF(Z)
and BF(Z), respectively, and ,n,m are in sort Z.
We leave the obvious coding C2 of L2 into T1 to the reader. This uses the
standard quadratic Q(x,y) which maps N2 one-one onto N, provably in RCA0.
We now must give a suitable iso-axiomatization T2 of C2.
1. There exists a bijection in BF(Z) from Z x Z onto Z.
2. BF(Z) and UF(Z) are related in the obvious way via any bijection in BF(Z)
from Z x Z onto Z, acting on the domain.
3. The elements of UF(Z) correspond exactly to the elements of BR(Z) that
are total and univalent.
4. BR(Z) and P(Z) are related in the obvious way via any bijection in BF(Z)
from Z x Z onto Z.
5. Equality holds only for objects of the same sort. Within each sort, we
have extensionality.
We leave it to the reader to verify that this is an iso-axiomatization of
C2.
Now that we have L2, C2, T2, we can introduce infinite sequences from Z and
finite sequences from Z. We can then introduce infinite sequences of finite
sequences from Z. In particular, we have infinite sequences of ordered pairs
from Z, where ordered pairs from Z are considered sequences of length 2 from
Z.
All of this is straightforward and nonproblematic, although rather complex.
One really does have fundamentally mathematical iso-axiomatizations.
We should next introduce the field of rational numbers. A good way to do
this is to have two primitive functions back into the Z sort. The first
yields the numerator of the reduced form of the rational q, and the second
yields the denominator of the reduced form of the rational q. Reduced forms
have positive integer denominators, and integer numerators. We should also
have the injection from Z into rationals. We can give an obvious coding into
T2. We can also give a fundamentally mathematical iso-axiomatization.
There are other ways to do this that are arguably "nicer", that do not
involve reduced forms. One can surely prove an appropriate result that other
good ways of doing this are "equivalent". And surely there is a nice way of
talking about what equivalence should mean here. The discussion at the end
of the Introduction is not quite general enough, because here we are talking
about using somewhat different primitives. We won't go into the general
treatment of equivalent codings here, when the primtiives differ. It
suffices to say that there is an underlying common goal of different setups
for rationals here, and that is the ordered field of rationals - even if
there are different primitives surrounding the treatment. The appropriate
notion of equivalence tells us that we get "provably isomorphic fields" in
the appropriate sense.
Once we have suitably introduced rationals, we can begin to get into
something more interesting than this previous spadework that surrounds the
nonproblematic coding mechanisms of RM. Specifically, we can get into
*coding of real numbers and finite and infinite sequences of real numbers.*
as well as much more advanced issues.
This is the beginning of where we see the real power of these ideas -
**mathematical iso-axiomatizations of codings.**
This will be taken up in the next installment.
REFERENCE
[1] H. Friedman and S. Simpson, Issues and problems in reverse mathematics,
in: Computability Theory and its Applications, ed. Cholak, Lempp, Lerman,
Shore, Contemporary Mathematics, vol. 257, American Math. Soc., 2000, pp.
127-144.
*********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 209th 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
Harvey Friedman
More information about the FOM
mailing list