[FOM] 244:LUB systems

[Harvey Friedman]

There is a very strong correspondence between certain fragments of Z2, which
is the standard first order theory of second order arithmetic, and certain
families of real closed fields with discrete subgroups.

This provides an unexpectedly clear model theoretic interpretation of
various developments in subsystems of second order arithmetic, as well as in
the closely associated recursion theory.

This correspondence between two subjects with rather different goals should
suggest fruitful lines of research based on new kinds of questions.

1. LUB Fields.

An LUB field is an ordered field in which every bounded definable subset has
a least upper bound.

THEOREM 1.1. The LUB fields are exactly the real closed fields.

We can strengthen Theorem 1.1 as follows.

THEOREM 1.2. Suppose F is an ordered field with the least upper bound
property for all atomic formulas. Then F is a real closed field.

2. LUB Systems.

An LUB system is a pair (F,S), where

1. F is an ordered field.
2. S is a discrete additive subgroup of F. (Here discrete means that S
intersect (0,1) = emptyset.)
3. Every bounded subset of F that is first order definable over (F,S) has a
least upper bound in F.

By Theorem 1.1, in every LUB system, the field is a real closed field.

A weak LUB system is a pair (F,S), where

1. F is an ordered field.
2. S is a discrete additive subgroup of F. (Here discrete means that S
intersect (0,1) = emptyset.)
3. Every bounded subset of F definable by a first order formula in the
language of (F,S), with quantifiers ranging over S and parameters from F,
has a least upper bound in F.

By Theorem 1.2, every weak LUB system is real closed.

THEOREM 2.1. The family of LUB systems and the family of models of Z2 are
synonymous. 

We can be explicit about the synonymy. Let an LUB field (F,S) be given. The
corresponding model of Z2 has first order part S,0,+,x,<. The second order
part is the set of all (F,S) definable subsets of S. In order to verify that
this satisfies Z2, we need a lemma to the effect that all (F,S) definable
subsets of S are (F,S) definable in a particular way, with a single
parameter. 

Conversely, let a model (A,X) be given of Z2, where A is the first order
part and X is the second order part. Use the usual construction of the real
number system via Dedekind cuts to construct the corresponding LUB system
with first order part A (made into a discrete group).

These ideas can be refined to give the following.

THEOREM 2.2. The family of weak LUB systems and the family of models of
Pi11-CA0 are synonymous.

Once we have this synonymy in place, we can apply some of the detailed
information known about models of Z2 and some its fragments, to the LUB
context. 

THEROEM 2.3. There is no LUB system which is isomorphically embeddable in
every LUB system. In fact, there is no weak LUB system which is
isomorphically embeddable in every Archimedean LUB system.

THEOREM 2.4. Among the (F,S) which are isomorphically embeddable in every
lub system, there is one in which every one is isomorphically embeddable.
Furthermore, it is unique up to isomorphism. This remains true if we replace
lub with weak lub, in which case we obtain the same (F,S) up to isomorphism.
This (F,S) is real closed but not a weak LUB system. It is an object from
recursion theory - the ordered field of recursive real numbers.

THEOREM 2.5. Among the (F,S) which are isomorphically embeddable in every
Archimedean lub system, there is one in which every one is isomorphically
embeddable. Furthermore, it is unique up to isomorphism. This remains true
if we replace lub with weak lub, in which case we obtain the same (F,S) up
to isomorphism. This (F,S) is real closed but not a weak LUB system. It is
an object from higher recursion theory - the ordered field of
hyperarithmetic real numbers.

THEOREM 2.6. Let (F,S) be an LUB system, where S is countable. There exists
a proper ordered subfield F' of F such that (F',S) is an LUB system.

THEOREM 2.7. There exists an Archimedean weak LUB system (F,S) such that for
no proper ordered subfield F' of F, is (F',S) an LUB system.

Theorem 2.6. is proved using the following theorem from

H. Friedman, Countable models of set theories, in: Mathias and Rogers
(eds.), Cambridge Summer Shool in Mathematical Logic, Lecture Notes in
Mathematics, no. 337, Springer-Verlag 1973, pp. 539-573.

THEOREM. Every omega model of Z2 has a proper omega submodel of Z2.

Quinsey proved a sharpening in

J.E. QUinsey, Applications of Kripke's Notion of Fulfilment, Ph.D. thesis,
Oxford University, 1980, 132 pages.

THEOREM. (Quinsey). Let S be a recursive set of L2 sentences which includes
the axioms of ATR0. Let M be an omega model of S. Then M has a proper omega
submodel M' of M such that M' is again an omega model of S.

This theorem is reproved in

S. Simpson, Subsystems of second order arithmetic, Perspectives in
Mathematical Logic, 1999, page 357, Springer Verlag.

Using it, we obviously obtain

THEOREM 2.8. Let (F,S) be a weak LUB system, where S is countable. There
exists a proper ordered subfield F' of F such that (F',S) is a weak LUB
system. 

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

I use www.math.ohio-state.edu/~friedman/ for downloadable manuscripts.
This is the 244th 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/03  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
211:Coding in Reverse Mathematics 2  2/4/04  10:52AM
212:On foundations of special relativistic kinematics 4  2/7/04  6:28PM
213:On foundations of special relativistic kinematics 5  2/8/04  9:33PM
214:On foundations of special relativistic kinematics 6  2/14/04 9:43AM
215:Special Relativity Corrections  2/24/04 8:13PM
216:New Pi01 statements  6/6/04  6:33PM
217:New new Pi01 statements  6/13/04  9:59PM
218:Unexpected Pi01 statements  6/13/04  9:40PM
219:Typos in Unexpected Pi01 statements  6/15/04  1:38AM
220:Brand New Corrected Pi01 Statements  9/18/04  4:32AM
221:Pi01 Statements/getting it right  10/7/04  5:56PM
222:Statements/getting it right again  10/9/04  1:32AM
223:Better Pi01 Independence  11/2/04  11:15AM
224:Prettier Pi01 Independence  11/7/04  8:11PM
225:Better Pi01 Independence  11/9/04  10:47AM
226:Nicer Pi01 Independence  11/10/04  10:43AM
227:Progress in Pi01 Independence  11/11/04  11:22PM
228:Further Progress in Pi01 Independence  11/12/04  2:49AM
229:More Progress in Pi01 Independence  11/13/04  10:41PM
230:Piecewise Linear Pi01 Independence  11/14/04  9:38PM
231:More Piecewise Linear Pi01 Independence  11/15/04  11:18PM
232:More Piecewise Linear Pi01 Independence/correction  11/16/04  8:57AM
233:Neatening Piecewise Linear Pi01 Independence  11/17/04  12:22AM
234:Affine Pi01 Independence  11/20/04  9:54PM
235:Neatening Affine Pi01 Independence  11/28/04  6:08PM
236:Pi01 Independence/Huge Cardinals  12/2/04  3:49PM
237:More Neatening Pi01 Affine Independence  12/6/04  12:56AM
238:Pi01 Independence/Large Large Cardinals/Correction  12/7/04  10:31PM
239:Pi01 Update  12/11/04  1:12PM
240:2nd Pi01 Update  12/13/04  2:49AM
241:3rd Pi01 Update  12/13/04  4:08AM
242:4th Pi01 Update  12/18/04  9:47PM
243:Inexplicit Pi01/Ordinals of Set Theories  12/19/04  11:48PM

Harvey Friedman